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

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
a₂ : Difference ℕ
n m : ℕ
⊢ n——m ≃ a₂ → -n——m ≃ -a₂
Tactic:
revert a₂
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ ∀ {a₂ : Difference ℕ}, n——m ≃ a₂ → -n——m ≃ -a₂

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

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ n——m ≃ k——j → -n——m ≃ -k——j
Tactic:
intro (_ : n——m ≃ k——j)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
⊢ -n——m ≃ -k——j

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
⊢ -n——m ≃ -k——j
Tactic:
have : n + j ≃ k + m := ‹n——m ≃ k——j›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ -n——m ≃ -k——j

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ -n——m ≃ -k——j
Tactic:
show m——n ≃ j——k
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m——n ≃ j——k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m——n ≃ j——k
Tactic:
show m + k ≃ j + n
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m + k ≃ j + n

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m + k ≃ j + n
Tactic:
calc
  m + k ≃ _ := AA.comm
  k + m ≃ _ := Rel.symm ‹n + j ≃ k + m›
  n + j ≃ _ := AA.comm
  j + n ≃ _ := Rel.refl
State after:
no goals