awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (hypothesis)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
⊢ HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
    HPow.hPow (β := ℕ) ε 2
have Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
Tactic: 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 _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
⊢ ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
have h : ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 =
  |HSub.hSub (α := ℝ) (∑ i ∈ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₁ ⊓ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2)|
Tactic: convert! H _ hs₂ _ has
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (hypothesis)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
⊢ ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 =
    |HSub.hSub (α := ℝ) (∑ i ∈ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₁ ⊓ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2)|
have this : s₁ ⊓ s₂ ⊆ s₂
Tactic: have : s₁ ⊓ s₂ ⊆ s₂ := Finset.inter_subset_right
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 =
    |HSub.hSub (α := ℝ) (∑ i ∈ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₁ ⊓ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2)|
have h : Eq (α := ℝ) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ i ∈ s₂ \ (s₁ ⊓ s₂), HPow.hPow (β := ℕ) ‖f i‖ 2)
Tactic: rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
h : Eq (α := ℝ) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ i ∈ s₂ \ (s₁ ⊓ s₂), HPow.hPow (β := ℕ) ‖f i‖ 2)
⊢ ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 =
    |HSub.hSub (α := ℝ) (∑ i ∈ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₁ ⊓ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2)|
have h₁ : ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2
Tactic: rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (hypothesis)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
⊢ HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
    HPow.hPow (β := ℕ) ε 2
have Hs₂ : ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
Tactic: 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 _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
Hs₂ : ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
⊢ HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
    HPow.hPow (β := ℕ) ε 2
have linarith : HPow.hPow (β := ℕ) ε 2 ≤
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
  1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
Hs₂ : ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
linarith :
  HPow.hPow (β := ℕ) ε 2 ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
⊢ HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
    HPow.hPow (β := ℕ) ε 2
have linarith₁ : HPow.hPow (β := ℕ) ε 2 ≤
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
  2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
Hs₂ : ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
linarith :
  HPow.hPow (β := ℕ) ε 2 ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁ :
  HPow.hPow (β := ℕ) ε 2 ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
    2 / 2 = 1
⊢ HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
    HPow.hPow (β := ℕ) ε 2
have linarith₂ : HPow.hPow (β := ℕ) ε 2 ≤
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
  HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
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
hf :
  ∀ ε > 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)| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n →
          |HSub.hSub (α := ℝ) (∑ i ∈ m, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ n, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
            HPow.hPow (β := ℕ) ε 2 / 2
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
has : a ≤ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
Hs₂ : ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2
linarith :
  HPow.hPow (β := ℕ) ε 2 ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁ :
  HPow.hPow (β := ℕ) ε 2 ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
    2 / 2 = 1
linarith₂ :
  HPow.hPow (β := ℕ) ε 2 ≤
      HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
    HMul.hMul (α := ℝ) 1 2 = 2
⊢ HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
    HPow.hPow (β := ℕ) ε 2
have linarith₃ : HPow.hPow (β := ℕ) ε 2 ≤
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) →
  GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
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
⊢ (Summable.{u_2, u_4} (α := E) fun (i : ι) ↦ (V i : (a : G i) → E) (f i)) ↔
    Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (β := ℕ) ‖f i‖ 2
have 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)| < ε
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
⊢ iSupIndep V
have h : Function.Injective (α := Π₀ (i : ι), ↥(V i)) (β := E)
  (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
        fun (i : ι) ↦ (V i).subtype) :
    (a : Π₀ (i : ι), ↥(V i)) → E)
Tactic: apply iSupIndep_of_dfinsupp_lsum_injective
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
⊢ Function.Injective (α := Π₀ (i : ι), ↥(V i)) (β := E)
    (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype) :
      (a : Π₀ (i : ι), ↥(V i)) → E)
have h : Eq (α := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
  (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
    ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
      fun (i : ι) ↦ (V i).subtype))
  ⊥
Tactic: refine LinearMap.ker_eq_bot.mp ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
⊢ Eq (α := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
        fun (i : ι) ↦ (V i).subtype))
    ⊥
have h : ∀ (x : Π₀ (i : ι), ↥(V i)),
  Membership.mem (γ := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
      (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
        ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype))
      x →
    x = 0
Tactic: rw [Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv :
  Membership.mem (γ := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
        fun (i : ι) ↦ (V i).subtype))
    v
⊢ v = 0
have hv₁ : Eq.{u_2 + 1} (α := E)
  (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype :
        (a : Π₀ (i : ι), ↥(V i)) → E)
      v :
    E)
  (0 : E)
Tactic: rw [LinearMap.mem_ker] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv :
  Eq.{u_2 + 1} (α := E)
    (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v :
      E)
    (0 : E)
⊢ v = 0
have h : ∀ (i : ι), (↑((v : (a : ι) → ↥(V a)) i) : E) = (↑(((0 : Π₀ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i) : E)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv :
  Eq.{u_2 + 1} (α := E)
    (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v :
      E)
    (0 : E)
i : ι
⊢ (↑((v : (a : ι) → ↥(V a)) i) : E) = (↑(((0 : Π₀ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i) : E)
have h : ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ = 0
Tactic: suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this