apply le_trans <| norm_add_le (a + b + c) d
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d : E
⊢ ‖a + b + c + d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d : E
⊢ ‖a + b + c‖ + ‖d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖