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

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)
case e_g
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (fun a b_1 =>
      sum (sum b.toFinsupp fun a₂ b₂ => single (a + a₂) (b_1 * (↑φ)^[a] b₂)) fun a₁ b₁ =>
        sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    fun a₁ b₁ =>
    sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
      single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)

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)