awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
h₁ : ∀ (i : ι), 0 ≤ 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)|

Tactic:
rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']

Premises used: Finset.abs_sum_of_nonneg', add_tsub_cancel_right, Finset.sum_sdiff
-- 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
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₁
⊢ Eq (α := ℝ) (∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ i ∈ s₁ \ (s₁ ⊓ s₂), HPow.hPow (β := ℕ) ‖f i‖ 2)

Tactic:
simp
-- 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
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₁
⊢ ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2

Tactic:
fun i => sq_nonneg _

Premises used: Norm.norm, sq_nonneg
-- 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
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₁
⊢ ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2

Tactic:
exact fun i => sq_nonneg _

Premises used: sq_nonneg
-- 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
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

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 _
-- 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
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
⊢ |HSub.hSub (α := ℝ) (∑ i ∈ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₁ ⊓ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2)| <
    HPow.hPow (β := ℕ) ε 2 / 2

Tactic:
H _ hs₂ _ has
-- 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
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
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)|
⊢ ∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2 < HPow.hPow (β := ℕ) ε 2 / 2

Tactic:
convert! H _ hs₂ _ has
-- 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
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
⊢ s₁ ⊓ s₂ ⊆ s₂

Tactic:
have : s₁ ⊓ s₂ ⊆ s₂ := Finset.inter_subset_right
-- 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
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)
h₁ : ∀ (i : ι), 0 ≤ 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)|

Tactic:
rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']

Premises used: Finset.abs_sum_of_nonneg', add_tsub_cancel_right, Finset.sum_sdiff
-- 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
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₂
⊢ Eq (α := ℝ) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ i ∈ s₂ \ (s₁ ⊓ s₂), HPow.hPow (β := ℕ) ‖f i‖ 2)

Tactic:
simp
-- 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
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₂
⊢ ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2

Tactic:
fun i => sq_nonneg _

Premises used: Norm.norm, sq_nonneg
-- 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
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₂
⊢ ∀ (i : ι), 0 ≤ HPow.hPow (β := ℕ) ‖f i‖ 2

Tactic:
exact fun i => sq_nonneg _

Premises used: sq_nonneg
-- 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
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

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 _
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
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ₗᵢ
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)
⊢ iSupIndep V

Tactic:
apply iSupIndep_of_dfinsupp_lsum_injective

Premises used: iSupIndep_of_dfinsupp_lsum_injective
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
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)

Tactic:
LinearMap.ker_eq_bot.mp ?_

Premises used: LinearMap.ker_eq_bot, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
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ₗᵢ
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))
    ⊥
⊢ 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:
refine LinearMap.ker_eq_bot.mp ?_

Premises used: LinearMap.ker_eq_bot, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
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ₗᵢ
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
⊢ 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:
rw [Submodule.eq_bot_iff]

Premises used: Submodule.eq_bot_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
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
⊢ 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

Premises used: LinearMap.mem_ker
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
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)
h : ∀ (i : ι), (↑((v : (a : ι) → ↥(V a)) i) : E) = (↑(((0 : Π₀ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i) : E)
⊢ v = 0

Tactic:
ext i
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
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 : ι
this : ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ = 0
⊢ (↑((v : (a : ι) → ↥(V a)) i) : E) = (↑(((0 : Π₀ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i) : E)

Tactic:
simpa only [inner_self_eq_zero] using this

Premises used: inner_self_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
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 : ι
h : ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ = 0
⊢ (↑((v : (a : ι) → ↥(V a)) i) : E) = (↑(((0 : Π₀ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i) : E)

Tactic:
suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this