𝕜 : Type ?u.219618
E : Type u_1
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
𝕜 : Type ?u.219618
E : Type u_1
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
refine' ⟨fun h => lt_of_not_ge fun hxy => _, closedBall_disjoint_closedBall⟩
𝕜 : Type ?u.219618
E : Type u_1
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
𝕜 : Type ?u.219618
E : Type u_1
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
rw [add_comm] at hxy
case intro.intro
𝕜 : Type ?u.219618
E : Type u_1
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
𝕜 : Type ?u.219618
E : Type u_1
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
obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy
case intro.intro
𝕜 : Type ?u.219618
E : Type u_1
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
case intro.intro
𝕜 : Type ?u.219618
E : Type u_1
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
rw [dist_comm] at hxz
no goals
case intro.intro
𝕜 : Type ?u.219618
E : Type u_1
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
exact h.le_bot ⟨hxz, hzy⟩