no goals
V : Type u_1
V₁ : Type ?u.319330
V₂ : Type ?u.319333
V₃ : Type ?u.319336
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V
⊢ ‖↑(id V) x‖ ≤ 1 * ‖x‖
simp