Show set with stricter restriction on finite set is finite

Stream: mathlib4

[An Qi Zhang]

Hello! I'm trying to show this lemma holds of a finite set, and was wondering if there are some useful Mathlib theorems or lemmas (the "API" of Mathlib in some sense) to prove this with? I'm also not sure what's the best way to identify which parts of Mathlib will help me with this lemma below, and also was wondering if anyone has any pointers on how navigate Mathlib for this.

This is the idea of what I want to show:

Consider a finite set s of n number of elements x that satisfy Prop p. If I know that from Prop q on x, I have p on x (q x -> p x, a potentially stricter restriction q), then I want to show the set t of x where x satisfies Prop q is a finite set of m elements that is either less than or equal to n.

And this is the lemma in a MWE left open:

import Mathlib

lemma Subtype.equiv_fin_impl_equiv_fin' {α} {n} {p q : α → Prop} (himpl : ∀ x, q x → p x)
  (f : {x // p x} ≃ Fin n) : ∃ m, m ≤ n ∧ Nonempty ({x // q x} ≃ Fin m) := by
    sorry

[Aaron Liu]

You can use the API around docs#Finite

[Kenny Lau]

@An Qi Zhang apart from the above excellent answer, I think I'd be interested to know what the context is.

[An Qi Zhang]

The local context around my question is:
I have this finite set s, of elements y that satisfy Prop p. I'm now declaring a set t of elements x, where x is in s, and x satisfies a Prop q. I also know any x satisfying Prop q satisfies Prop p, as q has more restrictions than p. Now because s is finite, t is also finite, since q can only restrict the elements of s.

The outer context around my question is:
This lemma will help me show t is also finite, by using the mpr of finite_iff_exists_equiv_fin. But I need to figure out how to show ∃ m, m ≤ n ∧ Nonempty ({x // q x} ≃ Fin m). Though it's not clear to me from the theorems in docs#Finite.

I want this finite "subset" tso I can then convert it into a list, sort it, and reason about the elements in the list.

[Kenny Lau]

@An Qi Zhang What is the context of the finite set s?

[Kenny Lau]

I'm asking because for almost any answer you can give me, I'm going to say that Finset is a better option

[Aaron Liu]

Or docs#Set.Finite

[An Qi Zhang]

@Kenny Lau Consider s to a Trace I'm reasoning about. I don't see an issue with it being a Finset. If I declare it as a Finset, how do I declare a Finset of elements of s? I think if define t with the set builder notation {x | x \in s} it'll get treated as a Set, and I'm back to square one:

import Mathlib

def T (s : Finset Nat) : Finset Nat := {x : Nat | x ∈ s} -- failed to synthesize Fintype ℕ

[Aaron Liu]

Do {x ∈ s | condition}

[Aaron Liu]

You still get a Finset Nat out at the end though

[Aaron Liu]

If you want a Finset s you can do {x : s | condition}

[Kenny Lau]

what do you mean by trace?

[An Qi Zhang]

@Aaron Liu That works, but if my Type is a subtype (instead of just Nat), then is there a similar analogue to get it to work for a subtype?

import Mathlib

def Nat.greater (m : Nat) : Type := {n : Nat // n > m}

def T (s : Finset Nat) (m : Nat) : Finset (Nat.greater m) := {x : Nat.greater m | x.val ∈ s} -- failed to synthesize Fintype m.greater

[An Qi Zhang]

@Kenny Lau Ah I mean a collection/set of operations, that apply/have some effect

[Aaron Liu]

An Qi Zhang said:

Aaron Liu That works, but if my Type is a subtype (instead of just Nat), then is there a similar analogue to get it to work for a subtype?

import Mathlib

def Nat.greater (m : Nat) : Type := {n : Nat // n > m}

def T (s : Finset Nat) (m : Nat) : Finset (Nat.greater m) := {x : Nat.greater m | x.val ∈ s} -- failed to synthesize Fintype m.greater

To compute a Finset you need an "algorithm" for listing out all the elements. What's the "algorithm" you want to use here?

[Aaron Liu]

I'm asking because there are two ways you can do this:

• construct t, the Finset of Nats at most m, then take s and subtract out t
• go through s and only keep the elements which are more than m, and discard the rest

[An Qi Zhang]

@Aaron Liu Here I don't have an "algorithm", I'm assuming the set is Finite, then apply Set.Finite.toFinset to get a Finset (like below). I suppose that means I have to use the second approach?

import Mathlib

def Nat.greater (m : Nat) : Type := {n : Nat // n > m}

structure Nats where
  ns : Set Nat
  finite : Finite ns

def T (s : Nats) (m : Nat) : Finset (Nat.greater m) :=
  {x : Nat.greater m | x.val ∈ (Set.Finite.toFinset s.finite)} -- failed to synthesize Fintype m.greater