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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x))‖
      2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
have hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
Tactic: have hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i := fun i hi => if_pos (Finset.sdiff_subset hi)
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x))‖
      2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
have hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
Tactic: have hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i := fun i hi => if_neg (Finset.mem_sdiff.mp hi).2
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
i : ι
⊢ ‖if i ∈ s₁ then f i else -f i‖ = ‖f i‖
have pos : i ∈ s₁ → ‖f i‖ = ‖f i‖
Tactic: split_ifs
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
i : ι
pos : i ∈ s₁ → ‖f i‖ = ‖f i‖
⊢ ‖if i ∈ s₁ then f i else -f i‖ = ‖f i‖
have neg : i ∉ s₁ → ‖-f i‖ = ‖f i‖
Tactic: split_ifs
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x))‖
      2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
have hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
Tactic: have hF : ∀ i, ‖F i‖ = ‖f i‖ := by
    intro i
    dsimp only [F]
    split_ifs <;> simp only [norm_neg]
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))‖ 2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖F i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖F i‖ 2)
have hs : Disjoint (s₁ \ s₂) (s₂ \ s₁)
Tactic: have hs : Disjoint (s₁ \ s₂) (s₂ \ s₁) := disjoint_sdiff_sdiff
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x))‖
      2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
have this : HPow.hPow (β := ℕ)
    ‖HAdd.hAdd (α := E) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))‖ 2 =
  HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖F i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖F i‖ 2)
Tactic: have :
    ‖(∑ i ∈ s₁ \ s₂, V i (F i)) + ∑ i ∈ s₂ \ s₁, V i (F i)‖ ^ 2 =
      (∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2) + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2 := by
    have hs : Disjoint (s₁ \ s₂) (s₂ \ s₁) := disjoint_sdiff_sdiff
    simpa only [Finset.sum_union hs] using hV.norm_sum F (s₁ \ s₂ ∪ s₂ \ s₁)
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))‖ 2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖F i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖F i‖ 2)
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x))‖
      2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
have h : Eq.{u_2 + 1} (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i))
Tactic: convert! this using 4
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))‖ 2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖F i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖F i‖ 2)
h : Eq.{u_2 + 1} (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i))
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x))‖
      2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
have h₁ : Eq.{u_2 + 1} (α := E) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))
Tactic: convert! this using 4
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))‖ 2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖F i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖F i‖ 2)
h : Eq.{u_2 + 1} (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i))
h₁ : Eq.{u_2 + 1} (α := E) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x))‖
      2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
have h₂ : ∀ x ∈ s₁ \ s₂, ‖f x‖ = ‖F x‖
Tactic: convert! this using 4
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))‖ 2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖F i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖F i‖ 2)
h : Eq.{u_2 + 1} (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i))
h₁ : Eq.{u_2 + 1} (α := E) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))
h₂ : ∀ x ∈ s₁ \ s₂, ‖f x‖ = ‖F x‖
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x))‖
      2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
have h₃ : ∀ x ∈ s₂ \ s₁, ‖f x‖ = ‖F x‖
Tactic: convert! this using 4
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))‖ 2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖F i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖F i‖ 2)
⊢ Eq.{u_2 + 1} (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i))
have h : ∀ (i : ι) (hi : i ∈ s₁ \ s₂), Eq.{u_2 + 1} (α := E) ((V i : (a : G i) → E) (f i) : E) ((V i : (a : G i) → E) (F i) : E)
Tactic: refine Finset.sum_congr rfl fun i hi => ?_
-- 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 : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ i ∈ s₁ \ s₂, (V i : (a : G i) → E) (F i)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))‖ 2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖F i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖F i‖ 2)
⊢ Eq.{u_2 + 1} (α := E) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x)) (∑ i ∈ s₂ \ s₁, (V i : (a : G i) → E) (F i))
have h : ∀ (i : ι) (hi : i ∈ s₂ \ s₁), Eq.{u_2 + 1} (α := E) (-(V i : (a : G i) → E) (f i) : E) ((V i : (a : G i) → E) (F i) : E)
Tactic: refine Finset.sum_congr rfl fun i hi => ?_
-- 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: simp only [summable_iff_cauchySeq_finset, NormedAddCommGroup.cauchySeq_iff, norm_neg_add,
      Real.norm_eq_abs]
-- 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
⊢ (∀ ε > 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)| < ε
have 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)| < ε
Tactic: constructor
-- 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
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)| < ε
⊢ (∀ ε > 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)| < ε
have 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))‖ < ε
Tactic: constructor
-- 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
⊢ ∃ (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)| < ε
have mp : ∀ (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))‖ < √ε),
  ∃ (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: obtain ⟨a, H⟩ := hf _ (sqrt_pos.mpr 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))‖ < √ε
⊢ ∃ (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)| < ε
have 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)| < ε
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 (α := 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 (α := ℝ) (∑ i ∈ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2)| < ε
have h : |HSub.hSub (α := ℝ) (∑ x ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f x‖ 2) (∑ x ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f x‖ 2)| < ε
Tactic: rw [← Finset.sum_sdiff_sub_sum_sdiff]