Error message using rcases: recursor 'Exists.casesOn' can on

Stream: new members

[Michael Rothgang]

Using the rcases, I get the error message above. Can a kind soul tell me what's going wrong/point to some documentation? (Searching zulip doesn't yield any results I understand --- if they're relevant, I would need a pointer to some more basic explanation first.)

import Mathlib.Topology.MetricSpace.Lipschitz
open Topology
set_option autoImplicit false
variable {X Y : Type*} [MetricSpace X] [MetricSpace Y]

/-- `f : X → Y` is **locally Lipschitz** iff every point `p ∈ X` has a neighourhood
on which `f` is Lipschitz. -/
def LocallyLipschitz (f : X → Y) : Prop := ∀ x : X, ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

lemma minimized {f : X → Y} (hf : LocallyLipschitz f) {s : Set X}: True /- dummy statement -/ := by
  -- Consider the cover (U_x) of s induced by hf: each N_s is an open subset containing x
  -- on which f is Lipschitz, say with constant K_x.
  let U : s → Set X := by
    intro x
    -- ERROR: uncommenting this line fails with error message
    -- tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop
    -- rcases hf x with ⟨Kx, t, ht, hfL⟩
    -- my aim: return the set t
    sorry
  trivial

[Eric Wieser]

The summary is that you can't construct data (computably) by splitting apart an existential; you need the axiom of choice

[Eric Wieser]

You can either write (hf x).choose and (hf x).choose_spec, or you can use the choose tactic as choose hf x with ... where I'm afraid you'll have to guess what to use for the ...

[Michael Rothgang]

Thanks. That solves it :-)