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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a * b * c ≃ a * (b * c)
Tactic:
intro (q——p)
State after:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
q p : ℕ
⊢ q——p * b * c ≃ q——p * (b * c)

State before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
q p : ℕ
⊢ q——p * b * c ≃ q——p * (b * c)
Tactic:
revert b
State after:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p : ℕ
⊢ ∀ {b : Difference ℕ}, q——p * b * c ≃ q——p * (b * c)

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

State before:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p n m : ℕ
⊢ q——p * n——m * c ≃ q——p * (n——m * c)
Tactic:
revert c
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m : ℕ
⊢ ∀ {c : Difference ℕ}, q——p * n——m * c ≃ q——p * (n——m * c)

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

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)
Tactic:
let qn_pm := q * n + p * m
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)
Tactic:
let qm_pn := q * m + p * n
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)
Tactic:
let nk_mj := n * k + m * j
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)
Tactic:
let nj_mk := n * j + m * k
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)
Tactic:
show qn_pm——qm_pn * k——j ≃ q——p * nk_mj——nj_mk
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ qn_pm——qm_pn * k——j ≃ q——p * nk_mj——nj_mk

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ qn_pm——qm_pn * k——j ≃ q——p * nk_mj——nj_mk
Tactic:
show (qn_pm * k + qm_pn * j)——(qn_pm * j + qm_pn * k)
   ≃ (q * nk_mj + p * nj_mk)——(q * nj_mk + p * nk_mj)
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ (qn_pm * k + qm_pn * j)——(qn_pm * j + qm_pn * k) ≃ (q * nk_mj + p * nj_mk)——(q * nj_mk + p * nk_mj)

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ (qn_pm * k + qm_pn * j)——(qn_pm * j + qm_pn * k) ≃ (q * nk_mj + p * nj_mk)——(q * nj_mk + p * nk_mj)
Tactic:
show from_prod (qn_pm * k + qm_pn * j, qn_pm * j + qm_pn * k)
   ≃ from_prod (q * nk_mj + p * nj_mk, q * nj_mk + p * nk_mj)
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ from_prod (qn_pm * k + qm_pn * j, qn_pm * j + qm_pn * k) ≃ from_prod (q * nk_mj + p * nj_mk, q * nj_mk + p * nk_mj)

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

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ (qn_pm * k + qm_pn * j, qn_pm * j + qm_pn * k) ≃ (q * nk_mj + p * nj_mk, q * nj_mk + p * nk_mj)
Tactic:
apply Relation.Equivalence.Impl.Prod.eqv_defn.mpr
State after:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ qn_pm * k + qm_pn * j ≃ q * nk_mj + p * nj_mk ∧ qn_pm * j + qm_pn * k ≃ q * nj_mk + p * nk_mj

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ qn_pm * k + qm_pn * j ≃ q * nk_mj + p * nj_mk ∧ qn_pm * j + qm_pn * k ≃ q * nj_mk + p * nk_mj
Tactic:
have redistribute (x y : ℕ)
    : (q * n + p * m) * x + (q * m + p * n) * y
    ≃  q * (n * x + m * y) + p * (n * y + m * x)
    := calc
  (q * n + p * m) * x + (q * m + p * n) * y
    ≃ _ := AA.substL AA.distribR
  (q * n) * x + (p * m) * x + (q * m + p * n) * y
    ≃ _ := AA.substR AA.distribR
  (q * n) * x + (p * m) * x + ((q * m) * y + (p * n) * y)
    ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (q * n) * x + (q * m) * y + ((p * m) * x + (p * n) * y)
    ≃ _ := AA.substR AA.comm
  (q * n) * x + (q * m) * y + ((p * n) * y + (p * m) * x)
    ≃ _ := AA.substL (AA.substL AA.assoc)
  q * (n * x) + (q * m) * y + ((p * n) * y + (p * m) * x)
    ≃ _ := AA.substL (AA.substR AA.assoc)
  q * (n * x) + q * (m * y) + ((p * n) * y + (p * m) * x)
    ≃ _ := AA.substR (AA.substL AA.assoc)
  q * (n * x) + q * (m * y) + (p * (n * y) + (p * m) * x)
    ≃ _ := AA.substR (AA.substR AA.assoc)
  q * (n * x) + q * (m * y) + (p * (n * y) + p * (m * x))
    ≃ _ := AA.substL (Rel.symm AA.distribL)
  q * (n * x + m * y) + (p * (n * y) + p * (m * x))
    ≃ _ := AA.substR (Rel.symm AA.distribL)
  q * (n * x + m * y) + p * (n * y + m * x)
    ≃ _ := Rel.refl
State after:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
redistribute : ∀ (x y : ℕ), (q * n + p * m) * x + (q * m + p * n) * y ≃ q * (n * x + m * y) + p * (n * y + m * x)
⊢ qn_pm * k + qm_pn * j ≃ q * nk_mj + p * nj_mk ∧ qn_pm * j + qm_pn * k ≃ q * nj_mk + p * nk_mj

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
redistribute : ∀ (x y : ℕ), (q * n + p * m) * x + (q * m + p * n) * y ≃ q * (n * x + m * y) + p * (n * y + m * x)
⊢ qn_pm * k + qm_pn * j ≃ q * nk_mj + p * nj_mk ∧ qn_pm * j + qm_pn * k ≃ q * nj_mk + p * nk_mj
Tactic:
apply And.intro
State after:
case a.left
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
redistribute : ∀ (x y : ℕ), (q * n + p * m) * x + (q * m + p * n) * y ≃ q * (n * x + m * y) + p * (n * y + m * x)
⊢ qn_pm * k + qm_pn * j ≃ q * nk_mj + p * nj_mk

case a.right
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
redistribute : ∀ (x y : ℕ), (q * n + p * m) * x + (q * m + p * n) * y ≃ q * (n * x + m * y) + p * (n * y + m * x)
⊢ qn_pm * j + qm_pn * k ≃ q * nj_mk + p * nk_mj

State before:
case a.left
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
redistribute : ∀ (x y : ℕ), (q * n + p * m) * x + (q * m + p * n) * y ≃ q * (n * x + m * y) + p * (n * y + m * x)
⊢ qn_pm * k + qm_pn * j ≃ q * nk_mj + p * nj_mk
Tactic:
exact redistribute k j
State after:
no goals

State before:
case a.right
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
redistribute : ∀ (x y : ℕ), (q * n + p * m) * x + (q * m + p * n) * y ≃ q * (n * x + m * y) + p * (n * y + m * x)
⊢ qn_pm * j + qm_pn * k ≃ q * nj_mk + p * nk_mj
Tactic:
exact redistribute j k
State after:
no goals