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

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

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

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

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m, 0) ≃ (n * m + 0 * 0, n * 0 + 0 * m)
Tactic:
apply Rel.symm (α := ℕ × ℕ)
State after:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m + 0 * 0, n * 0 + 0 * m) ≃ (n * m, 0)

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