no goals
V : Type ?u.324499
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.324508
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
⊢ ‖-f‖ = ‖f‖
simp only [norm_def, coe_neg, norm_neg, Pi.neg_apply]