Theorem: norm_add₄_le (PrimeNumberTheoremAnd/ZetaBounds.lean)

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

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

State before:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d : E
⊢ ‖a + b + c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖
Tactic:
apply norm_add₃_le
State after:
no goals