Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_identL (Lean4Axiomatic/Integer/Impl/Difference/Addition.lean)

State before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ 0 + a ≃ a
Tactic:
revert a
State after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, 0 + a ≃ a

State before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, 0 + a ≃ a
Tactic:
intro (n——m)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 0 + n——m ≃ n——m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 0 + n——m ≃ n——m
Tactic:
show 0——0 + n——m ≃ n——m
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 0——0 + n——m ≃ n——m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 0——0 + n——m ≃ n——m
Tactic:
show (0 + n)——(0 + m) ≃ n——m
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (0 + n)——(0 + m) ≃ n——m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (0 + n)——(0 + m) ≃ n——m
Tactic:
show from_prod (0 + n, 0 + m) ≃ from_prod (n, m)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ from_prod (0 + n, 0 + m) ≃ from_prod (n, m)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ from_prod (0 + n, 0 + m) ≃ from_prod (n, m)
Tactic:
apply AA.subst₁
State after:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (0 + n, 0 + m) ≃ (n, m)

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (0 + n, 0 + m) ≃ (n, m)
Tactic:
calc
  (0 + n, 0 + m) ≃ _ := AA.substL AA.identL
  (n, 0 + m)     ≃ _ := AA.substR AA.identL
  (n, m)         ≃ _ := Rel.refl
State after:
no goals