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

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

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

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