Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_identL (Lean4Axiomatic/Integer/Impl/Difference/Multiplication.lean)

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

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

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

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

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

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

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