case h
𝕜 : Type u_1
𝕜₂ : Type ?u.379365
E : Type u_2
F : Type ?u.379371
G : Type ?u.379374
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜₂
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ ↑(toSpanSingleton 𝕜 (x + y)) 1 = ↑(toSpanSingleton 𝕜 x + toSpanSingleton 𝕜 y) 1
𝕜 : Type u_1
𝕜₂ : Type ?u.379365
E : Type u_2
F : Type ?u.379371
G : Type ?u.379374
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜₂
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ toSpanSingleton 𝕜 (x + y) = toSpanSingleton 𝕜 x + toSpanSingleton 𝕜 y
ext1
no goals
case h
𝕜 : Type u_1
𝕜₂ : Type ?u.379365
E : Type u_2
F : Type ?u.379371
G : Type ?u.379374
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜₂
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ ↑(toSpanSingleton 𝕜 (x + y)) 1 = ↑(toSpanSingleton 𝕜 x + toSpanSingleton 𝕜 y) 1
simp [toSpanSingleton_apply]