internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ from_prod (n * k + m * j, n * j + m * k) ≃ from_prod (k * n + j * m, k * m + j * n)
Tactic:
apply AA.subst₁
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ (n * k + m * j, n * j + m * k) ≃ (k * n + j * m, k * m + j * n)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_comm
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ (n * k + m * j, n * j + m * k) ≃ (k * n + j * m, k * m + j * n)
Tactic:
calc
  (n * k + m * j, n * j + m * k) ≃ _ := AA.substL (AA.substL AA.comm)
  (k * n + m * j, n * j + m * k) ≃ _ := AA.substL (AA.substR AA.comm)
  (k * n + j * m, n * j + m * k) ≃ _ := AA.substR (AA.substL AA.comm)
  (k * n + j * m, j * n + m * k) ≃ _ := AA.substR (AA.substR AA.comm)
  (k * n + j * m, j * n + k * m) ≃ _ := AA.substR AA.comm
  (k * n + j * m, k * m + j * n) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b : Difference ℕ
⊢ a₁ ≃ a₂ → a₁ * b ≃ a₂ * b
Tactic:
revert a₁
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₂ b : Difference ℕ
⊢ ∀ {a₁ : Difference ℕ}, a₁ ≃ a₂ → a₁ * b ≃ a₂ * b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₂ b : Difference ℕ
⊢ ∀ {a₁ : Difference ℕ}, a₁ ≃ a₂ → a₁ * b ≃ a₂ * b
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₂ b : Difference ℕ
n m : ℕ
⊢ n——m ≃ a₂ → n——m * b ≃ a₂ * b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₂ b : Difference ℕ
n m : ℕ
⊢ n——m ≃ a₂ → n——m * b ≃ a₂ * b
Tactic:
revert a₂
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m : ℕ
⊢ ∀ {a₂ : Difference ℕ}, n——m ≃ a₂ → n——m * b ≃ a₂ * b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m : ℕ
⊢ ∀ {a₂ : Difference ℕ}, n——m ≃ a₂ → n——m * b ≃ a₂ * b
Tactic:
intro (k——j)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m k j : ℕ
⊢ n——m ≃ k——j → n——m * b ≃ k——j * b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m k j : ℕ
⊢ n——m ≃ k——j → n——m * b ≃ k——j * b
Tactic:
revert b
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ ∀ {b : Difference ℕ}, n——m ≃ k——j → n——m * b ≃ k——j * b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof 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)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
⊢ n——m ≃ k——j → n——m * p——q ≃ k——j * p——q
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof 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)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
⊢ n——m * p——q ≃ k——j * p——q
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_substL
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a b c : Difference ℕ
⊢ a * b * c ≃ a * (b * c)
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a * b * c ≃ a * (b * c)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a * b * c ≃ a * (b * c)
Tactic:
intro (q——p)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
q p : ℕ
⊢ q——p * b * c ≃ q——p * (b * c)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
q p : ℕ
⊢ q——p * b * c ≃ q——p * (b * c)
Tactic:
revert b
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p : ℕ
⊢ ∀ {b : Difference ℕ}, q——p * b * c ≃ q——p * (b * c)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p : ℕ
⊢ ∀ {b : Difference ℕ}, q——p * b * c ≃ q——p * (b * c)
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p n m : ℕ
⊢ q——p * n——m * c ≃ q——p * (n——m * c)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p n m : ℕ
⊢ q——p * n——m * c ≃ q——p * (n——m * c)
Tactic:
revert c
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
q p n m : ℕ
⊢ ∀ {c : Difference ℕ}, q——p * n——m * c ≃ q——p * (n——m * c)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
⊢ q——p * n——m * k——j ≃ q——p * (n——m * k——j)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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)
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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₁
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_assoc
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_identL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ 1 * a ≃ a
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, 1 * a ≃ a
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_identL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, 1 * a ≃ a
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 1 * n——m ≃ n——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_identL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 1 * n——m ≃ n——m
Tactic:
show 1——0 * n——m ≃ n——m
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 1——0 * n——m ≃ n——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_identL
Proof 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
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (1 * n + 0 * m)——(1 * m + 0 * n) ≃ n——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_identL
Proof 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)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ from_prod (1 * n + 0 * m, 1 * m + 0 * n) ≃ from_prod (n, m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_identL
Proof 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₁
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (1 * n + 0 * m, 1 * m + 0 * n) ≃ (n, m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_identL
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a b c : Difference ℕ
⊢ a * (b + c) ≃ a * b + a * c
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a * (b + c) ≃ a * b + a * c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a * (b + c) ≃ a * b + a * c
Tactic:
intro (q——p)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
q p : ℕ
⊢ q——p * (b + c) ≃ q——p * b + q——p * c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b c : Difference ℕ
q p : ℕ
⊢ q——p * (b + c) ≃ q——p * b + q——p * c
Tactic:
revert b
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p : ℕ
⊢ ∀ {b : Difference ℕ}, q——p * (b + c) ≃ q——p * b + q——p * c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p n m : ℕ
⊢ q——p * (n——m + c) ≃ q——p * n——m + q——p * c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
q p n m : ℕ
⊢ ∀ {c : Difference ℕ}, q——p * (n——m + c) ≃ q——p * n——m + q——p * c
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof 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
Proof 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