awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n → ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ |HSub.hSub (α := ℝ) (∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2)| < ε
have h : HAdd.hAdd (α := ℝ) |∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2| |∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2| < ε
Tactic: refine (abs_sub _ _).trans_lt ?_
-- 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 (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n → ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
⊢ HAdd.hAdd (α := ℝ) |∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2| |∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2| < ε
have this : ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2
Tactic: have : ∀ i, 0 ≤ ‖f i‖ ^ 2 := 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 (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n → ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2
⊢ HAdd.hAdd (α := ℝ) |∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2| |∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2| < ε
have h : HAdd.hAdd (α := ℝ) (∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2) < ε
Tactic: simp only [Finset.abs_sum_of_nonneg' this]
-- 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 (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n → ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2
⊢ HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
    HPow.hPow (β := ℕ) (√ε) 2
have rw : ‖HSub.hSub (α := E) (∑ i ∈ s₁, (V i : (a : G i) → E) (f i)) (∑ i ∈ s₂, (V i : (a : G i) → E) (f i))‖ < √ε
Tactic: rw [← hV.norm_sq_diff_sum, sq_lt_sq, abs_of_nonneg (sqrt_nonneg _),
          abs_of_nonneg (norm_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 (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n → ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this : ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2) < ε
have this₁ : HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
  HPow.hPow (β := ℕ) (√ε) 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₂
-- 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 (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n → ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this_1 : ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2
this :
  HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
    HPow.hPow (β := ℕ) (√ε) 2
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2) < ε
have hη : HPow.hPow (β := ℕ) (√ε) 2 = ε
Tactic: have hη := sq_sqrt (le_of_lt hε)
-- 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 (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H :
  ∀ (m : Finset ι),
    a ≤ m →
      ∀ (n : Finset ι),
        a ≤ n → ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < √ε
s₁ : Finset ι
hs₁ : a ≤ s₁
s₂ : Finset ι
hs₂ : a ≤ s₂
this_1 : ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2
this :
  HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
    HPow.hPow (β := ℕ) (√ε) 2
hη : HPow.hPow (β := ℕ) (√ε) 2 = ε
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2) < ε
have linarith : ε ≤ HAdd.hAdd (α := ℝ) (∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2) →
  HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) -
          HPow.hPow (β := ℕ) (√ε) 2 +
        (HPow.hPow (β := ℕ) (√ε) 2 - ε) +
      (ε - HAdd.hAdd (α := ℝ) (∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2)) =
    0
Tactic: linarith
-- 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
⊢ ∃ (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))‖ < ε
have hε' : 0 < HPow.hPow (β := ℕ) ε 2 / 2
Tactic: have hε' : 0 < ε ^ 2 / 2 := half_pos (sq_pos_of_pos hε)
-- 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
⊢ ∃ (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))‖ < ε
have mpr : ∀ (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),
  ∃ (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))‖ < ε
Tactic: obtain ⟨a, H⟩ := hf _ hε'
-- 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
⊢ ∃ (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))‖ < ε
have h : ∀ (m : Finset ι),
  a ≤ m →
    ∀ (n : Finset ι),
      a ≤ n → ‖HSub.hSub (α := E) (∑ i ∈ m, (V i : (a : G i) → E) (f i)) (∑ i ∈ n, (V i : (a : G i) → E) (f i))‖ < ε
Tactic: use a
-- 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₂
⊢ ‖HSub.hSub (α := E) (∑ i ∈ s₁, (V i : (a : G i) → E) (f i)) (∑ i ∈ s₂, (V i : (a : G i) → E) (f i))‖ < ε
have h : HPow.hPow (β := ℕ) ‖HSub.hSub (α := E) (∑ i ∈ s₁, (V i : (a : G i) → E) (f i)) (∑ i ∈ s₂, (V i : (a : G i) → E) (f i))‖
    2 <
  HPow.hPow (β := ℕ) ε 2
Tactic: refine (abs_lt_of_sq_lt_sq' ?_ (le_of_lt hε)).2
-- 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₂
⊢ HPow.hPow (β := ℕ)
      ‖HSub.hSub (α := E) (∑ i ∈ s₁, (V i : (a : G i) → E) (f i)) (∑ i ∈ s₂, (V i : (a : G i) → E) (f i))‖ 2 <
    HPow.hPow (β := ℕ) ε 2
have has : a ≤ s₁ ⊓ s₂
Tactic: have has : a ≤ s₁ ⊓ s₂ := le_inf hs₁ hs₂
-- 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₂
⊢ HPow.hPow (β := ℕ)
      ‖HSub.hSub (α := E) (∑ i ∈ s₁, (V i : (a : G i) → E) (f i)) (∑ i ∈ s₂, (V i : (a : G i) → E) (f i))‖ 2 <
    HPow.hPow (β := ℕ) ε 2
have h : HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) <
  HPow.hPow (β := ℕ) ε 2
Tactic: rw [hV.norm_sq_diff_sum]
-- 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₂
⊢ ∑ 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₂
⊢ ∑ 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_left
-- 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₂
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₂
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']