Theorem: succ_inj (Instructor/Lectures/grad/sets_relations.lean)

State before:
⊢ Injective fun n => n + 1
Tactic:
unfold Injective
State after:
⊢ ∀ ⦃a₁ a₂ : ℕ⦄, (fun n => n + 1) a₁ = (fun n => n + 1) a₂ → a₁ = a₂

State before:
⊢ ∀ ⦃a₁ a₂ : ℕ⦄, (fun n => n + 1) a₁ = (fun n => n + 1) a₂ → a₁ = a₂
Tactic:
intros a1 a2 h
State after:
a1 a2 : ℕ
h : (fun n => n + 1) a1 = (fun n => n + 1) a2
⊢ a1 = a2

State before:
a1 a2 : ℕ
h : (fun n => n + 1) a1 = (fun n => n + 1) a2
⊢ a1 = a2
Tactic:
simp [Nat.add] at h
State after:
a1 a2 : ℕ
h : a1 = a2
⊢ a1 = a2

State before:
a1 a2 : ℕ
h : a1 = a2
⊢ a1 = a2
Tactic:
assumption
State after:
no goals