no goals
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ Projectivization.submodule v = Submodule.span K {Projectivization.rep v}
conv_lhs => rw [← v.mk_rep]