no goals
n m k : Nat
⊢ n + m = n + k → m = k
induction n with
| zero => simp; intros; assumption
| succ n ih => simp [succ_add]; intro h; apply ih h
case zero
m k : Nat
⊢ m = k → m = k
case zero
m k : Nat
⊢ zero + m = zero + k → m = k
simp
case zero
m k : Nat
a✝ : m = k
⊢ m = k
case zero
m k : Nat
⊢ m = k → m = k
intros
no goals
case zero
m k : Nat
a✝ : m = k
⊢ m = k
assumption
case succ
m k n : Nat
ih : n + m = n + k → m = k
⊢ n + m = n + k → m = k
case succ
m k n : Nat
ih : n + m = n + k → m = k
⊢ succ n + m = succ n + k → m = k
simp [succ_add]
case succ
m k n : Nat
ih : n + m = n + k → m = k
h : n + m = n + k
⊢ m = k
case succ
m k n : Nat
ih : n + m = n + k → m = k
⊢ n + m = n + k → m = k
intro h
no goals
case succ
m k n : Nat
ih : n + m = n + k → m = k
h : n + m = n + k
⊢ m = k
apply ih h