# Zulip Chat Archive

## 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 `SetLike`

s, 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