α : Type u_4
β : Type u_5
γ : Type u_1
δ : Type ?u.160302
inst✝⁵ : AddCommMonoid α
inst✝⁴ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
inst✝³ : AddCommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_2
G' : Type u_3
inst✝¹ : AddMonoidHomClass G α γ
inst✝ : AddMonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous ↑g
hg' : Continuous ↑g'
hinv : LeftInverse ↑g' ↑g
h : Summable (↑g ∘ f)
this : Summable (↑g' ∘ ↑g ∘ f)
⊢ Summable f
α : Type u_4
β : Type u_5
γ : Type u_1
δ : Type ?u.160302
inst✝⁵ : AddCommMonoid α
inst✝⁴ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
inst✝³ : AddCommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_2
G' : Type u_3
inst✝¹ : AddMonoidHomClass G α γ
inst✝ : AddMonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous ↑g
hg' : Continuous ↑g'
hinv : LeftInverse ↑g' ↑g
h : Summable (↑g ∘ f)
⊢ Summable f
have := h.map _ hg'
no goals
α : Type u_4
β : Type u_5
γ : Type u_1
δ : Type ?u.160302
inst✝⁵ : AddCommMonoid α
inst✝⁴ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
inst✝³ : AddCommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_2
G' : Type u_3
inst✝¹ : AddMonoidHomClass G α γ
inst✝ : AddMonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous ↑g
hg' : Continuous ↑g'
hinv : LeftInverse ↑g' ↑g
h : Summable (↑g ∘ f)
this : Summable (↑g' ∘ ↑g ∘ f)
⊢ Summable f
rwa [← Function.comp.assoc, hinv.id] at this