case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s t : SummableFamily Γ R α
g : Γ
⊢ coeff (hsum (s + t)) g = coeff (hsum s + hsum t) g
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s t : SummableFamily Γ R α
⊢ hsum (s + t) = hsum s + hsum t
ext g
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s t : SummableFamily Γ R α
g : Γ
⊢ (∑ᶠ (i : α), coeff (toFun s i) g + coeff (toFun t i) g) =
    (∑ᶠ (i : α), coeff (toFun s i) g) + ∑ᶠ (i : α), coeff (toFun t i) g
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s t : SummableFamily Γ R α
g : Γ
⊢ coeff (hsum (s + t)) g = coeff (hsum s + hsum t) g
simp only [hsum_coeff, add_coeff, add_apply]
no goals
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_3
s t : SummableFamily Γ R α
g : Γ
⊢ (∑ᶠ (i : α), coeff (toFun s i) g + coeff (toFun t i) g) =
    (∑ᶠ (i : α), coeff (toFun s i) g) + ∑ᶠ (i : α), coeff (toFun t i) g
exact finsum_add_distrib (s.finite_co_support _) (t.finite_co_support _)