case inl
𝕜 : Type ?u.292192
E : Type u_1
F : Type ?u.292198
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Metric.ball 0 r ⊆ s
hr : r ≤ 0
⊢ r * gauge s x ≤ ‖x‖

case inr
𝕜 : Type ?u.292192
E : Type u_1
F : Type ?u.292198
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Metric.ball 0 r ⊆ s
hr : 0 < r
⊢ r * gauge s x ≤ ‖x‖
𝕜 : Type ?u.292192
E : Type u_1
F : Type ?u.292198
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Metric.ball 0 r ⊆ s
⊢ r * gauge s x ≤ ‖x‖
obtain hr | hr := le_or_lt r 0
case inr
𝕜 : Type ?u.292192
E : Type u_1
F : Type ?u.292198
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Metric.ball 0 r ⊆ s
hr : 0 < r
⊢ gauge s x ≤ gauge (Metric.ball 0 r) x
case inr
𝕜 : Type ?u.292192
E : Type u_1
F : Type ?u.292198
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Metric.ball 0 r ⊆ s
hr : 0 < r
⊢ r * gauge s x ≤ ‖x‖
rw [mul_comm, ← le_div_iff hr, ← gauge_ball hr]
no goals
case inr
𝕜 : Type ?u.292192
E : Type u_1
F : Type ?u.292198
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Metric.ball 0 r ⊆ s
hr : 0 < r
⊢ gauge s x ≤ gauge (Metric.ball 0 r) x
exact gauge_mono (absorbent_ball_zero hr) hs x
no goals
case inl
𝕜 : Type ?u.292192
E : Type u_1
F : Type ?u.292198
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Metric.ball 0 r ⊆ s
hr : r ≤ 0
⊢ r * gauge s x ≤ ‖x‖
exact (mul_nonpos_of_nonpos_of_nonneg hr <| gauge_nonneg _).trans (norm_nonneg _)