α : Type u
β : Type v
X : Type ?u.192900
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ ∃ ε', ε' > 0 ∧ ball y ε' ⊆ ball x ε
α : Type u
β : Type v
X : Type ?u.192900
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
⊢ ∃ ε', ε' > 0 ∧ ball y ε' ⊆ ball x ε
have : 0 < ε - edist y x := by simpa using h
α : Type u
β : Type v
X : Type ?u.192900
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ edist y x + (ε - edist y x) ≤ ε
α : Type u
β : Type v
X : Type ?u.192900
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ ∃ ε', ε' > 0 ∧ ball y ε' ⊆ ball x ε
refine' ⟨ε - edist y x, this, ball_subset _ (ne_top_of_lt h)⟩
no goals
α : Type u
β : Type v
X : Type ?u.192900
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ edist y x + (ε - edist y x) ≤ ε
exact (add_tsub_cancel_of_le (mem_ball.mp h).le).le
no goals
α : Type u
β : Type v
X : Type ?u.192900
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
⊢ 0 < ε - edist y x
simpa using h