no goals
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type ?u.13769
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
x : G
⊢ ‖↑f x‖ ≤ ‖completion f‖ * ‖x‖
simpa using f.completion.le_opNorm x