𝕜 : Type u_1
E : Type u_2
F : Type ?u.1016275
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
this : FiniteDimensional 𝕜 E
⊢ finrank 𝕜 { x // x ∈ (Submodule.span 𝕜 {v})ᗮ } = n
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1016275
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
⊢ finrank 𝕜 { x // x ∈ (Submodule.span 𝕜 {v})ᗮ } = n
haveI : FiniteDimensional 𝕜 E := fact_finiteDimensional_of_finrank_eq_succ n
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1016275
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
this : FiniteDimensional 𝕜 E
⊢ finrank 𝕜 { x // x ∈ (Submodule.span 𝕜 {v})ᗮ } = n
exact Submodule.finrank_add_finrank_orthogonal' <| by
  simp [finrank_span_singleton hv, _i.elim, add_comm]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1016275
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
this : FiniteDimensional 𝕜 E
⊢ finrank 𝕜 { x // x ∈ Submodule.span 𝕜 {v} } + n = finrank 𝕜 E
simp [finrank_span_singleton hv, _i.elim, add_comm]