How to prove fin subtype with stricter restriction is fin

Stream: new members

[An Qi Zhang]

Hello, I have this problem narrowed down to a lemma I want to prove, where if I know a subtype a of elements that satisfy restriction p is finite with n elements, and I know if restriction q holds for an element x implies p holds for x as well, then the subtype b where q holds for elements of x is a finite subtype of the same or smaller size m.

Now intuitively, restriction q must be either as strict as p, or stricter, if q holds for x implies p holds for x to be true, so it makes sense for the subtype b to have the same or less m number of elements.

This sounds straightforward, however, I'm struggling with trying to get this intuition into Lean and Mathlib, and prove this lemma below, and was wondering if anyone has an idea on how to write this intuition in Lean / Mathlib?

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

[Matt Diamond]

if you interpret p and q as sets instead of functions to Prop, what you're trying to prove is essentially docs#Set.ncard_le_ncard, as himpl becomes the hypothesis that q is a subset of p

[Matt Diamond]

in that case, m would simply be q.ncard

[Matt Diamond]

you could also use docs#Nat.card_mono

[Matt Diamond]

For example:

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
  use Nat.card {x | q x}
  have p_finite : Finite {x | p x} := Finite.of_equiv _ f.symm
  have q_finite : Finite {x | q x} := Finite.Set.subset {x | p x} himpl
  rw [← Nat.card_eq_of_equiv_fin f]
  exact ⟨Nat.card_mono p_finite himpl, ⟨Finite.equivFin {x | q x}⟩⟩

[Matt Diamond]

there's a little bit of defeq abuse here but you get the idea

[Matt Diamond]

actually it looks like the proof works with subtypes (though I suspect this is also defeq abuse):

import Mathlib

lemma Subtype.equiv_fin_impl_equiv_fin' {α : Type*} {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
  use Nat.card {x // q x}
  have p_finite : Finite {x | p x} := Finite.of_equiv _ f.symm
  have q_finite : Finite {x | q x} := Finite.Set.subset {x | p x} himpl
  rw [← Nat.card_eq_of_equiv_fin f]
  exact ⟨Nat.card_mono p_finite himpl, ⟨Finite.equivFin {x | q x}⟩⟩

[Matt Diamond]

I guess it works because a set coerced to a type is a subtype, so they're the same thing

[Matt Diamond]

oh, docs#Cardinal.mk_subtype_mono would allow you to talk about the cardinalities without referring to sets

[Matt Diamond]

here's a proof using Cardinal.mk_subtype_mono:

import Mathlib

lemma Subtype.equiv_fin_impl_equiv_fin' {α : Type*} {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
  have := Cardinal.mk_subtype_mono himpl
  rw [Cardinal.le_def] at this
  obtain ⟨map, map_inj⟩ := this
  have finite_p : Finite { x // p x } := Finite.of_equiv _ f.symm
  have finite_q : Finite { x // q x } := Finite.of_injective map map_inj
  rw [← Nat.card_eq_of_equiv_fin f]
  exact ⟨
    Nat.card {x // q x},
    Nat.card_le_card_of_injective map map_inj,
    ⟨Finite.equivFin {x // q x}⟩
  ⟩

[An Qi Zhang]

Awesome, thanks! I wouldn't have been able to figure out the right theorems to use from Mathlib you! This has also helped me learn a bit more about the theorems that are in Mathlib, and working with Lean in general.

In principle, I assume it's better not to abuse definitional equality? And in the last field in exact's constructor, does ⟨Finite.equivFin {x // q x}⟩ satisfy Nonempty ({x // q x} ≃ Fin m) because a Finite type is non-empty?

[Matt Diamond]

It satisfies it because Finite.equivFin {x // q x} is the equivalence and the brackets ⟨...⟩ are serving as the constructor for Nonempty

[Matt Diamond]

in this context, ⟨Finite.equivFin {x // q x}⟩ is the same as Nonempty.intro (Finite.equivFin {x // q x})

[Matt Diamond]

and you can see that docs#Finite.equivFin provides us with a term of type {x // q x} ≃ Fin (Nat.card {x // q x}), which satisfies {x // q x} ≃ Fin m because m is equal to Nat.card {x // q x}

[Matt Diamond]

and yes, it's generally a good idea to avoid abusing definitional equality since it means your code will break if the underlying definitions change