Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s : SummableFamily Γ R α
g : Γ
hg :
  ∑ i in Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g)), coeff (toFun s i) g ≠ 0
⊢ g ∈ ⋃ (a : α), support (toFun s a)
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s : SummableFamily Γ R α
g : Γ
hg : g ∈ support (hsum s)
⊢ g ∈ ⋃ (a : α), support (toFun s a)
rw [mem_support, hsum_coeff, finsum_eq_sum _ (s.finite_co_support _)] at hg
case intro.intro
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s : SummableFamily Γ R α
g : Γ
hg :
  ∑ i in Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g)), coeff (toFun s i) g ≠ 0
a : α
left✝ : a ∈ Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g))
h2 : coeff (toFun s a) g ≠ 0
⊢ g ∈ ⋃ (a : α), support (toFun s a)
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s : SummableFamily Γ R α
g : Γ
hg :
  ∑ i in Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g)), coeff (toFun s i) g ≠ 0
⊢ g ∈ ⋃ (a : α), support (toFun s a)
obtain ⟨a, _, h2⟩ := exists_ne_zero_of_sum_ne_zero hg
case intro.intro
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s : SummableFamily Γ R α
g : Γ
hg :
  ∑ i in Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g)), coeff (toFun s i) g ≠ 0
a : α
left✝ : a ∈ Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g))
h2 : coeff (toFun s a) g ≠ 0
⊢ ∃ i, g ∈ support (toFun s i)
case intro.intro
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s : SummableFamily Γ R α
g : Γ
hg :
  ∑ i in Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g)), coeff (toFun s i) g ≠ 0
a : α
left✝ : a ∈ Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g))
h2 : coeff (toFun s a) g ≠ 0
⊢ g ∈ ⋃ (a : α), support (toFun s a)
rw [Set.mem_iUnion]
no goals
case intro.intro
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s : SummableFamily Γ R α
g : Γ
hg :
  ∑ i in Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g)), coeff (toFun s i) g ≠ 0
a : α
left✝ : a ∈ Set.Finite.toFinset (_ : Set.Finite (Function.support fun a => coeff (toFun s a) g))
h2 : coeff (toFun s a) g ≠ 0
⊢ ∃ i, g ∈ support (toFun s i)
exact ⟨a, h2⟩