no goals
R : Type u_2
M : Type u_1
N : Type u_3
G : Type ?u.204628
M' : Type ?u.204631
inst✝⁹ : NormedField R
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : NormedSpace R M
inst✝⁴ : NormedSpace R N
inst✝³ : NormedSpace R G
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c : R
inst✝ : Subsingleton M
f' : M →L[R] N
x : M
⊢ ‖↑0 x‖ = ‖x‖
simp [Subsingleton.elim x 0]