ι : Type u
γ : Type w
β : ι → Type v
β₁✝ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
this : ∀ (i₁ : ι), (sum f fun i b => ↑(g i b) i₁) ≠ 0 → ∃ i, ↑f i ≠ 0 ∧ ¬↑(g i (↑f i)) i₁ = 0
⊢ support (sum f g) ⊆ Finset.biUnion (support f) fun i => support (g i (↑f i))
ι : Type u
γ : Type w
β : ι → Type v
β₁✝ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
⊢ support (sum f g) ⊆ Finset.biUnion (support f) fun i => support (g i (↑f i))
have :
  ∀ i₁ : ι,
    (f.sum fun (i : ι₁) (b : β₁ i) => (g i b) i₁) ≠ 0 → ∃ i : ι₁, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0 :=
  fun i₁ h =>
  let ⟨i, hi, Ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
  ⟨i, mem_support_iff.1 hi, Ne⟩
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁✝ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
this : ∀ (i₁ : ι), (sum f fun i b => ↑(g i b) i₁) ≠ 0 → ∃ i, ↑f i ≠ 0 ∧ ¬↑(g i (↑f i)) i₁ = 0
⊢ support (sum f g) ⊆ Finset.biUnion (support f) fun i => support (g i (↑f i))
simpa [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply] using this