awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀))
hu₀_max : Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset (s := u₀)
fu : ↥u ≃ (↑u₀ : Type u_4) := hu₀_finite.subtypeEquivToFinset (s := u₀).symm
hu : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
⊢ ∃ (u : Finset E) (b : OrthonormalBasis (↥u) 𝕜 E),
    v ⊆ (↑u : Set E) ∧ Eq.{u_4 + 1} (α := (a : ↥u) → E) (⇑b : (a : ↥u) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ u))

Tactic:
⟨u, OrthonormalBasis.mkOfOrthogonalEqBot hu ?_, ?_, ?_⟩

Premises used: OrthonormalBasis.mkOfOrthogonalEqBot, And.intro, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀))
hu₀_max : Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset (s := u₀)
fu : ↥u ≃ (↑u₀ : Type u_4) := hu₀_finite.subtypeEquivToFinset (s := u₀).symm
hu : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
refine_1 : Eq.{u_4 + 1} (α := Submodule 𝕜 E) (span 𝕜 (range (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))))ᗮ ⊥
refine_2 : v ⊆ (↑u : Set E)
refine_3 :
  Eq.{u_4 + 1} (α := (a : ↥u) → E) (⇑(OrthonormalBasis.mkOfOrthogonalEqBot hu ⋯) : (a : ↥u) → E)
    (Subtype.val (p := fun (x : E) ↦ x ∈ u))
⊢ ∃ (u : Finset E) (b : OrthonormalBasis (↥u) 𝕜 E),
    v ⊆ (↑u : Set E) ∧ Eq.{u_4 + 1} (α := (a : ↥u) → E) (⇑b : (a : ↥u) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ u))

Tactic:
refine ⟨u, OrthonormalBasis.mkOfOrthogonalEqBot hu ?_, ?_, ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀))
hu₀_max : Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset (s := u₀)
fu : ↥u ≃ (↑u₀ : Type u_4) := hu₀_finite.subtypeEquivToFinset (s := u₀).symm
hu : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
⊢ Eq.{u_4 + 1} (α := Submodule 𝕜 E) (span 𝕜 (range (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))))ᗮ ⊥

Tactic:
simpa [u] using hu₀_max
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀))
hu₀_max : Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset (s := u₀)
fu : ↥u ≃ (↑u₀ : Type u_4) := hu₀_finite.subtypeEquivToFinset (s := u₀).symm
hu : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
⊢ v ⊆ (↑u : Set E)

Tactic:
simpa [u] using hu₀s
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀))
hu₀_max : Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset (s := u₀)
fu : ↥u ≃ (↑u₀ : Type u_4) := hu₀_finite.subtypeEquivToFinset (s := u₀).symm
hu : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
⊢ Eq.{u_4 + 1} (α := (a : ↥u) → E) (⇑(OrthonormalBasis.mkOfOrthogonalEqBot hu ⋯) : (a : ↥u) → E)
    (Subtype.val (p := fun (x : E) ↦ x ∈ u))

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
⊢ Injective (s.restrict («π» := fun (a : ι) ↦ E) v)

Tactic:
have hsv : Injective (s.restrict v) := hv.linearIndependent.injective
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
rwa rwa₁ rwa₂ rwa₃ : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
⊢ 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:
rwa [orthonormal_subtype_range hsv]

Premises used: orthonormal_subtype_range
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
⊢ 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]
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)))
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
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i

Tactic:
obtain ⟨Y, b₀, hX, hb₀⟩ := hX.exists_orthonormalBasis_extension

Premises used: Orthonormal.exists_orthonormalBasis_extension
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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

Tactic:
card_ι.symm.trans ?_

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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))
refine : finrank 𝕜 E = Y.card
⊢ Fintype.card ι = Y.card

Tactic:
refine card_ι.symm.trans ?_

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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))
⊢ finrank 𝕜 E = Y.card

Tactic:
Module.finrank_eq_card_finset_basis b₀.toBasis

Premises used: Module.finrank_eq_card_finset_basis, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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))
⊢ finrank 𝕜 E = Y.card

Tactic:
exact Module.finrank_eq_card_finset_basis b₀.toBasis

Premises used: Module.finrank_eq_card_finset_basis, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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

Tactic:
have hιY : Fintype.card ι = Y.card := by
    refine card_ι.symm.trans ?_
    exact Module.finrank_eq_card_finset_basis b₀.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
rwa rwa₁ rwa₂ rwa₃ : range (s.restrict («π» := fun (a : ι) ↦ E) v) ⊆ (↑Y : Set E)
⊢ v '' s ⊆ (↑Y : Set E)

Tactic:
rwa [← range_restrict]

Premises used: Set.range_restrict
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
⊢ MapsTo v s (↑Y : Set E)

Tactic:
have hvsY : s.MapsTo v Y := (s.mapsTo_image v).mono_right (by rwa [← range_restrict])
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
rw : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
⊢ InjOn v s

Tactic:
rw [Set.injOn_iff_injective]

Premises used: Set.injOn_iff_injective
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
⊢ Injective (s.restrict («π» := fun (a : ι) ↦ E) v)

Tactic:
hsv
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
⊢ Injective (s.restrict («π» := fun (a : ι) ↦ E) v)

Tactic:
exact hsv
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
⊢ InjOn v s

Tactic:
have hsv' : Set.InjOn v s := by
    rw [Set.injOn_iff_injective]
    exact hsv
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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
⊢ ∃ (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'

Premises used: Set.MapsTo.exists_equiv_extend_of_card_eq
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
h : ∀ i ∈ s, (b₀.reindex g.symm : (a : ι) → E) i = v i
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i

Tactic:
use b₀.reindex g.symm

Premises used: OrthonormalBasis.reindex, Equiv.symm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
i : ι
hi : i ∈ s
⊢ (b₀.reindex g.symm : (a : ι) → E) i = v i

Tactic:
simp [hb₀, hg i hi]
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
⊢ ∃ (w : Finset E) (b : OrthonormalBasis (↥w) 𝕜 E),
    Eq.{u_4 + 1} (α := (a : ↥w) → E) (⇑b : (a : ↥w) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ w))

Tactic:
let ⟨w, hw, _, hw''⟩ := (orthonormal_empty 𝕜 E).exists_orthonormalBasis_extension
  ⟨w, hw, hw''⟩

Premises used: orthonormal_empty, Exists, _private.0.exists_orthonormalBasis.match_1, Exists.intro, Subtype.val, Eq, Orthonormal.exists_orthonormalBasis_extension, DFunLike.coe