∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1),
  (LinearIsometry.toSpanSingleton 𝕜 E hv).toLinearMap = LinearMap.toSpanSingleton 𝕜 E v