simp only [add_le_add_iff_right]
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d e : E
⊢ ‖a + b + c + d‖ + ‖e‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ + ‖e‖
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d e : E
⊢ ‖a + b + c + d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖