Cast term to a subtype

Stream: new members

[Michael Rothgang]

Given a type X, a term x : X, a subset S of X (i.e. S : Set X) and a proof that x : S, how can I cast x to type S?
Lean code (with a small caveat: I want something slightly stronger, namely that I've cast x as opposed to choosing some random element of S, see below):

lemma cast_to_subtype {X : Type*} {S : Set X} (x : X) (hx : x ∈ S) : S := sorry

[Michael Rothgang]

To elaborate more and un-#xy, this is the context I need this in.

theorem context_reduced {X Y : Type*} (S : Set (Set X)) (f : Y → ↑S) (hf : Function.Surjective f)
  {x : X} {s : Set X} (h : s ∈ S) (hxs : x ∈ s) : x ∈ ⋃ (y : Y), ↑(f y) := by
  -- Choose y with f y = s.
  have : ∀ s : ↑S, ∃ y : Y, f y = s := hf
  -- Using cast_to_subtype, somehow turn y into an element of s. Need HELP here!
  have : ∃ y, f y = s := by sorry
  rcases this with ⟨n, hn⟩
  exact ⟨f n, mem_range_self n, (by rw [hn]; exact hxs)⟩

[Eric Wieser]

Your first sorry is ⟨x, hx⟩

[Anatole Dedecker]

⟨s, h⟩ should work for the second sorry

[Eric Wieser]

Aka docs#Subtype.mk

[Anatole Dedecker]

To explain the syntax, you can have a look at docs#Subtype and see that elements of Subtype p are just pairs ⟨x, hx⟩ where x : X and hx : p x.

[Michael Rothgang]

The first sorry works; the second one doesn't. However, I can fix the proof as follows (the last line was suggested by aesop):

theorem context_reduced {X Y : Type*} (S : Set (Set X)) (f : Y → ↑S) (hf : Function.Surjective f)
  {x : X} {s : Set X} (h : s ∈ S) (hxs : x ∈ s) : x ∈ ⋃ (y : Y), ↑(f y) := by
  -- Choose y with f y = s.
  have : ∃ y, f y = s := by
    obtain ⟨y, hy⟩ := hf ⟨s, h⟩
    use y
    simp_all only [Subtype.forall]
  rcases this with ⟨n, hn⟩
  exact ⟨f n, mem_range_self n, (by rw [hn]; exact hxs)⟩

[Anatole Dedecker]

Right I wrote too fast: I gave the solution to the first sorry but with the notations of the second :face_palm: