awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_7
inst_4 : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
hsv : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
have hX : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v) })
  (Subtype.val (p := fun (x : E) ↦ x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v)))
Tactic: have hX : Orthonormal 𝕜 ((↑) : Set.range (s.restrict v) → E) := by
    rwa [orthonormal_subtype_range hsv]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_7
inst_4 : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
hsv : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
hX :
  Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v) })
    (Subtype.val (p := fun (x : E) ↦ x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v)))
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
have obtain : ∀ (Y : Finset E) (b₀ : OrthonormalBasis (↥Y) 𝕜 E) (hX : range (s.restrict («π» := fun (a : ι) ↦ E) v) ⊆ (↑Y : Set E))
  (hb₀ : Eq.{u_4 + 1} (α := (a : ↥Y) → E) (⇑b₀ : (a : ↥Y) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Y))),
  ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
Tactic: obtain ⟨Y, b₀, hX, hb₀⟩ := hX.exists_orthonormalBasis_extension
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_7
inst_4 : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
hsv : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
hX_1 :
  Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v) })
    (Subtype.val (p := fun (x : E) ↦ x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v)))
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.restrict («π» := fun (a : ι) ↦ E) v) ⊆ (↑Y : Set E)
hb₀ : Eq.{u_4 + 1} (α := (a : ↥Y) → E) (⇑b₀ : (a : ↥Y) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Y))
⊢ Fintype.card ι = Y.card
have refine : finrank 𝕜 E = Y.card
Tactic: refine card_ι.symm.trans ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_7
inst_4 : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
hsv : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
hX_1 :
  Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v) })
    (Subtype.val (p := fun (x : E) ↦ x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v)))
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.restrict («π» := fun (a : ι) ↦ E) v) ⊆ (↑Y : Set E)
hb₀ : Eq.{u_4 + 1} (α := (a : ↥Y) → E) (⇑b₀ : (a : ↥Y) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Y))
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
have hιY : Fintype.card ι = Y.card
Tactic: have hιY : Fintype.card ι = Y.card := by
    refine card_ι.symm.trans ?_
    exact Module.finrank_eq_card_finset_basis b₀.toBasis
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_7
inst_4 : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
hsv : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
hX_1 :
  Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v) })
    (Subtype.val (p := fun (x : E) ↦ x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v)))
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.restrict («π» := fun (a : ι) ↦ E) v) ⊆ (↑Y : Set E)
hb₀ : Eq.{u_4 + 1} (α := (a : ↥Y) → E) (⇑b₀ : (a : ↥Y) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Y))
hιY : Fintype.card ι = Y.card
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
have hvsY : MapsTo v s (↑Y : Set E)
Tactic: have hvsY : s.MapsTo v Y := (s.mapsTo_image v).mono_right (by rwa [← range_restrict])
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_7
inst_4 : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
hsv : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
hX_1 :
  Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v) })
    (Subtype.val (p := fun (x : E) ↦ x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v)))
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.restrict («π» := fun (a : ι) ↦ E) v) ⊆ (↑Y : Set E)
hb₀ : Eq.{u_4 + 1} (α := (a : ↥Y) → E) (⇑b₀ : (a : ↥Y) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Y))
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s (↑Y : Set E)
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
have hsv' : InjOn v s
Tactic: have hsv' : Set.InjOn v s := by
    rw [Set.injOn_iff_injective]
    exact hsv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_7
inst_4 : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
hsv : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
hX_1 :
  Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v) })
    (Subtype.val (p := fun (x : E) ↦ x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v)))
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.restrict («π» := fun (a : ι) ↦ E) v) ⊆ (↑Y : Set E)
hb₀ : Eq.{u_4 + 1} (α := (a : ↥Y) → E) (⇑b₀ : (a : ↥Y) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Y))
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s (↑Y : Set E)
hsv' : InjOn v s
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
have obtain : ∀ (g : Equiv.{u_7 + 1, u_4 + 1} ι ↥Y) (hg : ∀ i ∈ s, (↑((g : (a : ι) → ↥Y) i) : E) = v i),
  ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
Tactic: obtain ⟨g, hg⟩ := hvsY.exists_equiv_extend_of_card_eq hιY hsv'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_7
inst_4 : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
hsv : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
hX_1 :
  Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v) })
    (Subtype.val (p := fun (x : E) ↦ x ∈ range (s.restrict («π» := fun (a : ι) ↦ E) v)))
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.restrict («π» := fun (a : ι) ↦ E) v) ⊆ (↑Y : Set E)
hb₀ : Eq.{u_4 + 1} (α := (a : ↥Y) → E) (⇑b₀ : (a : ↥Y) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Y))
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s (↑Y : Set E)
hsv' : InjOn v s
g : Equiv.{u_7 + 1, u_4 + 1} ι ↥Y
hg : ∀ i ∈ s, (↑((g : (a : ι) → ↥Y) i) : E) = v i
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
have h : ∀ i ∈ s, (b₀.reindex g.symm : (a : ι) → E) i = v i
Tactic: use b₀.reindex g.symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
b : OrthonormalBasis
  (↥(Classical.choose (p := fun (x : Finset E) ↦
      ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
        Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
      ⋯))
  𝕜 E :=
  Classical.choose (p :=
    fun
      (x :
        OrthonormalBasis
          (↥(Classical.choose (p := fun (x : Finset E) ↦
              ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
                Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
              ⋯))
          𝕜 E) ↦
    Eq.{u_4 + 1} (α :=
      (a :
          ↥(Classical.choose (p := fun (x : Finset E) ↦
              ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
                Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
              ⋯)) →
        E)
      (⇑x : (a : ↥(Classical.choose ⋯)) → E)
      (Subtype.val (p := fun (x : E) ↦
        x ∈
          Classical.choose (p := fun (x : Finset E) ↦
            ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
              Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
            ⋯)))
    ⋯
⊢ OrthonormalBasis (Fin (finrank 𝕜 E)) 𝕜 E
have rw : OrthonormalBasis
  (Fin
    (Fintype.card.{u_4}
      ↥(Classical.choose (p := fun (x : Finset E) ↦
          ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
            Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
          sorry)))
  𝕜 E
Tactic: rw [finrank_eq_card_basis b.toBasis]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ (Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ 1) ∨ Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ -1
have have : ∀ (this : Unique ι),
  (Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ 1) ∨ Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ -1
Tactic: have : Unique ι := b.toBasis.unique
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
have this₁ : Norm.norm (E := ℝ) ((b : (a : ι) → ℝ) default : ℝ) = 1
Tactic: have : ‖b default‖ = 1 := b.orthonormal.1 _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this_1 : Unique ι
this : Norm.norm (E := ℝ) ((b : (a : ι) → ℝ) default : ℝ) = 1
⊢ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
have rwa : ∀ (this : Eq (α := ℝ) (|(b : (a : ι) → ℝ) default| : ℝ) (1 : ℝ)),
  Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
Tactic: rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this_1 : Unique ι
this : Norm.norm (E := ℝ) ((b : (a : ι) → ℝ) default : ℝ) = 1
rwa :
  ∀ (this : Eq (α := ℝ) (|(b : (a : ι) → ℝ) default| : ℝ) (1 : ℝ)),
    Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
⊢ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
have rwa₁ : ∀ (this : Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)),
  Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
Tactic: rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ (Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ 1) ∨ Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ -1
have this₁ : Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
Tactic: have : b default = 1 ∨ b default = -1 := by
    have : ‖b default‖ = 1 := b.orthonormal.1 _
    rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this_1 : Unique ι
this : Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
⊢ (Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ 1) ∨ Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ -1
have rw : (Eq (α := (a : ι) → ℝ) (const ι ((b : (a : ι) → ℝ) default) : ι → ℝ) fun (x : ι) ↦ (1 : ℝ)) ∨
  Eq (α := (a : ι) → ℝ) (const ι ((b : (a : ι) → ℝ) default) : ι → ℝ) fun (x : ι) ↦ (-1 : ℝ)
Tactic: rw [eq_const_of_unique b]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_5 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
hi : V i ≠ ⊥
⊢ ∃ (a : Fin n), subordinateOrthonormalBasisIndex hn hV a hV' = i
have h : subordinateOrthonormalBasisIndex hn hV
    ((sigmaOrthonormalBasisIndexEquiv hn hV hV' : (a : (i : ι) × Fin (finrank 𝕜 ↥(V i))) → Fin n)
      (Sigma.mk (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))) i (⟨0, sorry⟩ : Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))))
    hV' =
  i
Tactic: use hV.sigmaOrthonormalBasisIndexEquiv hn hV' ⟨i, ⟨0, by grind [finrank_eq_zero (S := V i)]⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_9 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
a : { a : Fin n // subordinateOrthonormalBasisIndex hn hV a hV' = i }
⊢ finrank.{u_3, u_4} 𝕜
      ↥(V
          (Sigma.fst (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))
            (((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm : (a : Fin n) → (i : ι) × Fin (finrank 𝕜 ↥(V i)))
              (↑a : Fin n)))) =
    finrank.{u_3, u_4} 𝕜 ↥(V i)
have rw : finrank.{u_3, u_4} 𝕜 ↥(V (subordinateOrthonormalBasisIndex hn hV (↑a : Fin n) hV')) = finrank.{u_3, u_4} 𝕜 ↥(V i)
Tactic: rw [← subordinateOrthonormalBasisIndex_def, a.property]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_9 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
a : { a : Fin n // subordinateOrthonormalBasisIndex hn hV a hV' = i }
rw : finrank.{u_3, u_4} 𝕜 ↥(V (subordinateOrthonormalBasisIndex hn hV (↑a : Fin n) hV')) = finrank.{u_3, u_4} 𝕜 ↥(V i)
⊢ finrank.{u_3, u_4} 𝕜
      ↥(V
          (Sigma.fst (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))
            (((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm : (a : Fin n) → (i : ι) × Fin (finrank 𝕜 ↥(V i)))
              (↑a : Fin n)))) =
    finrank.{u_3, u_4} 𝕜 ↥(V i)
have rw₁ : finrank.{u_3, u_4} 𝕜 ↥(V i) = finrank.{u_3, u_4} 𝕜 ↥(V i)
Tactic: rw [← subordinateOrthonormalBasisIndex_def, a.property]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_5 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
⊢ Finset.card (α := Fin n) {a : Fin n | subordinateOrthonormalBasisIndex hn hV a hV' = i} = finrank.{u_3, u_4} 𝕜 ↥(V i)
have i₁ : ↥{a : Fin n | subordinateOrthonormalBasisIndex hn hV a hV' = i} ≃ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))
Tactic: apply Finset.card_eq_of_equiv_fin
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
⊢ ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
have dim_LS_perp : finrank.{u_3, u_7} 𝕜 ↥LSᗮ = d
Tactic: have dim_LS_perp : finrank 𝕜 LSᗮ = d :=
      calc
        finrank 𝕜 LSᗮ = finrank 𝕜 V - finrank 𝕜 LS := by
          simp only [← LS.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
        _ = finrank 𝕜 V - finrank 𝕜 S := by
          simp only [LS, LinearMap.finrank_range_of_inj L.injective]
        _ = finrank 𝕜 Sᗮ := by simp only [← S.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
⊢ V →ₗᵢ[𝕜] V
have have : (E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ) → V →ₗᵢ[𝕜] V
Tactic: have E : Sᗮ ≃ₗᵢ[𝕜] LSᗮ := by
    have dim_LS_perp : finrank 𝕜 LSᗮ = d :=
      calc
        finrank 𝕜 LSᗮ = finrank 𝕜 V - finrank 𝕜 LS := by
          simp only [← LS.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
        _ = finrank 𝕜 V - finrank 𝕜 S := by
          simp only [LS, LinearMap.finrank_range_of_inj L.injective]
        _ = finrank 𝕜 Sᗮ := by simp only [← S.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
    exact
      (stdOrthonormalBasis 𝕜 Sᗮ).repr.trans
        ((stdOrthonormalBasis 𝕜 LSᗮ).reindex <| finCongr dim_LS_perp).repr.symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
⊢ V →ₗᵢ[𝕜] V
have this : CompleteSpace.{u_7} ↥S
Tactic: haveI : CompleteSpace S := FiniteDimensional.complete 𝕜 S
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this : CompleteSpace.{u_7} ↥S
⊢ V →ₗᵢ[𝕜] V
have this₁ : CompleteSpace V
Tactic: haveI : CompleteSpace V := FiniteDimensional.complete 𝕜 V
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
⊢ Norm.norm (E := V) ((M : (a : V) → V) x : V) = ‖x‖
have Mx_decomp : (M : (a : V) → V) x =
  HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
    ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
Tactic: have Mx_decomp : M x = L (p1 x) + L3 (p2 x) := by
      simp only [M, LinearMap.add_apply, LinearMap.comp_apply, LinearMap.comp_apply,
        LinearIsometry.coe_toLinearMap]