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
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ j ∈ s,
      ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E))
    (∑ j ∈ s,
      ∑ i ∈ s,
        if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
        else 0)
have e_f : ∀ (i : ι),
  Eq.{u_1 + 1} (α := 𝕜)
    (∑ i_1 ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i_1 : (a : G i_1) → E) (l₁ i_1) : E) ((V i : (a : G i) → E) (l₂ i) : E))
    (∑ i_1 ∈ s,
      if i_1 = i then
        inner.{u_1, u_2} 𝕜 (E := E) ((V i_1 : (a : G i_1) → E) (l₁ i_1) : E) ((V i : (a : G i) → E) (l₂ i) : E)
      else 0)
Tactic: congr with i
-- 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
l₁ l₂ : (i : ι) → G i
s : Finset ι
i : ι
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ i_1 ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i_1 : (a : G i_1) → E) (l₁ i_1) : E) ((V i : (a : G i) → E) (l₂ i) : E))
    (∑ i_1 ∈ s,
      if i_1 = i then
        inner.{u_1, u_2} 𝕜 (E := E) ((V i_1 : (a : G i_1) → E) (l₁ i_1) : E) ((V i : (a : G i) → E) (l₂ i) : E)
      else 0)
have e_f : ∀ (j : ι),
  inner.{u_1, u_2} 𝕜 (E := E) ((V j : (a : G j) → E) (l₁ j) : E) ((V i : (a : G i) → E) (l₂ i) : E) =
    if j = i then inner.{u_1, u_2} 𝕜 (E := E) ((V j : (a : G j) → E) (l₁ j) : E) ((V i : (a : G i) → E) (l₂ i) : E)
    else 0
Tactic: congr with j
-- 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
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ i ∈ s, ⟪l₁ i, l₂ i⟫
have i : inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
  ∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
Tactic: calc
    ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
      simp only [sum_inner, inner_sum]
    _ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 := by
      congr with i
      congr with j
      apply hV.eq_ite
    _ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
      simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
        imp_self, imp_true_iff]
-- 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
l₁ l₂ : (i : ι) → G i
s : Finset ι
i :
  inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ i ∈ s, ⟪l₁ i, l₂ i⟫
have i₁ : Eq.{u_1 + 1} (α := 𝕜)
  (∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E))
  (∑ j ∈ s,
    ∑ i ∈ s,
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
      else 0)
Tactic: calc
    ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
      simp only [sum_inner, inner_sum]
    _ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 := by
      congr with i
      congr with j
      apply hV.eq_ite
    _ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
      simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
        imp_self, imp_true_iff]
-- 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
l₁ l₂ : (i : ι) → G i
s : Finset ι
i :
  inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
i₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    (∑ j ∈ s,
      ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E))
    (∑ j ∈ s,
      ∑ i ∈ s,
        if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
        else 0)
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ i ∈ s, ⟪l₁ i, l₂ i⟫
have i₂ : Eq.{u_1 + 1} (α := 𝕜)
  (∑ j ∈ s,
    ∑ i ∈ s,
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
      else 0)
  (∑ i ∈ s, ⟪l₁ i, l₂ i⟫)
Tactic: calc
    ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
      simp only [sum_inner, inner_sum]
    _ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 := by
      congr with i
      congr with j
      apply hV.eq_ite
    _ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
      simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
        imp_self, imp_true_iff]
-- 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
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ i ∈ s, ⟪l₁ i, l₂ i⟫
have i : inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
  ∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
Tactic: classical
  calc
    ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
      simp only [sum_inner, inner_sum]
    _ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 := by
      congr with i
      congr with j
      apply hV.eq_ite
    _ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
      simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
        imp_self, imp_true_iff]
-- 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
l₁ l₂ : (i : ι) → G i
s : Finset ι
i :
  inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ i ∈ s, ⟪l₁ i, l₂ i⟫
have i₁ : Eq.{u_1 + 1} (α := 𝕜)
  (∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E))
  (∑ j ∈ s,
    ∑ i ∈ s,
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
      else 0)
Tactic: classical
  calc
    ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
      simp only [sum_inner, inner_sum]
    _ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 := by
      congr with i
      congr with j
      apply hV.eq_ite
    _ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
      simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
        imp_self, imp_true_iff]
-- 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
l₁ l₂ : (i : ι) → G i
s : Finset ι
i :
  inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
i₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    (∑ j ∈ s,
      ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E))
    (∑ j ∈ s,
      ∑ i ∈ s,
        if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
        else 0)
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ i ∈ s, ⟪l₁ i, l₂ i⟫
have i₂ : Eq.{u_1 + 1} (α := 𝕜)
  (∑ j ∈ s,
    ∑ i ∈ s,
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
      else 0)
  (∑ i ∈ s, ⟪l₁ i, l₂ i⟫)
Tactic: classical
  calc
    ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
      simp only [sum_inner, inner_sum]
    _ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 := by
      congr with i
      congr with j
      apply hV.eq_ite
    _ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
      simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
        imp_self, imp_true_iff]
-- 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
l : (i : ι) → G i
s : Finset ι
⊢ HPow.hPow (β := ℕ) (Norm.norm.{u_2} (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l i))) 2 =
    ∑ i ∈ s, HPow.hPow (β := ℕ) ‖l i‖ 2
have this : HPow.hPow (α := 𝕜) (β := ℕ) (↑(Norm.norm.{u_2} (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l i))) : 𝕜) 2 =
  ∑ i ∈ s, HPow.hPow (α := 𝕜) (β := ℕ) (↑‖l i‖ : 𝕜) 2
Tactic: have : ((‖∑ i ∈ s, V i (l i)‖ : ℝ) : 𝕜) ^ 2 = ∑ i ∈ s, ((‖l i‖ : ℝ) : 𝕜) ^ 2 := by
    simp only [← inner_self_eq_norm_sq_to_K, hV.inner_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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
⊢ Orthonormal 𝕜 (E := E) fun (a : (i : ι) × α i) ↦
    (V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
      (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i)))
have left : ∀ (i : (i : ι) × α i),
  Norm.norm.{u_2} (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        i) =
    1
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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
left :
  ∀ (i : (i : ι) × α i),
    Norm.norm.{u_2} (E := E)
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          i) =
      1
⊢ Orthonormal 𝕜 (E := E) fun (a : (i : ι) × α i) ↦
    (V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
      (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i)))
have right : Pairwise fun (i j : (i : ι) × α i) ↦
  inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        i)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        j) =
    0
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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) j w
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
    0
have pos : ∀ (hij : i = j),
  inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
    0
Tactic: by_cases hij : i = j
-- 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) j w
pos :
  ∀ (hij : i = j),
    inner.{u_1, u_2} 𝕜 (E := E)
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
      0
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
    0
have neg : ∀ (hij : ¬i = j),
  inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
    0
Tactic: by_cases hij : i = j
-- 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) j w
hij : i = j
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
    0
have pos : ∀ (w : α i) (hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i w),
  inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i w)) =
    0
Tactic: subst hij
Cleared hypotheses: j, w, hvw, hij
-- 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v w : α i
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i w
h : v = w
⊢ False
have hvw₁ : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i v
Tactic: subst h
Cleared hypotheses: w, hvw, h
-- 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v w : α i
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i w
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i w)) =
    0
have this : v ≠ w
Tactic: have : v ≠ w := fun h => by
      subst h
      exact hvw rfl
-- 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 ι
⊢ 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 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
have rw : 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)
Tactic: rw [← Finset.sum_sdiff_sub_sum_sdiff, sub_eq_add_neg, ← Finset.sum_neg_distrib]