case pos
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f
⊢ (∑' (z : ι), ↑e (f z)) = y ↔ (∑' (z : ι), f z) = ↑(ContinuousLinearEquiv.symm e) y

case neg
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
⊢ (∑' (z : ι), ↑e (f z)) = y ↔ (∑' (z : ι), f z) = ↑(ContinuousLinearEquiv.symm e) y
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
⊢ (∑' (z : ι), ↑e (f z)) = y ↔ (∑' (z : ι), f z) = ↑(ContinuousLinearEquiv.symm e) y
by_cases hf : Summable f
no goals
case pos
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f
⊢ (∑' (z : ι), ↑e (f z)) = y ↔ (∑' (z : ι), f z) = ↑(ContinuousLinearEquiv.symm e) y
exact
  ⟨fun h => (e.hasSum.mp ((e.summable.mpr hf).hasSum_iff.mpr h)).tsum_eq, fun h =>
    (e.hasSum.mpr (hf.hasSum_iff.mpr h)).tsum_eq⟩
case neg
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ (∑' (z : ι), ↑e (f z)) = y ↔ (∑' (z : ι), f z) = ↑(ContinuousLinearEquiv.symm e) y
case neg
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
⊢ (∑' (z : ι), ↑e (f z)) = y ↔ (∑' (z : ι), f z) = ↑(ContinuousLinearEquiv.symm e) y
have hf' : ¬Summable fun z => e (f z) := fun h => hf (e.summable.mp h)
case neg
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = y ↔ 0 = ↑(ContinuousLinearEquiv.symm e) y
case neg
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ (∑' (z : ι), ↑e (f z)) = y ↔ (∑' (z : ι), f z) = ↑(ContinuousLinearEquiv.symm e) y
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hf']
case neg.refine_1
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = y → 0 = ↑(ContinuousLinearEquiv.symm e) y

case neg.refine_2
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
H : 0 = ↑(ContinuousLinearEquiv.symm e) y
⊢ 0 = y
case neg
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = y ↔ 0 = ↑(ContinuousLinearEquiv.symm e) y
refine ⟨?_, fun H => ?_⟩
case neg.refine_1
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = ↑(ContinuousLinearEquiv.symm e) 0
case neg.refine_1
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = y → 0 = ↑(ContinuousLinearEquiv.symm e) y
rintro rfl
no goals
case neg.refine_1
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = ↑(ContinuousLinearEquiv.symm e) 0
simp
no goals
case neg.refine_2
ι : Type u_5
R : Type u_3
R₂ : Type u_4
M : Type u_1
M₂ : Type u_2
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 σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
H : 0 = ↑(ContinuousLinearEquiv.symm e) y
⊢ 0 = y
simpa using congr_arg (fun z => e z) H