Theorem: Form.nat_injection (Fine/PropositionalLanguage.lean)

State before:
⊢ Function.Injective atom
Tactic:
unfold Function.Injective
State after:
⊢ ∀ ⦃a₁ a₂ : ℕ⦄, #a₁ = #a₂ → a₁ = a₂

State before:
⊢ ∀ ⦃a₁ a₂ : ℕ⦄, #a₁ = #a₂ → a₁ = a₂
Tactic:
intros n m h₁
State after:
n m : ℕ
h₁ : #n = #m
⊢ n = m

State before:
n m : ℕ
h₁ : #n = #m
⊢ n = m
Tactic:
injection h₁
State after:
no goals