Cast to a subset, given proof of inclusion

Stream: new members

[Michael Rothgang]

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]

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]

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]

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

[Michael Rothgang]

@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]

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

[Kevin Buzzard]

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]

@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]

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]

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]

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]

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]

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]

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]

Thanks so much for the quick and exhaustive responses!