Converse to `Finset.equivOfCardEq`

Stream: Is there code for X?

[Jz Pan]

I tried Loogle but it seems that we don't have the converse to docs#Finset.equivOfCardEq

Finset.equivOfCardEq Mathlib.Data.Fintype.Card
{α : Type u_1} → {s t : Finset α} → Finset.card s = Finset.card t → { x // x ∈ s } ≃ { x // x ∈ t }

Although it easily comes from existing results:

lemma Finset.card_eq_of_equiv {α : Type u} {s t : Finset α} (i : s ≃ t) : s.card = t.card :=
  Fin.equiv_iff_eq.1 <| Nonempty.intro <| (s.equivFin.symm.trans i).trans t.equivFin

[Jz Pan]

Or shorter Fin.equiv_iff_eq.1 ⟨(s.equivFin.symm.trans i).trans t.equivFin⟩.

Other possible proofs:

lemma Finset.card_eq_of_equiv {α : Type u} {s t : Finset α} (i : s ≃ t) : s.card = t.card := by
  simpa only [Fintype.card_coe] using Fintype.card_eq.2 ⟨i⟩

[Jz Pan]

So this is basically Fintype.card_eq.