case h.e'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1005430
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K✝ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 { x // x ∈ K } + finrank 𝕜 { x // x ∈ Kᗮ } = finrank 𝕜 { x // x ∈ K } + finrank 𝕜 { x // x ∈ Kᗮ ⊓ ⊤ }

case h.e'_3
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1005430
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K✝ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 E = finrank 𝕜 { x // x ∈ ⊤ }
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1005430
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K✝ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 { x // x ∈ K } + finrank 𝕜 { x // x ∈ Kᗮ } = finrank 𝕜 E
convert Submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤) using 1
no goals
case h.e'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1005430
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K✝ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 { x // x ∈ K } + finrank 𝕜 { x // x ∈ Kᗮ } = finrank 𝕜 { x // x ∈ K } + finrank 𝕜 { x // x ∈ Kᗮ ⊓ ⊤ }
rw [inf_top_eq]
no goals
case h.e'_3
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1005430
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K✝ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 E = finrank 𝕜 { x // x ∈ ⊤ }
simp