α : Type u_2
β : Type u_1
γ : Type ?u.35832
δ : Type ?u.35835
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b : α
s✝ : Finset β
s : Set β
hs : Set.Finite s
f : β → α
this : Summable (f ∘ Subtype.val)
⊢ Summable (f ∘ Subtype.val)
α : Type u_2
β : Type u_1
γ : Type ?u.35832
δ : Type ?u.35835
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b : α
s✝ : Finset β
s : Set β
hs : Set.Finite s
f : β → α
⊢ Summable (f ∘ Subtype.val)
have := hs.toFinset.summable f
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.35832
δ : Type ?u.35835
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b : α
s✝ : Finset β
s : Set β
hs : Set.Finite s
f : β → α
this : Summable (f ∘ Subtype.val)
⊢ Summable (f ∘ Subtype.val)
rwa [hs.coe_toFinset] at this