Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h.e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
a₃ : ℕ
b₃ : R
⊢ single (a₁ + a₂ + a₃) (b₁ * (↑φ)^[a₁] b₂ * (↑φ)^[a₁ + a₂] b₃) =
    sum (single (a₂ + a₃) (b₂ * (↑φ)^[a₂] b₃)) fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)

case e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ (sum c.toFinsupp fun a₂_1 b₂ => single (a₁ + a₂ + a₂_1) (0 * (↑φ)^[a₁ + a₂] b₂)) = 0

case e_g.h.h.e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ) (b₁_1 b₂ : R),
    single (a₁ + a) (b₁ * (↑φ)^[a₁] (b₁_1 + b₂)) =
      single (a₁ + a) (b₁ * (↑φ)^[a₁] b₁_1) + single (a₁ + a) (b₁ * (↑φ)^[a₁] b₂)

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ) (b₁_1 b₂ : R),
    single (a₁ + a) (b₁ * (↑φ)^[a₁] (b₁_1 + b₂)) =
      single (a₁ + a) (b₁ * (↑φ)^[a₁] b₁_1) + single (a₁ + a) (b₁ * (↑φ)^[a₁] b₂)

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Tactic:
rw [AddMonoidAlgebra.sum_single_index, _root_.mul_assoc, RingHom.iterate_map_mul,
  ← Function.iterate_add_apply, add_assoc]
Proof state after:
case e_g.h.h.e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
a₃ : ℕ
b₃ : R
⊢ single (a₁ + (a₂ + a₃)) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ (sum c.toFinsupp fun a₂_1 b₂ => single (a₁ + a₂ + a₂_1) (0 * (↑φ)^[a₁ + a₂] b₂)) = 0

case e_g.h.h.e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ) (b₁_1 b₂ : R),
    single (a₁ + a) (b₁ * (↑φ)^[a₁] (b₁_1 + b₂)) =
      single (a₁ + a) (b₁ * (↑φ)^[a₁] b₁_1) + single (a₁ + a) (b₁ * (↑φ)^[a₁] b₂)

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ) (b₁_1 b₂ : R),
    single (a₁ + a) (b₁ * (↑φ)^[a₁] (b₁_1 + b₂)) =
      single (a₁ + a) (b₁ * (↑φ)^[a₁] b₁_1) + single (a₁ + a) (b₁ * (↑φ)^[a₁] b₂)

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)