## Stream: new members

### Topic: Cast to a subset, given proof of inclusion

#### Michael Rothgang (Sep 19 2023 at 13:31):

Given subsets s and t of a set X with $s\subseteq t$, can I "coerce" (unsure what the proper term is) $s$ to a subset of $t$? I have a proof that the inclusion holds, after all.

(I know standard coercions go from a subset of $s$ to a subset of $X$, not the other way around.)

#### Jireh Loreaux (Sep 19 2023 at 14:15):

Can you provide types on the above variables? Otherwise it's hard to know what needs coercing. As written, it didn't look to me like anything needed it.

#### Anne Baanen (Sep 19 2023 at 14:39):

Is this the question?

def toSubset {X : Type*} (s t : Set X) (h : s  t) : Set t := sorry

lemma mem_toSubset {X : Type*} (s t : Set X) (h : s  t)
(x : t) : x  toSubset s t h  x  s := sorry

#### Eric Wieser (Sep 19 2023 at 14:41):

(note that $\LaTeX$ requires double dollars in Zulip, even though it's inline)

#### Michael Rothgang (Sep 19 2023 at 14:42):

@Anne Baanen Indeed, that's the question.
$s$ and $t$ are both subsets of $X$, we know $s\subseteq t$ and want to regard $s$ as a subset of $t$. Thank you.

#### Anne Baanen (Sep 19 2023 at 14:43):

I can't find anything like this :( I know we have it for other SetLikes, such as docs#Submodule.ofLe

#### Kevin Buzzard (Sep 19 2023 at 15:42):

In lean "s is a subset of t" doesn't typecheck, because a subset is a term but things which have subsets must be types. This is why Jireh is asking what you actually mean. Anne is guessing, but only you know the answer :-)

#### Michael Rothgang (Sep 19 2023 at 16:41):

@Kevin Buzzard I'm aware of the distinction (though apparently I didn't phrase my question well!). Thanks for pointing out that I can be more precise in my questions.

#### Michael Rothgang (Sep 19 2023 at 16:46):

Indeed, Anne's code stub does what I need: if s and t are of type Set X (where X is a Type), and h is a proof that $s \subseteq t$, I'm looking for a way to cast s to type Set t.

#### Michael Rothgang (Sep 19 2023 at 16:48):

Anne's stub suffices for my purposes right now. At some point, I can prove at PR it. (Not my top priority, though - so unlikely to happen soon.)

#### Jireh Loreaux (Sep 19 2023 at 17:09):

There's some stuff of this variety in file#Data/Set/Functor, but I don't think we have exactly what you are looking for.

#### Kevin Buzzard (Sep 19 2023 at 17:29):

Michael Rothgang said:

Kevin Buzzard I'm aware of the distinction (though apparently I didn't phrase my question well!). Thanks for pointing out that I can be more precise in my questions.

The best way to ask a question on this forum is to post fully working code (with e.g. a sorry saying "how do I solve this goal" or "how do I complete this definition"); this way there is no ambiguity at all.

#### Jireh Loreaux (Sep 19 2023 at 17:38):

And also, I'm not entirely sure how you want to use the hypothesis h : s ⊆ t. What I mean is that this works just fine, and you get the following lemmas:

import Mathlib.Data.Set.Functor

namespace Set

variable {X : Type*} (s t : Set X)

/-- Given sets s t : Set X, Set.toSubset s t is s ∩ t realized as a term of Set t. -/
def toSubset : Set t := (Subtype.val ·  s)

@[simp]
lemma mem_toSubset (x : t) : x  toSubset s t  x  s := Iff.rfl

@[simp]
lemma coe_toSubset : (s.toSubset t : Set X) = s  t := by
ext
refine fun h  ?_, fun h  _, ⟨⟨_, h.2⟩, rfl⟩, by simpa using h.1, rfl⟩⟩⟩
· obtain -, a, rfl⟩, ha := h
simp only [mem_toSubset, pure_def, mem_iUnion, mem_singleton_iff, exists_prop] at ha
obtain ha, rfl := ha
exact ha, a.property

#### Kyle Miller (Sep 19 2023 at 21:22):

For Anne's formulation, you can piece together docs#Set.range and docs#Set.inclusion

def toSubset {X : Type*} (s t : Set X) (h : s  t) : Set t :=
Set.range (Set.inclusion h)

lemma mem_toSubset {X : Type*} (s t : Set X) (h : s  t) (x : t) :
x  toSubset s t h  x  s := by
rw [toSubset, Set.range_inclusion]
rfl -- or rw [Set.mem_setOf_eq]

#### Michael Rothgang (Sep 19 2023 at 22:19):

Thanks so much for the quick and exhaustive responses!

Last updated: Dec 20 2023 at 11:08 UTC