case intro.intro.intro
M : Type u_1
N : Type ?u.346908
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ ‖↑x + ↑y‖ ≤ ‖↑x‖ + ‖↑y‖
M : Type u_1
N : Type ?u.346908
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M ⧸ S
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖
rcases And.intro (mk_surjective x) (mk_surjective y) with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
case intro.intro.intro
M : Type u_1
N : Type ?u.346908
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ (⨅ (a : ↑↑S), ‖x + y + ↑a‖) ≤ (⨅ (a : ↑↑S), ‖x + ↑a‖) + ⨅ (a : ↑↑S), ‖y + ↑a‖
case intro.intro.intro
M : Type u_1
N : Type ?u.346908
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ ‖↑x + ↑y‖ ≤ ‖↑x‖ + ‖↑y‖
simp only [← mk'_apply, ← map_add, quotient_norm_mk_eq, sInf_image']
case intro.intro.intro
M : Type u_1
N : Type ?u.346908
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ (⨅ (a : ↑↑S), ‖x + y + ↑a‖) ≤ ‖x + ↑a‖ + ‖y + ↑b‖
case intro.intro.intro
M : Type u_1
N : Type ?u.346908
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ (⨅ (a : ↑↑S), ‖x + y + ↑a‖) ≤ (⨅ (a : ↑↑S), ‖x + ↑a‖) + ⨅ (a : ↑↑S), ‖y + ↑a‖
refine le_ciInf_add_ciInf fun a b ↦ ?_
case intro.intro.intro
M : Type u_1
N : Type ?u.346908
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ‖x + y + ↑(a + b)‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖
case intro.intro.intro
M : Type u_1
N : Type ?u.346908
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ (⨅ (a : ↑↑S), ‖x + y + ↑a‖) ≤ ‖x + ↑a‖ + ‖y + ↑b‖
refine ciInf_le_of_le ⟨0, forall_range_iff.2 fun _ ↦ norm_nonneg _⟩ (a + b) ?_
no goals
case intro.intro.intro
M : Type u_1
N : Type ?u.346908
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ‖x + y + ↑(a + b)‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖
exact (congr_arg norm (add_add_add_comm _ _ _ _)).trans_le (norm_add_le _ _)