Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_comm (Lean4Axiomatic/Integer/Impl/Difference/Multiplication.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 (n——m)
State after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m : ℕ
⊢ n——m * b ≃ b * n——m

State before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m : ℕ
⊢ n——m * b ≃ b * n——m
Tactic:
revert b
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ ∀ {b : Difference ℕ}, n——m * b ≃ b * n——m

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

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

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

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

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