no goals
𝕜 : Type u_2
𝕜₂ : Type ?u.374483
E : Type u_1
F : Type ?u.374489
G : Type ?u.374492
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜₂
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : 𝕜
⊢ ↑(toSpanSingleton 𝕜 x) r = r • x
simp [toSpanSingleton, ofHomothety, LinearMap.toSpanSingleton]