match this with
| Or.inl (_ : dist p q > 0) =>
  let ε := dist p q
  have (And.intro (_ : ε > ε/2) (_ : ε/2 > 0)) := halve ‹ε > 0›
  have : p ⊢ε/2⊣ q := hyp ‹ε/2 > 0›
  have : dist p q ≤ ε/2 := close_dist.mp this
  have : ε ≤ ε/2 := this
  have : p ≃ q := (le_gt_false ‹ε ≤ ε/2› ‹ε > ε/2›).elim
  exact this
| Or.inr (_ : dist p q ≃ 0) =>
  have : p ≃ q := dist_zero.mp ‹dist p q ≃ 0›
  exact this
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
⊢ p ≃ q
no goals