-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : CompleteSpace E
f : (i : ι) → G i
simp :
  (∀ ε > 0,
      ∃ (N : Finset ι),
        ∀ (m : Finset ι),
          N ≤ m →
            ∀ (n : Finset ι),
              N ≤ n →
                ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ <
                  ε) ↔
    ∀ ε > 0,
      ∃ (N : Finset ι),
        ∀ (m : Finset ι),
          N ≤ m →
            ∀ (n : Finset ι),
              N ≤ n →
                |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| < ε
mp :
  (∀ ε > 0,
      ∃ (N : Finset ι),
        ∀ (m : Finset ι),
          N ≤ m →
            ∀ (n : Finset ι),
              N ≤ n →
                ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ <
                  ε) →
    ∀ ε > 0,
      ∃ (N : Finset ι),
        ∀ (m : Finset ι),
          N ≤ m →
            ∀ (n : Finset ι),
              N ≤ n →
                |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| < ε
mpr mpr₁ :
  (∀ ε > 0,
      ∃ (N : Finset ι),
        ∀ (m : Finset ι),
          N ≤ m →
            ∀ (n : Finset ι),
              N ≤ n →
                |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| < ε) →
    ∀ ε > 0,
      ∃ (N : Finset ι),
        ∀ (m : Finset ι),
          N ≤ m →
            ∀ (n : Finset ι),
              N ≤ n →
                ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < ε
⊢ (Summable.{u_2, u_4} (α := E) fun (i : ι) ↦ (V i : (a : G i) → E) (f i)) ↔
    Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖f i‖ 2

Tactic:
classical
    simp only [summable_iff_cauchySeq_finset, NormedAddCommGroup.cauchySeq_iff, norm_neg_add,
      Real.norm_eq_abs]
    constructor
    · intro hf ε hε
      obtain ⟨a, H⟩ := hf _ (sqrt_pos.mpr hε)
      use a
      intro s₁ hs₁ s₂ hs₂
      rw [← Finset.sum_sdiff_sub_sum_sdiff]
      refine (abs_sub _ _).trans_lt ?_
      have : ∀ i, 0 ≤ ‖f i‖ ^ 2 := fun i : ι => sq_nonneg _
      simp only [Finset.abs_sum_of_nonneg' this]
      have : ((∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2) + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2) < √ε ^ 2 := by
        rw [← hV.norm_sq_diff_sum, sq_lt_sq, abs_of_nonneg (sqrt_nonneg _),
          abs_of_nonneg (norm_nonneg _)]
        exact H s₁ hs₁ s₂ hs₂
      have hη := sq_sqrt (le_of_lt hε)
      linarith
    · intro hf ε hε
      have hε' : 0 < ε ^ 2 / 2 := half_pos (sq_pos_of_pos hε)
      obtain ⟨a, H⟩ := hf _ hε'
      use a
      intro s₁ hs₁ s₂ hs₂
      refine (abs_lt_of_sq_lt_sq' ?_ (le_of_lt hε)).2
      have has : a ≤ s₁ ⊓ s₂ := le_inf hs₁ hs₂
      rw [hV.norm_sq_diff_sum]
      have Hs₁ : ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2 := by
        convert! H _ hs₁ _ has
        have : s₁ ⊓ s₂ ⊆ s₁ := Finset.inter_subset_left
        rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']
        · simp
        · exact fun i => sq_nonneg _
      have Hs₂ : ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 < ε ^ 2 / 2 := by
        convert! H _ hs₂ _ has
        have : s₁ ⊓ s₂ ⊆ s₂ := Finset.inter_subset_right
        rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']
        · simp
        · exact fun i => sq_nonneg _
      linarith

Premises used: abs_sub, NormedAddCommGroup.cauchySeq_iff, norm_neg_add, Finset.sum_sdiff_sub_sum_sdiff, summable_iff_cauchySeq_finset, LE.le.trans_lt, Real.norm_eq_abs