feat(Data.Set.Ncard): enat set cardinality (#5908)

This PR is a second attempt at defining the cardinality of a set as extended natural number, with a function `encard`. The implementation involves a refactor, where the existing`ncard` function is redefined in terms of `encard`. This shortens a lot of proofs, reduces reliance on the `Finset` API, and allows for a potential future refactor where `ncard` is removed if it is decided to be redundant.  



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Author: apnelson1

Mathlib/Data/ENat/Basic.lean

@@ -92,6 +92,10 @@ instance canLift : CanLift ℕ∞ ℕ (↑) fun n => n ≠ ⊤ :=
   WithTop.canLift
 #align enat.can_lift ENat.canLift
 
+instance : WellFoundedRelation ℕ∞ where
+  rel := (· < ·)
+  wf := IsWellFounded.wf
+
 /-- Conversion of `ℕ∞` to `ℕ` sending `∞` to `0`. -/
 def toNat : MonoidWithZeroHom ℕ∞ ℕ
     where
@@ -202,6 +206,9 @@ theorem le_of_lt_add_one (h : m < n + 1) : m ≤ n :=
   Order.le_of_lt_succ <| n.succ_def.symm ▸ h
 #align enat.le_of_lt_add_one ENat.le_of_lt_add_one
 
+theorem le_coe_iff {n : ℕ∞} {k : ℕ} : n ≤ ↑k ↔ ∃ (n₀ : ℕ), n = n₀ ∧ n₀ ≤ k :=
+  WithTop.le_coe_iff
+
 @[elab_as_elim]
 theorem nat_induction {P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ n : ℕ, P n → P n.succ)
     (htop : (∀ n : ℕ, P n) → P ⊤) : P a := by

Mathlib/Data/Set/Function.lean

@@ -1259,6 +1259,26 @@ theorem InjOn.invFunOn_image [Nonempty α] (h : InjOn f s₂) (ht : s₁ ⊆ s
   h.leftInvOn_invFunOn.image_image' ht
 #align set.inj_on.inv_fun_on_image Set.InjOn.invFunOn_image
 
+theorem _root_.Function.LeftInvOn_invFunOn_of_subset_image_image [Nonempty α]
+    (h : s ⊆ (invFunOn f s) '' (f '' s)) : LeftInvOn (invFunOn f s) f s :=
+  fun x hx ↦ by
+    obtain ⟨-, ⟨x, hx', rfl⟩, rfl⟩ := h hx
+    rw [invFunOn_apply_eq (f := f) hx']
+
+theorem injOn_iff_invFunOn_image_image_eq_self [Nonempty α] :
+    InjOn f s ↔ (invFunOn f s) '' (f '' s) = s :=
+  ⟨fun h ↦ h.invFunOn_image Subset.rfl, fun h ↦
+    (Function.LeftInvOn_invFunOn_of_subset_image_image h.symm.subset).injOn⟩
+
+theorem _root_.Function.invFunOn_injOn_image [Nonempty α] (f : α → β) (s : Set α) :
+    Set.InjOn (invFunOn f s) (f '' s) := by
+  rintro _ ⟨x, hx, rfl⟩ _ ⟨x', hx', rfl⟩ he
+  rw [←invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']
+
+theorem _root_.Function.invFunOn_image_image_subset [Nonempty α] (f : α → β) (s : Set α) :
+    (invFunOn f s) '' (f '' s) ⊆ s := by
+  rintro _ ⟨_, ⟨x,hx,rfl⟩, rfl⟩; exact invFunOn_apply_mem hx
+
 theorem SurjOn.rightInvOn_invFunOn [Nonempty α] (h : SurjOn f s t) :
     RightInvOn (invFunOn f s) f t := fun _y hy => invFunOn_eq <| h hy
 #align set.surj_on.right_inv_on_inv_fun_on Set.SurjOn.rightInvOn_invFunOn