Theorem: Lean4Axiomatic.Integer.Impl.Difference.from_ℕ_inject (Lean4Axiomatic/Integer/Impl/Difference/Core.lean)

State before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
⊢ n₁——0 ≃ n₂——0 → n₁ ≃ n₂
Tactic:
intro (_ : n₁——0 ≃ n₂——0)
State after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁——0 ≃ n₂——0
⊢ n₁ ≃ n₂

State before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁——0 ≃ n₂——0
⊢ n₁ ≃ n₂
Tactic:
have : n₁ + 0 ≃ n₂ + 0 := ‹n₁——0 ≃ n₂——0›
State after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁——0 ≃ n₂——0
this : n₁ + 0 ≃ n₂ + 0
⊢ n₁ ≃ n₂

State before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁——0 ≃ n₂——0
this : n₁ + 0 ≃ n₂ + 0
⊢ n₁ ≃ n₂
Tactic:
calc
  n₁     ≃ _ := Rel.symm AA.identR
  n₁ + 0 ≃ _ := ‹n₁ + 0 ≃ n₂ + 0›
  n₂ + 0 ≃ _ := AA.identR
  n₂     ≃ _ := Rel.refl
State after:
no goals