no goals
V : Type ?u.496737
W : Type ?u.496740
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.496749
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
v : V₁
⊢ ‖↑0 v‖ ≤ ‖v‖
simp