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

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

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p : ℕ
⊢ ∀ {b : Difference ℕ}, q——p * (b + c) ≃ q——p * b + q——p * 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 + q——p * c

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

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m : ℕ
⊢ ∀ {c : Difference ℕ}, q——p * (n——m + c) ≃ q——p * n——m + q——p * 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 + q——p * k——j

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

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

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

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
Tactic:
let qj := q * j
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
Tactic:
let pn := p * n
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
Tactic:
let pm := p * m
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
Tactic:
let pk := p * k
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
Tactic:
let pj := p * j
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
Tactic:
show q——p * n_k——m_j ≃ (qn + pm)——(qm + pn) + (qk + pj)——(qj + pk)
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q——p * n_k——m_j ≃ (qn + pm)——(qm + pn) + (qk + pj)——(qj + pk)

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q——p * n_k——m_j ≃ (qn + pm)——(qm + pn) + (qk + pj)——(qj + pk)
Tactic:
show (q * n_k + p * m_j)——(q * m_j + p * n_k)
   ≃ ((qn + pm) + (qk + pj))——((qm + pn) + (qj + pk))
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ (q * n_k + p * m_j)——(q * m_j + p * n_k) ≃ (qn + pm + (qk + pj))——(qm + pn + (qj + pk))

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ (q * n_k + p * m_j)——(q * m_j + p * n_k) ≃ (qn + pm + (qk + pj))——(qm + pn + (qj + pk))
Tactic:
show from_prod (q * n_k + p * m_j, q * m_j + p * n_k)
   ≃ from_prod ((qn + pm) + (qk + pj), (qm + pn) + (qj + pk))
State after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ from_prod (q * n_k + p * m_j, q * m_j + p * n_k) ≃ from_prod (qn + pm + (qk + pj), qm + pn + (qj + pk))

State before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ from_prod (q * n_k + p * m_j, q * m_j + p * n_k) ≃ from_prod (qn + pm + (qk + pj), qm + pn + (qj + pk))
Tactic:
apply AA.subst₁
State after:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ (q * n_k + p * m_j, q * m_j + p * n_k) ≃ (qn + pm + (qk + pj), qm + pn + (qj + pk))

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ (q * n_k + p * m_j, q * m_j + p * n_k) ≃ (qn + pm + (qk + pj), qm + pn + (qj + pk))
Tactic:
apply Relation.Equivalence.Impl.Prod.eqv_defn.mpr
State after:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
Tactic:
have distrib_swap (w x y z : ℕ)
    : q * (w + y) + p * (x + z) ≃ (q * w + p * x) + (q * y + p * z)
    := calc
  q * (w + y) + p * (x + z)         ≃ _ := AA.substL AA.distribL
  (q * w + q * y) + p * (x + z)     ≃ _ := AA.substR AA.distribL
  (q * w + q * y) + (p * x + p * z) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (q * w + p * x) + (q * y + p * z) ≃ _ := Rel.refl
State after:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
Tactic:
apply And.intro
State after:
case a.left
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj)

case a.right
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * m_j + p * n_k ≃ qm + pn + (qj + pk)

State before:
case a.left
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj)
Tactic:
exact distrib_swap n m k j
State after:
no goals

State before:
case a.right
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
Tactic:
exact distrib_swap m n j k
State after:
no goals