α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.59444
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : γ → α
e : ↑(support f) ≃ ↑(support g)
he : ∀ (x : ↑(support f)), g ↑(↑e x) = f ↑x
this : (g ∘ Subtype.val) ∘ ↑e = f ∘ Subtype.val
⊢ HasSum f a ↔ HasSum g a
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.59444
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : γ → α
e : ↑(support f) ≃ ↑(support g)
he : ∀ (x : ↑(support f)), g ↑(↑e x) = f ↑x
⊢ HasSum f a ↔ HasSum g a
have : (g ∘ (↑)) ∘ e = f ∘ (↑) := funext he
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.59444
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : γ → α
e : ↑(support f) ≃ ↑(support g)
he : ∀ (x : ↑(support f)), g ↑(↑e x) = f ↑x
this : (g ∘ Subtype.val) ∘ ↑e = f ∘ Subtype.val
⊢ HasSum f a ↔ HasSum g a
rw [← hasSum_subtype_support, ← this, e.hasSum_iff, hasSum_subtype_support]