## Stream: new members

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

#### Michael Rothgang (Sep 22 2023 at 12:44):

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 (Sep 22 2023 at 12:51):

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

#### Eric Wieser (Sep 22 2023 at 12:51):

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 (Sep 22 2023 at 20:18):

Thanks. That solves it :-)

Last updated: Dec 20 2023 at 11:08 UTC