-- Mathlib/Analysis/InnerProductSpace/Subspace.lean
theorem OrthogonalFamily.summable_iff_norm_sq_summable [CompleteSpace E] (f : ∀ i, G i) :
    (Summable fun i => V i (f i)) ↔ Summable fun i => ‖f i‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
⊢ ‖∑ i ∈ s₁, (V i) (f i) - ∑ i ∈ s₂, (V i) (f i)‖ < √ε

Tactic:
exact H s₁ hs₁ s₂ hs₂

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (∀ ε > 0,
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε) ↔
    ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (∀ ε > 0,
      ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε) →
    ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
⊢ (∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε) →
    ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
⊢ ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 < ε

Tactic:
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₂

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this✝ : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
this : ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2 < √ε ^ 2
⊢ ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 < ε

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this✝ : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
this : ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2 < √ε ^ 2
⊢ ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 < ε

Tactic:
have hη := sq_sqrt (le_of_lt hε)

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this✝ : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
this : ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2 < √ε ^ 2
hη : √ε ^ 2 = ε
⊢ ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 < ε

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε

Tactic:
obtain ⟨a, H⟩ := hf _ (sqrt_pos.mpr hε)

Result:
case mp.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ≤ m → ∀ (n : Finset ι), a ≤ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < √ε
⊢ ∃ N, ∀ (m : Finset ι), N ≤ m → ∀ (n : Finset ι), N ≤ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε