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

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

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

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ a₁——a₂ + b₁——b₂ ≃ b₁——b₂ + a₁——a₂
Tactic:
show (a₁ + b₁)——(a₂ + b₂) ≃ (b₁ + a₁)——(b₂ + a₂)
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ (a₁ + b₁)——(a₂ + b₂) ≃ (b₁ + a₁)——(b₂ + a₂)

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ (a₁ + b₁)——(a₂ + b₂) ≃ (b₁ + a₁)——(b₂ + a₂)
Tactic:
show from_prod (a₁ + b₁, a₂ + b₂) ≃ from_prod (b₁ + a₁, b₂ + a₂)
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ from_prod (a₁ + b₁, a₂ + b₂) ≃ from_prod (b₁ + a₁, b₂ + a₂)

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

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ (a₁ + b₁, a₂ + b₂) ≃ (b₁ + a₁, b₂ + a₂)
Tactic:
calc
  (a₁ + b₁, a₂ + b₂) ≃ _ := AA.substL AA.comm
  (b₁ + a₁, a₂ + b₂) ≃ _ := AA.substR AA.comm
  (b₁ + a₁, b₂ + a₂) ≃ _ := Rel.refl
State after:
no goals