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

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

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

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

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

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

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
⊢ n——m * p——q ≃ k——j * p——q
Tactic:
have h : n + j ≃ k + m := ‹n——m ≃ k——j›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
h : n + j ≃ k + m
⊢ n——m * p——q ≃ k——j * p——q

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
h : n + j ≃ k + m
⊢ n * p + m * q + (k * q + j * p) ≃ k * p + j * q + (n * q + m * p)
Tactic:
calc
  (n * p + m * q) + (k * q + j * p) ≃ _ := Rel.symm expand_swap
  (n + j) * p     + (k + m) * q     ≃ _ := AA.substL (AA.substL h)
  (k + m) * p     + (k + m) * q     ≃ _ := AA.substR (AA.substL (Rel.symm h))
  (k + m) * p     + (n + j) * q     ≃ _ := expand_swap
  (k * p + j * q) + (n * q + m * p) ≃ _ := Rel.refl
State after:
no goals