値域がEmptyになっているせいで失敗する例. choose タクティク

class Metric (X : Type ) where
  dist : X → X → ℝ

example  [Metric X] :
  ∃ δ, 0 < δ ∧ ∀ y : X, Metric.dist y y = δ
:= by
  by_contra F; simp at F
  -- これは失敗する
  -- choose! g Hg using F
  choose g Hg using F
  guard_hyp g : (x : ℝ) → 0 < x → X
  sorry

example [Nonempty X] [Metric X] :
  ∃ δ, 0 < δ ∧ ∀ y : X, Metric.dist y y = δ
:= by
  by_contra F; simp at F
  -- これは成功
  choose! g Hg using F
  sorry

Start with the two Lean examples in the issue and reproduce the contrasting choose and choose! results. Trace how the tactics handle the empty-valued range and identify the repository example or explanation that needs updating; done means the distinction and required assumptions are clear.