case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : ∀ (u : Set E), u ⊇ u₀ → Orthonormal 𝕜 Subtype.val → u = u₀
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
obtain ⟨u₀, hu₀s, hu₀, hu₀_max⟩ := exists_maximal_orthonormal hv
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : ∀ (u : Set E), u ⊇ u₀ → Orthonormal 𝕜 Subtype.val → u = u₀
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hu₀] at hu₀_max
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
have hu₀_finite : u₀.Finite := hu₀.linearIndependent.finite
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
let u : Finset E := hu₀_finite.toFinset
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
let fu : ↥u ≃ ↥u₀ := Equiv.cast (congr_arg (↥) hu₀_finite.coe_toFinset)
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
have hfu : ((↑) : u → E) = ((↑) : u₀ → E) ∘ fu := by ext; simp
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
hu : Orthonormal 𝕜 Subtype.val
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
have hu : Orthonormal 𝕜 ((↑) : u → E) := by simpa [hfu] using hu₀.comp _ fu.injective
case intro.intro.intro.refine'_1
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
hu : Orthonormal 𝕜 Subtype.val
⊢ (span 𝕜 (range Subtype.val))ᗮ = ⊥

case intro.intro.intro.refine'_2
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
hu : Orthonormal 𝕜 Subtype.val
⊢ v ⊆ ↑u

case intro.intro.intro.refine'_3
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
hu : Orthonormal 𝕜 Subtype.val
⊢ ↑(OrthonormalBasis.mkOfOrthogonalEqBot hu ?intro.intro.intro.refine'_1) = Subtype.val
case intro.intro.intro
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
hu : Orthonormal 𝕜 Subtype.val
⊢ ∃ u b, v ⊆ ↑u ∧ ↑b = Subtype.val
refine' ⟨u, OrthonormalBasis.mkOfOrthogonalEqBot hu _, _, _⟩
case h
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
x✝ : { x // x ∈ u }
⊢ ↑x✝ = (Subtype.val ∘ ↑fu) x✝
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
⊢ Subtype.val = Subtype.val ∘ ↑fu
ext
no goals
case h
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
x✝ : { x // x ∈ u }
⊢ ↑x✝ = (Subtype.val ∘ ↑fu) x✝
simp
no goals
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
⊢ Orthonormal 𝕜 Subtype.val
simpa [hfu] using hu₀.comp _ fu.injective
no goals
case intro.intro.intro.refine'_1
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
hu : Orthonormal 𝕜 Subtype.val
⊢ (span 𝕜 (range Subtype.val))ᗮ = ⊥
simpa using hu₀_max
no goals
case intro.intro.intro.refine'_2
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
hu : Orthonormal 𝕜 Subtype.val
⊢ v ⊆ ↑u
simpa using hu₀s
no goals
case intro.intro.intro.refine'_3
ι : Type ?u.1609152
ι' : Type ?u.1609155
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1609184
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1609202
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1609222
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : Set.Finite u₀
u : Finset E := Finite.toFinset hu₀_finite
fu : { x // x ∈ u } ≃ ↑u₀ := Equiv.cast (_ : ↑↑(Finite.toFinset hu₀_finite) = ↑u₀)
hfu : Subtype.val = Subtype.val ∘ ↑fu
hu : Orthonormal 𝕜 Subtype.val
⊢ ↑(OrthonormalBasis.mkOfOrthogonalEqBot hu (_ : (span 𝕜 (range Subtype.val))ᗮ = ⊥)) = Subtype.val
simp