α : Type u_4
ι : Type ?u.303409
γ : Type ?u.303412
A : Type ?u.303415
B : Type ?u.303418
C : Type ?u.303421
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_1
M : Type u_2
M' : Type ?u.306557
N : Type u_3
P : Type ?u.306563
G : Type ?u.306566
H : Type ?u.306569
R : Type ?u.306572
S : Type ?u.306575
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
this : ∀ (c : β), (sum f fun a b => ↑(g a b) c) ≠ 0 → ∃ a, ↑f a ≠ 0 ∧ ¬↑(g a (↑f a)) c = 0
⊢ (sum f g).support ⊆ Finset.biUnion f.support fun a => (g a (↑f a)).support
α : Type u_4
ι : Type ?u.303409
γ : Type ?u.303412
A : Type ?u.303415
B : Type ?u.303418
C : Type ?u.303421
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_1
M : Type u_2
M' : Type ?u.306557
N : Type u_3
P : Type ?u.306563
G : Type ?u.306566
H : Type ?u.306569
R : Type ?u.306572
S : Type ?u.306575
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
⊢ (sum f g).support ⊆ Finset.biUnion f.support fun a => (g a (↑f a)).support
have : ∀ c, (f.sum fun a b => g a b c) ≠ 0 → ∃ a, f a ≠ 0 ∧ ¬(g a (f a)) c = 0 := fun a₁ h =>
  let ⟨a, ha, ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
  ⟨a, mem_support_iff.mp ha, ne⟩
no goals
α : Type u_4
ι : Type ?u.303409
γ : Type ?u.303412
A : Type ?u.303415
B : Type ?u.303418
C : Type ?u.303421
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_1
M : Type u_2
M' : Type ?u.306557
N : Type u_3
P : Type ?u.306563
G : Type ?u.306566
H : Type ?u.306569
R : Type ?u.306572
S : Type ?u.306575
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
this : ∀ (c : β), (sum f fun a b => ↑(g a b) c) ≠ 0 → ∃ a, ↑f a ≠ 0 ∧ ¬↑(g a (↑f a)) c = 0
⊢ (sum f g).support ⊆ Finset.biUnion f.support fun a => (g a (↑f a)).support
simpa only [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply, exists_prop]