case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q✝ : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ sum ({ toFinsupp := toFinsupp✝ } + q) f = sum { toFinsupp := toFinsupp✝ } f + sum q f
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ sum (p + q) f = sum p f + sum q f
rcases p with ⟨⟩
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ sum ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) f =
    sum { toFinsupp := toFinsupp✝¹ } f + sum { toFinsupp := toFinsupp✝ } f
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q✝ : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ sum ({ toFinsupp := toFinsupp✝ } + q) f = sum { toFinsupp := toFinsupp✝ } f + sum q f
rcases q with ⟨⟩
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ sum { toFinsupp := toFinsupp✝¹ + toFinsupp✝ } f =
    sum { toFinsupp := toFinsupp✝¹ } f + sum { toFinsupp := toFinsupp✝ } f
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ sum ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) f =
    sum { toFinsupp := toFinsupp✝¹ } f + sum { toFinsupp := toFinsupp✝ } f
simp only [← ofFinsupp_add, Sum, support, coeff, Pi.add_apply, coe_add]
no goals
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ sum { toFinsupp := toFinsupp✝¹ + toFinsupp✝ } f =
    sum { toFinsupp := toFinsupp✝¹ } f + sum { toFinsupp := toFinsupp✝ } f
exact Finsupp.sum_add_index' hf h_add