𝕜 : Type ?u.213757
E : Type u_1
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 < ε
𝕜 : Type ?u.213757
E : Type u_1
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 < ε
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 => _
𝕜 : Type ?u.213757
E : Type u_1
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 / (ε + δ) * ε < ε
𝕜 : Type ?u.213757
E : Type u_1
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 < ε
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
𝕜 : Type ?u.213757
E : Type u_1
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 / (ε + δ) * ε < ε
𝕜 : Type ?u.213757
E : Type u_1
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 / (ε + δ) * ε < ε
rw [← div_lt_one (add_pos hε hδ)] at h
no goals
𝕜 : Type ?u.213757
E : Type u_1
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 / (ε + δ) * ε < ε
exact ⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩
no goals
𝕜 : Type ?u.213757
E : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1
rw [← add_div, div_self (add_pos hε hδ).ne']