mwe.lean

structure mystruct := {a : ℕ} {b : ℕ}

def a_pred (s : mystruct) : option ℕ
  := match s.a with nat.zero := none
                  | (nat.succ a) := some a end

lemma mylemma
  : ∀ {a' b : ℕ}, a_pred {a := a'.succ, b := b} = some a'
  := begin intros, simp [a_pred] end

theorem mytheorem
  : ∀ {a b : ℕ}, a_pred {a := a, b := b}
                = ite (a = a.pred) (none) (some a.pred)
  := begin
    intros,
    cases h : a,
    simp [a_pred],
    sorry
  end