Zulip Chat Archive

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

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