no goals
ι : Type u_5
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
x : M
⊢ HasSum (fun b => ↑e (f b)) (↑e x) ↔ HasSum f x
rw [e.hasSum, ContinuousLinearEquiv.symm_apply_apply]