case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.781831
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ ≤ topologicalClosure K

case refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.781831
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ topologicalClosure K ≤ Kᗮᗮ
𝕜 : Type u_2
E : Type u_1
F : Type ?u.781831
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ = topologicalClosure K
refine' le_antisymm _ _
case h.e'_4
𝕜 : Type u_2
E : Type u_1
F : Type ?u.781831
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ topologicalClosure K = (topologicalClosure K)ᗮᗮ
case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.781831
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ ≤ topologicalClosure K
convert Submodule.orthogonal_orthogonal_monotone K.le_topologicalClosure using 1
case h.e'_4
𝕜 : Type u_2
E : Type u_1
F : Type ?u.781831
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
this : CompleteSpace { x // x ∈ topologicalClosure K }
⊢ topologicalClosure K = (topologicalClosure K)ᗮᗮ
case h.e'_4
𝕜 : Type u_2
E : Type u_1
F : Type ?u.781831
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ topologicalClosure K = (topologicalClosure K)ᗮᗮ
haveI : CompleteSpace K.topologicalClosure :=
  K.isClosed_topologicalClosure.completeSpace_coe
no goals
case h.e'_4
𝕜 : Type u_2
E : Type u_1
F : Type ?u.781831
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
this : CompleteSpace { x // x ∈ topologicalClosure K }
⊢ topologicalClosure K = (topologicalClosure K)ᗮᗮ
rw [K.topologicalClosure.orthogonal_orthogonal]
no goals
case refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.781831
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ topologicalClosure K ≤ Kᗮᗮ
exact K.topologicalClosure_minimal K.le_orthogonal_orthogonal Kᗮ.isClosed_orthogonal