[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
⊢ EMetric.diam (c • s) = ‖c‖₊ • EMetric.diam s
[PROOFSTEP]
refine' le_antisymm (ediam_smul_le c s) _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
⊢ ‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)
[PROOFSTEP]
obtain rfl | hc := eq_or_ne c 0
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
s : Set E
⊢ ‖0‖₊ • EMetric.diam s ≤ EMetric.diam (0 • s)
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
⊢ ‖0‖₊ • EMetric.diam ∅ ≤ EMetric.diam (0 • ∅)
[PROOFSTEP]
simp
[GOAL]
case inl.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
s : Set E
hs : Set.Nonempty s
⊢ ‖0‖₊ • EMetric.diam s ≤ EMetric.diam (0 • s)
[PROOFSTEP]
simp [zero_smul_set hs, ← Set.singleton_zero]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
⊢ ‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)
[PROOFSTEP]
have := (lipschitzWith_smul c⁻¹).ediam_image_le (c • s)
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : EMetric.diam ((fun x x_1 => x • x_1) c⁻¹ '' (c • s)) ≤ ↑‖c⁻¹‖₊ * EMetric.diam (c • s)
⊢ ‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)
[PROOFSTEP]
rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
  ENNReal.le_inv_smul_iff (nnnorm_ne_zero_iff.mpr hc)] at this 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
x : Set E
⊢ diam (c • x) = ‖c‖ * diam x
[PROOFSTEP]
simp_rw [diam, ediam_smul₀, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ EMetric.infEdist (c • x) (c • s) = ‖c‖₊ • EMetric.infEdist x s
[PROOFSTEP]
simp_rw [EMetric.infEdist]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ⨅ (y : E) (_ : y ∈ c • s), edist (c • x) y = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
[PROOFSTEP]
have : Function.Surjective ((c • ·) : E → E) := Function.RightInverse.surjective (smul_inv_smul₀ hc)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ ⨅ (y : E) (_ : y ∈ c • s), edist (c • x) y = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
[PROOFSTEP]
trans ⨅ (y) (_ : y ∈ s), ‖c‖₊ • edist x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ ⨅ (y : E) (_ : y ∈ c • s), edist (c • x) y = ⨅ (y : E) (_ : y ∈ s), ‖c‖₊ • edist x y
[PROOFSTEP]
refine' (this.iInf_congr _ fun y => _).symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
y : E
⊢ ⨅ (_ : c • y ∈ c • s), edist (c • x) (c • y) = ⨅ (_ : y ∈ s), ‖c‖₊ • edist x y
[PROOFSTEP]
simp_rw [smul_mem_smul_set_iff₀ hc, edist_smul₀]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ ⨅ (y : E) (_ : y ∈ s), ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
[PROOFSTEP]
have : (‖c‖₊ : ENNReal) ≠ 0 := by simp [hc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ ↑‖c‖₊ ≠ 0
[PROOFSTEP]
simp [hc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this✝ : Function.Surjective fun x => c • x
this : ↑‖c‖₊ ≠ 0
⊢ ⨅ (y : E) (_ : y ∈ s), ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
[PROOFSTEP]
simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ infDist (c • x) (c • s) = ‖c‖ * infDist x s
[PROOFSTEP]
simp_rw [Metric.infDist, infEdist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • ball x r = ball (c • x) (‖c‖ * r)
[PROOFSTEP]
ext y
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem₀ hc]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
[PROOFSTEP]
conv_lhs => rw [← inv_smul_smul₀ hc x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
| c⁻¹ • y ∈ ball x r
[PROOFSTEP]
rw [← inv_smul_smul₀ hc x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
| c⁻¹ • y ∈ ball x r
[PROOFSTEP]
rw [← inv_smul_smul₀ hc x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
| c⁻¹ • y ∈ ball x r
[PROOFSTEP]
rw [← inv_smul_smul₀ hc x]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball (c⁻¹ • c • x) r ↔ y ∈ ball (c • x) (‖c‖ * r)
[PROOFSTEP]
simp [← div_eq_inv_mul, div_lt_iff (norm_pos_iff.2 hc), mul_comm _ r, dist_smul₀]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
⊢ c • ball 0 1 = ball 0 ‖c‖
[PROOFSTEP]
rw [_root_.smul_ball hc, smul_zero, mul_one]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)
[PROOFSTEP]
ext y
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem₀ hc]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
[PROOFSTEP]
conv_lhs => rw [← inv_smul_smul₀ hc x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
| c⁻¹ • y ∈ sphere x r
[PROOFSTEP]
rw [← inv_smul_smul₀ hc x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
| c⁻¹ • y ∈ sphere x r
[PROOFSTEP]
rw [← inv_smul_smul₀ hc x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
| c⁻¹ • y ∈ sphere x r
[PROOFSTEP]
rw [← inv_smul_smul₀ hc x]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r ↔ y ∈ sphere (c • x) (‖c‖ * r)
[PROOFSTEP]
simp only [mem_sphere, dist_smul₀, norm_inv, ← div_eq_inv_mul, div_eq_iff (norm_pos_iff.2 hc).ne', mul_comm r]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)
[PROOFSTEP]
simp only [← ball_union_sphere, Set.smul_set_union, _root_.smul_ball hc, smul_sphere' hc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
[PROOFSTEP]
obtain ⟨ε, εpos, hε⟩ : ∃ ε : ℝ, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
[PROOFSTEP]
obtain ⟨R, Rpos, hR⟩ : ∃ R : ℝ, 0 < R ∧ s ⊆ closedBall 0 R := hs.subset_ball_lt 0 0
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
[PROOFSTEP]
have : Metric.closedBall (0 : 𝕜) (ε / R) ∈ 𝓝 (0 : 𝕜) := closedBall_mem_nhds _ (div_pos εpos Rpos)
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
[PROOFSTEP]
filter_upwards [this] with r hr
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
⊢ {x} + r • s ⊆ u
[PROOFSTEP]
simp only [image_add_left, singleton_add]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
⊢ (fun x_1 => -x + x_1) ⁻¹' (r • s) ⊆ u
[PROOFSTEP]
intro y hy
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)
⊢ y ∈ u
[PROOFSTEP]
obtain ⟨z, zs, hz⟩ : ∃ z : E, z ∈ s ∧ r • z = -x + y := by simpa [mem_smul_set] using hy
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)
⊢ ∃ z, z ∈ s ∧ r • z = -x + y
[PROOFSTEP]
simpa [mem_smul_set] using hy
[GOAL]
case h.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ y ∈ u
[PROOFSTEP]
have I : ‖r • z‖ ≤ ε :=
  calc
    ‖r • z‖ = ‖r‖ * ‖z‖ := norm_smul _ _
    _ ≤ ε / R * R :=
      (mul_le_mul (mem_closedBall_zero_iff.1 hr) (mem_closedBall_zero_iff.1 (hR zs)) (norm_nonneg _)
        (div_pos εpos Rpos).le)
    _ = ε := by field_simp [Rpos.ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ε / R * R = ε
[PROOFSTEP]
field_simp [Rpos.ne']
[GOAL]
case h.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
⊢ y ∈ u
[PROOFSTEP]
have : y = x + r • z := by simp only [hz, add_neg_cancel_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
⊢ y = x + r • z
[PROOFSTEP]
simp only [hz, add_neg_cancel_left]
[GOAL]
case h.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this✝ : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
this : y = x + r • z
⊢ y ∈ u
[PROOFSTEP]
apply hε
[GOAL]
case h.intro.intro.a
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Metric.Bounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this✝ : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
this : y = x + r • z
⊢ y ∈ closedBall x ε
[PROOFSTEP]
simpa only [this, dist_eq_norm, add_sub_cancel', mem_closedBall] using I
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε r : ℝ
hr : 0 < r
⊢ r • ball 0 1 = ball 0 r
[PROOFSTEP]
rw [smul_unitBall hr.ne', Real.norm_of_nonneg hr.le]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z
[PROOFSTEP]
use a • x + b • z
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist x (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
[PROOFSTEP]
nth_rw 1 [← one_smul ℝ x]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
[PROOFSTEP]
nth_rw 4 [← one_smul ℝ z]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) (1 • z) = a * dist x z
[PROOFSTEP]
simp [dist_eq_norm, ← hab, add_smul, ← smul_sub, norm_smul_of_nonneg, ha, hb]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε
[PROOFSTEP]
obtain rfl | hε' := hε.eq_or_lt
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ 0
h : dist x z ≤ 0 + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ 0
[PROOFSTEP]
exact ⟨z, by rwa [zero_add] at h , (dist_self _).le⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ 0
h : dist x z ≤ 0 + δ
⊢ dist x z ≤ δ
[PROOFSTEP]
rwa [zero_add] at h 
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε
[PROOFSTEP]
have hεδ := add_pos_of_pos_of_nonneg hε' hδ
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε
[PROOFSTEP]
refine'
  (exists_dist_eq x z (div_nonneg hε <| add_nonneg hε hδ) (div_nonneg hδ <| add_nonneg hε hδ) <| by
        rw [← add_div, div_self hεδ.ne']).imp
    fun y hy => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1
[PROOFSTEP]
rw [← add_div, div_self hεδ.ne']
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y ≤ δ ∧ dist y z ≤ ε
[PROOFSTEP]
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε
[PROOFSTEP]
rw [← div_le_one hεδ] at h 
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z / (ε + δ) ≤ 1
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε
[PROOFSTEP]
exact ⟨mul_le_of_le_one_left hδ h, mul_le_of_le_one_left hε h⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z < ε
[PROOFSTEP]
refine'
  (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ) (div_nonneg hδ <| add_nonneg hε.le hδ) <| by
        rw [← add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']).imp
    fun y hy => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1
[PROOFSTEP]
rw [← add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y ≤ δ ∧ dist y z < ε
[PROOFSTEP]
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
[PROOFSTEP]
rw [← div_lt_one (add_pos_of_pos_of_nonneg hε hδ)] at h 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z / (ε + δ) < 1
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
[PROOFSTEP]
exact ⟨mul_le_of_le_one_left hδ h.le, mul_lt_of_lt_one_left hε h⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
⊢ ∃ y, dist x y < δ ∧ dist y z ≤ ε
[PROOFSTEP]
obtain ⟨y, yz, xy⟩ := exists_dist_le_lt hε hδ (show dist z x < δ + ε by simpa only [dist_comm, add_comm] using h)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
⊢ dist z x < δ + ε
[PROOFSTEP]
simpa only [dist_comm, add_comm] using h
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
y : E
yz : dist z y ≤ ε
xy : dist y x < δ
⊢ ∃ y, dist x y < δ ∧ dist y z ≤ ε
[PROOFSTEP]
exact ⟨y, by simp [dist_comm x y, dist_comm y z, *]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
y : E
yz : dist z y ≤ ε
xy : dist y x < δ
⊢ dist x y < δ ∧ dist y z ≤ ε
[PROOFSTEP]
simp [dist_comm x y, dist_comm y z, *]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ∃ y, dist x y < δ ∧ dist y z < ε
[PROOFSTEP]
refine'
  (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ.le) (div_nonneg hδ.le <| add_nonneg hε.le hδ.le) <| by
        rw [← add_div, div_self (add_pos hε hδ).ne']).imp
    fun y hy => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1
[PROOFSTEP]
rw [← add_div, div_self (add_pos hε hδ).ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y < δ ∧ dist y z < ε
[PROOFSTEP]
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
[PROOFSTEP]
rw [← div_lt_one (add_pos hε hδ)] at h 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y✝ z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z / (ε + δ) < 1
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
[PROOFSTEP]
exact ⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
⊢ Disjoint (ball x δ) (ball y ε) ↔ δ + ε ≤ dist x y
[PROOFSTEP]
refine' ⟨fun h => le_of_not_lt fun hxy => _, ball_disjoint_ball⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < δ + ε
⊢ False
[PROOFSTEP]
rw [add_comm] at hxy 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
⊢ False
[PROOFSTEP]
obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_lt hδ hε hxy
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z✝ : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y < ε
⊢ False
[PROOFSTEP]
rw [dist_comm] at hxz 
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z✝ : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y < ε
⊢ False
[PROOFSTEP]
exact h.le_bot ⟨hxz, hzy⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
⊢ Disjoint (ball x δ) (closedBall y ε) ↔ δ + ε ≤ dist x y
[PROOFSTEP]
refine' ⟨fun h => le_of_not_lt fun hxy => _, ball_disjoint_closedBall⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < δ + ε
⊢ False
[PROOFSTEP]
rw [add_comm] at hxy 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
⊢ False
[PROOFSTEP]
obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_le hδ hε hxy
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z✝ : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y ≤ ε
⊢ False
[PROOFSTEP]
rw [dist_comm] at hxz 
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z✝ : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y ≤ ε
⊢ False
[PROOFSTEP]
exact h.le_bot ⟨hxz, hzy⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
⊢ Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y
[PROOFSTEP]
rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
⊢ Disjoint (closedBall x δ) (closedBall y ε) ↔ δ + ε < dist x y
[PROOFSTEP]
refine' ⟨fun h => lt_of_not_ge fun hxy => _, closedBall_disjoint_closedBall⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : δ + ε ≥ dist x y
⊢ False
[PROOFSTEP]
rw [add_comm] at hxy 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : ε + δ ≥ dist x y
⊢ False
[PROOFSTEP]
obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z✝ : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : ε + δ ≥ dist x y
z : E
hxz : dist x z ≤ δ
hzy : dist z y ≤ ε
⊢ False
[PROOFSTEP]
rw [dist_comm] at hxz 
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z✝ : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : ε + δ ≥ dist x y
z : E
hxz : dist z x ≤ δ
hzy : dist z y ≤ ε
⊢ False
[PROOFSTEP]
exact h.le_bot ⟨hxz, hzy⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
⊢ infEdist x (thickening δ s) = infEdist x s - ENNReal.ofReal δ
[PROOFSTEP]
obtain hs | hs := lt_or_le (infEdist x s) (ENNReal.ofReal δ)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : infEdist x s < ENNReal.ofReal δ
⊢ infEdist x (thickening δ s) = infEdist x s - ENNReal.ofReal δ
[PROOFSTEP]
rw [infEdist_zero_of_mem, tsub_eq_zero_of_le hs.le]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : infEdist x s < ENNReal.ofReal δ
⊢ x ∈ thickening δ s
[PROOFSTEP]
exact hs
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
⊢ infEdist x (thickening δ s) = infEdist x s - ENNReal.ofReal δ
[PROOFSTEP]
refine' (tsub_le_iff_right.2 infEdist_le_infEdist_thickening_add).antisymm' _
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
⊢ infEdist x (thickening δ s) ≤ infEdist x s - ENNReal.ofReal δ
[PROOFSTEP]
refine' le_sub_of_add_le_right ofReal_ne_top _
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
⊢ infEdist x (thickening δ s) + ENNReal.ofReal δ ≤ infEdist x s
[PROOFSTEP]
refine' le_infEdist.2 fun z hz => le_of_forall_lt' fun r h => _
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : ℝ≥0∞
h : edist x z < r
⊢ infEdist x (thickening δ s) + ENNReal.ofReal δ < r
[PROOFSTEP]
cases' r with r
[GOAL]
case inr.none
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
h : edist x z < none
⊢ infEdist x (thickening δ s) + ENNReal.ofReal δ < none
[PROOFSTEP]
exact add_lt_top.2 ⟨lt_top_iff_ne_top.2 <| infEdist_ne_top ⟨z, self_subset_thickening hδ _ hz⟩, ofReal_lt_top⟩
[GOAL]
case inr.some
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < Option.some r
⊢ infEdist x (thickening δ s) + ENNReal.ofReal δ < Option.some r
[PROOFSTEP]
have hr : 0 < ↑r - δ := by
  refine' sub_pos_of_lt _
  have := hs.trans_lt ((infEdist_le_edist_of_mem hz).trans_lt h)
  rw [ofReal_eq_coe_nnreal hδ.le, some_eq_coe] at this 
  exact_mod_cast this
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < Option.some r
⊢ 0 < ↑r - δ
[PROOFSTEP]
refine' sub_pos_of_lt _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < Option.some r
⊢ δ < ↑r
[PROOFSTEP]
have := hs.trans_lt ((infEdist_le_edist_of_mem hz).trans_lt h)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < Option.some r
this : ENNReal.ofReal δ < Option.some r
⊢ δ < ↑r
[PROOFSTEP]
rw [ofReal_eq_coe_nnreal hδ.le, some_eq_coe] at this 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < Option.some r
this : ↑{ val := δ, property := (_ : 0 ≤ δ) } < ↑r
⊢ δ < ↑r
[PROOFSTEP]
exact_mod_cast this
[GOAL]
case inr.some
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < Option.some r
hr : 0 < ↑r - δ
⊢ infEdist x (thickening δ s) + ENNReal.ofReal δ < Option.some r
[PROOFSTEP]
rw [some_eq_coe, edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel'_right δ ↑r] at h 
[GOAL]
case inr.some
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + (↑r - δ)
hr : 0 < ↑r - δ
⊢ infEdist x (thickening δ s) + ENNReal.ofReal δ < Option.some r
[PROOFSTEP]
obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hr hδ h
[GOAL]
case inr.some.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y✝ z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + (↑r - δ)
hr : 0 < ↑r - δ
y : E
hxy : dist x y < ↑r - δ
hyz : dist y z < δ
⊢ infEdist x (thickening δ s) + ENNReal.ofReal δ < Option.some r
[PROOFSTEP]
refine'
  (ENNReal.add_lt_add_right ofReal_ne_top <|
        infEdist_lt_iff.2 ⟨_, mem_thickening_iff.2 ⟨_, hz, hyz⟩, edist_lt_ofReal.2 hxy⟩).trans_le
    _
[GOAL]
case inr.some.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y✝ z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + (↑r - δ)
hr : 0 < ↑r - δ
y : E
hxy : dist x y < ↑r - δ
hyz : dist y z < δ
⊢ ENNReal.ofReal (↑r - δ) + ENNReal.ofReal δ ≤ Option.some r
[PROOFSTEP]
rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]
[GOAL]
case inr.some.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y✝ z✝ : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEdist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + (↑r - δ)
hr : 0 < ↑r - δ
y : E
hxy : dist x y < ↑r - δ
hyz : dist y z < δ
⊢ ↑r ≤ Option.some r
[PROOFSTEP]
exact le_rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x : E
⊢ x ∈ thickening (ε + δ) s → x ∈ thickening ε (thickening δ s)
[PROOFSTEP]
simp_rw [mem_thickening_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x : E
⊢ (∃ z, z ∈ s ∧ dist x z < ε + δ) → ∃ z, (∃ z_1, z_1 ∈ s ∧ dist z z_1 < δ) ∧ dist x z < ε
[PROOFSTEP]
rintro ⟨z, hz, hxz⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < ε + δ
⊢ ∃ z, (∃ z_1, z_1 ∈ s ∧ dist z z_1 < δ) ∧ dist x z < ε
[PROOFSTEP]
rw [add_comm] at hxz 
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z✝ : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
⊢ ∃ z, (∃ z_1, z_1 ∈ s ∧ dist z z_1 < δ) ∧ dist x z < ε
[PROOFSTEP]
obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hε hδ hxz
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y✝ z✝ : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
y : E
hxy : dist x y < ε
hyz : dist y z < δ
⊢ ∃ z, (∃ z_1, z_1 ∈ s ∧ dist z z_1 < δ) ∧ dist x z < ε
[PROOFSTEP]
exact ⟨y, ⟨_, hz, hyz⟩, hxy⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (thickening δ s)
[PROOFSTEP]
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ.le, infEdist_thickening hδ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEdist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
[PROOFSTEP]
exact tsub_le_iff_right.2
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
s : Set E
⊢ closure (thickening δ s) = cthickening δ s
[PROOFSTEP]
rw [← cthickening_zero, cthickening_thickening le_rfl hδ, zero_add]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ✝ ε δ : ℝ
s : Set E
x : E
⊢ infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ
[PROOFSTEP]
obtain hδ | hδ := le_or_lt δ 0
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ✝ ε δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ
[PROOFSTEP]
rw [cthickening_of_nonpos hδ, infEdist_closure, ofReal_of_nonpos hδ, tsub_zero]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ✝ ε δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ
[PROOFSTEP]
rw [← closure_thickening hδ, infEdist_closure, infEdist_thickening hδ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
s : Set E
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
[PROOFSTEP]
obtain rfl | hδ := hδ.eq_or_lt
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s
[PROOFSTEP]
rw [cthickening_zero, thickening_closure, add_zero]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
[PROOFSTEP]
rw [← closure_thickening hδ, thickening_closure, thickening_thickening hε hδ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (cthickening δ s)
[PROOFSTEP]
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ, infEdist_cthickening]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEdist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
[PROOFSTEP]
exact tsub_le_iff_right.2
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
x : E
⊢ thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)
[PROOFSTEP]
rw [← thickening_singleton, thickening_thickening hε hδ, thickening_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
x : E
⊢ thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)
[PROOFSTEP]
rw [← cthickening_singleton _ hδ, thickening_cthickening hε hδ, thickening_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
x : E
⊢ cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)
[PROOFSTEP]
rw [← thickening_singleton, cthickening_thickening hε hδ, cthickening_singleton _ (add_nonneg hε hδ.le)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : E
⊢ cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)
[PROOFSTEP]
rw [← cthickening_singleton _ hδ, cthickening_cthickening hε hδ, cthickening_singleton _ (add_nonneg hε hδ)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
[PROOFSTEP]
rw [ball_add, thickening_ball hε hδ b, Metric.vadd_ball, vadd_eq_add]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
[PROOFSTEP]
simp_rw [sub_eq_add_neg, neg_ball, ball_add_ball hε hδ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)
[PROOFSTEP]
rw [ball_add, thickening_closedBall hε hδ b, Metric.vadd_ball, vadd_eq_add]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)
[PROOFSTEP]
simp_rw [sub_eq_add_neg, neg_closedBall, ball_add_closedBall hε hδ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
[PROOFSTEP]
rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_comm δ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
[PROOFSTEP]
simp_rw [sub_eq_add_neg, neg_ball, closedBall_add_ball hε hδ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
[PROOFSTEP]
rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a, Metric.vadd_closedBall, vadd_eq_add,
  add_comm, add_comm δ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
[PROOFSTEP]
rw [sub_eq_add_neg, neg_closedBall, closedBall_add_closedBall hε hδ, sub_eq_add_neg]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | hc)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • closedBall x r = closedBall (0 • x) (‖0‖ * r)
[PROOFSTEP]
simp [hr, zero_smul_set, Set.singleton_zero, ← nonempty_closedBall]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)
[PROOFSTEP]
exact smul_closedBall' hc x r
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ c • closedBall 0 1 = closedBall 0 ‖c‖
[PROOFSTEP]
rw [smul_closedBall _ _ zero_le_one, smul_zero, mul_one]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
⊢ r • closedBall 0 1 = closedBall 0 r
[PROOFSTEP]
rw [smul_closedUnitBall, Real.norm_of_nonneg hr]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ Set.Nonempty (sphere x r) ↔ 0 ≤ r
[PROOFSTEP]
obtain ⟨y, hy⟩ := exists_ne x
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
⊢ Set.Nonempty (sphere x r) ↔ 0 ≤ r
[PROOFSTEP]
refine' ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr => ⟨r • ‖y - x‖⁻¹ • (y - x) + x, _⟩⟩
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
⊢ r • ‖y - x‖⁻¹ • (y - x) + x ∈ sphere x r
[PROOFSTEP]
have : ‖y - x‖ ≠ 0 := by simpa [sub_eq_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
⊢ ‖y - x‖ ≠ 0
[PROOFSTEP]
simpa [sub_eq_zero]
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
this : ‖y - x‖ ≠ 0
⊢ r • ‖y - x‖⁻¹ • (y - x) + x ∈ sphere x r
[PROOFSTEP]
simp [norm_smul, this, Real.norm_of_nonneg hr]
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
this : ‖y - x‖ ≠ 0
⊢ |r| * (‖y - x‖⁻¹ * ‖y - x‖) = r
[PROOFSTEP]
rw [inv_mul_cancel this, mul_one, abs_eq_self.mpr hr]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | hc)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • sphere x r = sphere (0 • x) (‖0‖ * r)
[PROOFSTEP]
simp [zero_smul_set, Set.singleton_zero, hr]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)
[PROOFSTEP]
exact smul_sphere' hc x r
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
⊢ x +ᵥ r • ball 0 1 = ball x r
[PROOFSTEP]
rw [smul_unitBall_of_pos hr, vadd_ball_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ x +ᵥ r • closedBall 0 1 = closedBall x r
[PROOFSTEP]
rw [smul_closedUnitBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]
