intros n r1 r2
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 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
n : ℕ
r1 r2 : R
⊢ (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) ((r1 + r2) * (↑φ)^[n] b₂)) =
    (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r1 * (↑φ)^[n] b₂)) +
      sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r2 * (↑φ)^[n] b₂)