case symmetric
𝕜 : Type ?u.286698
E : Type u_1
F : Type ?u.286704
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x✝ : E
hr : 0 < r
x : E
⊢ ∀ (x : E), x ∈ Metric.ball 0 1 → -x ∈ Metric.ball 0 1
𝕜 : Type ?u.286698
E : Type u_1
F : Type ?u.286704
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x✝ : E
hr : 0 < r
x : E
⊢ gauge (Metric.ball 0 r) x = ‖x‖ / r
rw [← smul_unitBall_of_pos hr, gauge_smul_left, Pi.smul_apply, gauge_unit_ball, smul_eq_mul,
  abs_of_nonneg hr.le, div_eq_inv_mul]
case symmetric
𝕜 : Type ?u.286698
E : Type u_1
F : Type ?u.286704
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x✝ : E
hr : 0 < r
x : E
⊢ ∀ (x : E), ‖x‖ < 1 → ‖x‖ < 1
case symmetric
𝕜 : Type ?u.286698
E : Type u_1
F : Type ?u.286704
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x✝ : E
hr : 0 < r
x : E
⊢ ∀ (x : E), x ∈ Metric.ball 0 1 → -x ∈ Metric.ball 0 1
simp_rw [mem_ball_zero_iff, norm_neg]
no goals
case symmetric
𝕜 : Type ?u.286698
E : Type u_1
F : Type ?u.286704
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x✝ : E
hr : 0 < r
x : E
⊢ ∀ (x : E), ‖x‖ < 1 → ‖x‖ < 1
exact fun _ => id