ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), ↑f c ≠ 0 → ↑(g c) (↑f c) ∈ s
⊢ (sum f fun x => ↑(g x)) ∈ s
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), ↑f c ≠ 0 → ↑(g c) (↑f c) ∈ s
⊢ ↑(sumAddHom g) f ∈ s
rw [Dfinsupp.sumAddHom_apply]