ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
have hsv : Injective (s.restrict v) := hv.linearIndependent.injective
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX : Orthonormal 𝕜 Subtype.val
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
have hX : Orthonormal 𝕜 ((↑) : Set.range (s.restrict v) → E) := by
  rwa [orthonormal_subtype_range hsv]
case intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX : Orthonormal 𝕜 Subtype.val
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
obtain ⟨Y, b₀, hX, hb₀⟩ := hX.exists_orthonormalBasis_extension
case intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
case intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
have hιY : Fintype.card ι = Y.card := by
  refine' card_ι.symm.trans _
  exact FiniteDimensional.finrank_eq_card_finset_basis b₀.toBasis
case intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
case intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
have hvsY : s.MapsTo v Y := (s.mapsTo_image v).mono_right (by rwa [← range_restrict])
case intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
case intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
have hsv' : Set.InjOn v s := by
  rw [Set.injOn_iff_injective]
  exact hsv
case intro.intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
g : ι ≃ { x // x ∈ Y }
hg : ∀ (i : ι), i ∈ s → ↑(↑g i) = v i
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
case intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
obtain ⟨g, hg⟩ := hvsY.exists_equiv_extend_of_card_eq hιY hsv'
case intro.intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
g : ι ≃ { x // x ∈ Y }
hg : ∀ (i : ι), i ∈ s → ↑(↑g i) = v i
⊢ ∀ (i : ι), i ∈ s → ↑(OrthonormalBasis.reindex b₀ g.symm) i = v i
case intro.intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
g : ι ≃ { x // x ∈ Y }
hg : ∀ (i : ι), i ∈ s → ↑(↑g i) = v i
⊢ ∃ b, ∀ (i : ι), i ∈ s → ↑b i = v i
use b₀.reindex g.symm
case intro.intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
g : ι ≃ { x // x ∈ Y }
hg : ∀ (i : ι), i ∈ s → ↑(↑g i) = v i
i : ι
hi : i ∈ s
⊢ ↑(OrthonormalBasis.reindex b₀ g.symm) i = v i
case intro.intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
g : ι ≃ { x // x ∈ Y }
hg : ∀ (i : ι), i ∈ s → ↑(↑g i) = v i
⊢ ∀ (i : ι), i ∈ s → ↑(OrthonormalBasis.reindex b₀ g.symm) i = v i
intro i hi
no goals
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
⊢ Orthonormal 𝕜 Subtype.val
rwa [orthonormal_subtype_range hsv]
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
⊢ finrank 𝕜 E = Finset.card Y
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
⊢ Fintype.card ι = Finset.card Y
refine' card_ι.symm.trans _
no goals
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
⊢ finrank 𝕜 E = Finset.card Y
exact FiniteDimensional.finrank_eq_card_finset_basis b₀.toBasis
no goals
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
⊢ v '' s ⊆ ↑Y
rwa [← range_restrict]
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
⊢ Injective (restrict s v)
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
⊢ InjOn v s
rw [Set.injOn_iff_injective]
no goals
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
⊢ Injective (restrict s v)
exact hsv
no goals
case intro.intro.intro.intro
ι✝ : Type ?u.1635810
ι' : Type ?u.1635813
𝕜 : Type u_2
inst✝¹¹ : IsROrC 𝕜
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1635842
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1635860
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1635880
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι✝
v✝ : Set E
A : ι✝ → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_1
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (restrict s v)
hsv : Injective (restrict s v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (restrict s v) ⊆ ↑Y
hb₀ : ↑b₀ = Subtype.val
hιY : Fintype.card ι = Finset.card Y
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
g : ι ≃ { x // x ∈ Y }
hg : ∀ (i : ι), i ∈ s → ↑(↑g i) = v i
i : ι
hi : i ∈ s
⊢ ↑(OrthonormalBasis.reindex b₀ g.symm) i = v i
simp [hb₀, hg i hi]