Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_invL (Lean4Axiomatic/Integer/Impl/Difference/Negation.lean)

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

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

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

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

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ m + n + 0 ≃ 0 + (n + m)
Tactic:
apply Natural.add_swapped_zeros_eqv.mpr
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ m + n ≃ n + m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ m + n ≃ n + m
Tactic:
exact AA.comm
State after:
no goals