A finite image has a finite preimage with a same cardinality

Stream: general

[Hagb (Junyu Guo)]

I formalized it when I needed it in an other theorem. Has it been in Mathlib yet? (If not yet) is it worth being submitted to Mathlib?
Also I think it might have a shorter proof with more advanced tools.

import Mathlib.Data.Set.Finite
import Mathlib.Data.Finset.Basic
lemma finset_subset_preimage_of_finite_image {α : Type _} {β : Type _}
    {s : Set α} {f : α → β} (h : (f '' s).Finite) :
    ∃ (s' : Finset α), s'.toSet ⊆ s ∧ f '' s' = f '' s ∧ s'.card = h.toFinset.card := by
  have := s.mem_image f
  rw [←h.coe_toFinset] at this
  by_cases h' : s = ∅
  · use ∅; simp [h']
  ·
    classical
    cases' Set.nonempty_iff_ne_empty.mpr h' with a ha
    let s' := h.toFinset.image fun (x : β) =>
      if hx : x ∈ h.toFinset
        then ((this x).mp (hx)).choose
        else a
    have hs' : s'.toSet ⊆ s := by
      intro x hx
      simp [s'] at hx
      let ⟨y, hy, hy'⟩ := hx
      rw [←hy']
      have hxy: ∃ x ∈ s, f x = f y := by use y, hy
      simp [hxy, hxy.choose_spec]
    use s'
    constructor
    ·exact hs'
    constructor
    ·
      apply Set.eq_of_subset_of_subset
      ·exact Set.image_subset _ hs'
      ·
        intro y hy
        simp at hy
        let ⟨x,hx, hxy⟩ := hy
        simp [s']
        use x
        simp [hx, hxy, hy, hy.choose_spec]
    ·
      simp_rw [s', Finset.card_image_iff, Set.InjOn]
      intro x₁ hx₁ x₂ hx₂
      simp at hx₁ hx₂
      simp [hx₁, hx₂]
      intro hx₁x₂
      rw [←hx₂.choose_spec.2, ←hx₁.choose_spec.2, hx₁x₂]

Edited: adjusted coding style

[Floris van Doorn]

This proof should be a lot shorter when using docs#Set.exists_subset_bijOn.

[Hagb (Junyu Guo)]

Floris van Doorn said:

This proof should be a lot shorter when using docs#Set.exists_subset_bijOn.

Thanks! (And sorry for my late reply.) It is now a lot shorter:

import Mathlib.Data.Set.Finite.Basic
namespace Set

lemma card_bijOn {α β : Type*} {s : Finset α} {t : Finset β}
    (i : α → β) (h : Set.BijOn i s t) : s.card = t.card :=
  Finset.card_nbij i h.mapsTo h.injOn h.surjOn

lemma finset_subset_preimage_of_finite_image {α : Type*} {β : Type*}
    {s : Set α} {f : α → β} (h : (f '' s).Finite) :
    ∃ (s' : Finset α), ↑s' ⊆ s ∧ f '' s' = f '' s ∧ s'.card = h.toFinset.card := by
  have ⟨s', hs', hs'₁⟩ := Set.exists_subset_bijOn s f
  have h' := Set.Finite.of_finite_image (hs'₁.image_eq.symm ▸ h) hs'₁.injOn
  use h'.toFinset
  rw [Set.Finite.coe_toFinset]
  exact ⟨hs', hs'₁.image_eq, card_bijOn _ <| h.coe_toFinset.symm ▸ h'.coe_toFinset.symm ▸ hs'₁⟩

edit: refine -> exact
edit: define card_bijOn instead of a helper theorem that convert BijOn to "bij"