case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_4
β : Type u_3
s : SummableFamily Γ R α
f : α ↪ β
a : α
b : β
g : Γ
⊢ coeff (hsum (embDomain s f)) g = coeff (hsum s) g
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_4
β : Type u_3
s : SummableFamily Γ R α
f : α ↪ β
a : α
b : β
⊢ hsum (embDomain s f) = hsum s
ext g
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_4
β : Type u_3
s : SummableFamily Γ R α
f : α ↪ β
a : α
b : β
g : Γ
⊢ (∑ᶠ (i : β), if h : i ∈ Set.range ↑f then coeff (toFun s (Classical.choose (_ : i ∈ Set.range ↑f))) g else 0) =
    ∑ᶠ (i : α), coeff (toFun s i) g
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_4
β : Type u_3
s : SummableFamily Γ R α
f : α ↪ β
a : α
b : β
g : Γ
⊢ coeff (hsum (embDomain s f)) g = coeff (hsum s) g
simp only [hsum_coeff, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, zero_coeff]
no goals
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_4
β : Type u_3
s : SummableFamily Γ R α
f : α ↪ β
a : α
b : β
g : Γ
⊢ (∑ᶠ (i : β), if h : i ∈ Set.range ↑f then coeff (toFun s (Classical.choose (_ : i ∈ Set.range ↑f))) g else 0) =
    ∑ᶠ (i : α), coeff (toFun s i) g
exact finsum_emb_domain f fun a => (s a).coeff g