𝕜 : Type ?u.224089
E : Type u_1
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 < ε
𝕜 : Type ?u.224089
E : Type u_1
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)
simp_rw [mem_thickening_iff]
case intro.intro
𝕜 : Type ?u.224089
E : Type u_1
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 < ε
𝕜 : Type ?u.224089
E : Type u_1
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 < ε
rintro ⟨z, hz, hxz⟩
case intro.intro
𝕜 : Type ?u.224089
E : Type u_1
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 < ε
case intro.intro
𝕜 : Type ?u.224089
E : Type u_1
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 < ε
rw [add_comm] at hxz
case intro.intro.intro.intro
𝕜 : Type ?u.224089
E : Type u_1
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 < ε
case intro.intro
𝕜 : Type ?u.224089
E : Type u_1
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 < ε
obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hε hδ hxz
no goals
case intro.intro.intro.intro
𝕜 : Type ?u.224089
E : Type u_1
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 < ε
exact ⟨y, ⟨_, hz, hyz⟩, hxy⟩