diff --git a/Mathlib/Data/Finite/Card.lean b/Mathlib/Data/Finite/Card.lean
index 2ae24189dfbd4..9dba1fc2433b5 100644
--- a/Mathlib/Data/Finite/Card.lean
+++ b/Mathlib/Data/Finite/Card.lean
@@ -193,6 +193,17 @@ theorem card_subtype_lt [Finite α] {p : α → Prop} {x : α} (hx : ¬p x) :
 
 end Finite
 
+namespace PartENat
+
+theorem card_eq_coe_nat_card (α : Type _) [Finite α] : card α = Nat.card α := by
+  unfold PartENat.card
+  apply symm
+  rw [Cardinal.natCast_eq_toPartENat_iff]
+  exact Finite.cast_card_eq_mk
+#align part_enat.card_of_finite PartENat.card_eq_coe_nat_card
+
+end PartENat
+
 namespace Set
 
 theorem card_union_le (s t : Set α) : Nat.card (↥(s ∪ t)) ≤ Nat.card s + Nat.card t := by
@@ -206,4 +217,3 @@ theorem card_union_le (s t : Set α) : Nat.card (↥(s ∪ t)) ≤ Nat.card s +
 #align set.card_union_le Set.card_union_le
 
 end Set
-
diff --git a/Mathlib/Data/Nat/PartENat.lean b/Mathlib/Data/Nat/PartENat.lean
index 1c791c055e301..0ea546797d9e1 100644
--- a/Mathlib/Data/Nat/PartENat.lean
+++ b/Mathlib/Data/Nat/PartENat.lean
@@ -511,6 +511,10 @@ theorem add_one_le_iff_lt {x y : PartENat} (hx : x ≠ ⊤) : x + 1 ≤ y ↔ x
   norm_cast; apply Nat.lt_of_succ_le; norm_cast at h
 #align part_enat.add_one_le_iff_lt PartENat.add_one_le_iff_lt
 
+theorem coe_succ_le_iff {n : ℕ} {e : PartENat} : ↑n.succ ≤ e ↔ ↑n < e:= by
+  rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, add_one_le_iff_lt (natCast_ne_top n)]
+#align part_enat.coe_succ_le_succ_iff PartENat.coe_succ_le_iff
+
 theorem lt_add_one_iff_lt {x y : PartENat} (hx : x ≠ ⊤) : x < y + 1 ↔ x ≤ y := by
   refine ⟨le_of_lt_add_one, fun h => ?_⟩
   rcases ne_top_iff.mp hx with ⟨m, rfl⟩
@@ -521,6 +525,10 @@ theorem lt_add_one_iff_lt {x y : PartENat} (hx : x ≠ ⊤) : x < y + 1 ↔ x 
   norm_cast; apply Nat.lt_succ_of_le; norm_cast at h
 #align part_enat.lt_add_one_iff_lt PartENat.lt_add_one_iff_lt
 
+lemma lt_coe_succ_iff_le {x : PartENat} {n : ℕ} (hx : x ≠ ⊤) : x < n.succ ↔ x ≤ n :=
+by rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, lt_add_one_iff_lt hx]
+#align part_enat.lt_coe_succ_iff_le PartENat.lt_coe_succ_iff_le
+
 theorem add_eq_top_iff {a b : PartENat} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ := by
   refine PartENat.casesOn a ?_ ?_
   <;> refine PartENat.casesOn b ?_ ?_
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index 65c2f42469980..7b9922d7729ae 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -1690,6 +1690,12 @@ theorem cast_toNat_of_aleph0_le {c : Cardinal} (h : ℵ₀ ≤ c) : ↑(toNat c)
   rw [toNat_apply_of_aleph0_le h, Nat.cast_zero]
 #align cardinal.cast_to_nat_of_aleph_0_le Cardinal.cast_toNat_of_aleph0_le
 
+/-- Two finite cardinals are equal iff they are equal their to_nat are equal -/
+theorem toNat_eq_iff_eq_of_lt_aleph0 {c d : Cardinal} (hc : c < ℵ₀) (hd : d < ℵ₀) :
+    toNat c = toNat d ↔ c = d := by
+  rw [← natCast_inj, cast_toNat_of_lt_aleph0 hc, cast_toNat_of_lt_aleph0 hd]
+#align cardinal.to_nat_eq_iff_eq_of_lt_aleph_0 Cardinal.toNat_eq_iff_eq_of_lt_aleph0
+
 theorem toNat_le_iff_le_of_lt_aleph0 {c d : Cardinal} (hc : c < ℵ₀) (hd : d < ℵ₀) :
     toNat c ≤ toNat d ↔ c ≤ d := by
   rw [← natCast_le, cast_toNat_of_lt_aleph0 hc, cast_toNat_of_lt_aleph0 hd]
@@ -1880,6 +1886,85 @@ theorem toPartENat_surjective : Surjective toPartENat := fun x =>
   PartENat.casesOn x ⟨ℵ₀, toPartENat_apply_of_aleph0_le le_rfl⟩ fun n => ⟨n, toPartENat_cast n⟩
 #align cardinal.to_part_enat_surjective Cardinal.toPartENat_surjective
 
+theorem toPartENat_eq_top_iff_le_aleph0 {c : Cardinal} :
+  toPartENat c = ⊤ ↔ ℵ₀ ≤ c := by
+  cases lt_or_ge c ℵ₀ with
+  | inl hc =>
+    simp only [toPartENat_apply_of_lt_aleph0 hc, PartENat.natCast_ne_top, false_iff, not_le, hc]
+  | inr hc => simp only [toPartENat_apply_of_aleph0_le hc, eq_self_iff_true, true_iff]; exact hc
+#align to_part_enat_eq_top_iff_le_aleph_0 Cardinal.toPartENat_eq_top_iff_le_aleph0
+
+lemma toPartENat_le_iff_of_le_aleph0 {c c' : Cardinal} (h : c ≤ ℵ₀) :
+  toPartENat c ≤ toPartENat c' ↔ c ≤ c' := by
+  cases lt_or_ge c ℵ₀ with
+  | inl hc =>
+    rw [toPartENat_apply_of_lt_aleph0 hc]
+    cases lt_or_ge c' ℵ₀ with
+    | inl hc' =>
+      rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
+      exact toNat_le_iff_le_of_lt_aleph0 hc hc'
+    | inr hc' =>
+      simp only [toPartENat_apply_of_aleph0_le hc',
+      le_top, true_iff]
+      exact le_trans h hc'
+  | inr hc =>
+    rw [toPartENat_apply_of_aleph0_le hc]
+    simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0,
+    le_antisymm h hc]
+#align to_part_enat_le_iff_le_of_le_aleph_0 Cardinal.toPartENat_le_iff_of_le_aleph0
+
+lemma toPartENat_le_iff_of_lt_aleph0 {c c' : Cardinal} (hc' : c' < ℵ₀) :
+  toPartENat c ≤ toPartENat c' ↔ c ≤ c' := by
+  cases lt_or_ge c ℵ₀ with
+  | inl hc =>
+    rw [toPartENat_apply_of_lt_aleph0 hc]
+    rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
+    exact toNat_le_iff_le_of_lt_aleph0 hc hc'
+  | inr hc =>
+    rw [toPartENat_apply_of_aleph0_le hc]
+    simp only [top_le_iff, toPartENat_eq_top_iff_le_aleph0]
+    rw [← not_iff_not, not_le, not_le]
+    simp only [hc', lt_of_lt_of_le hc' hc]
+#align to_part_enat_le_iff_le_of_lt_aleph_0 Cardinal.toPartENat_le_iff_of_lt_aleph0
+
+lemma toPartENat_eq_iff_of_le_aleph0 {c c' : Cardinal} (hc : c ≤ ℵ₀) (hc' : c' ≤ ℵ₀) :
+  toPartENat c = toPartENat c' ↔ c = c' := by
+  rw [le_antisymm_iff, le_antisymm_iff, toPartENat_le_iff_of_le_aleph0 hc,
+    toPartENat_le_iff_of_le_aleph0 hc']
+#align to_part_enat_eq_iff_eq_of_le_aleph_0 Cardinal.toPartENat_eq_iff_of_le_aleph0
+
+theorem toPartENat_mono {c c' : Cardinal} (h : c ≤ c') :
+  toPartENat c ≤ toPartENat c' := by
+  cases lt_or_ge c ℵ₀ with
+  | inl hc =>
+    rw [toPartENat_apply_of_lt_aleph0 hc]
+    cases lt_or_ge c' ℵ₀ with
+    | inl hc' =>
+      rw [toPartENat_apply_of_lt_aleph0 hc', PartENat.coe_le_coe]
+      exact toNat_le_of_le_of_lt_aleph0 hc' h
+    | inr hc' =>
+        rw [toPartENat_apply_of_aleph0_le hc']
+        exact le_top
+  | inr hc =>
+      rw [toPartENat_apply_of_aleph0_le hc,
+      toPartENat_apply_of_aleph0_le (le_trans hc h)]
+#align cardinal.to_part_enat_mono Cardinal.toPartENat_mono
+
+theorem toPartENat_lift (c : Cardinal.{v}) : toPartENat (lift.{u, v} c) = toPartENat c := by
+  cases' lt_or_ge c ℵ₀ with hc hc
+  · rw [toPartENat_apply_of_lt_aleph0 hc, Cardinal.toPartENat_apply_of_lt_aleph0 _]
+    simp only [toNat_lift]
+    rw [lift_lt_aleph0]
+    exact hc
+  . rw [toPartENat_apply_of_aleph0_le hc, toPartENat_apply_of_aleph0_le _]
+    rw [aleph0_le_lift]
+    exact hc
+#align cardinal.to_part_enat_lift Cardinal.toPartENat_lift
+
+theorem toPartENat_congr {β : Type v} (e : α ≃ β) : toPartENat (#α) = toPartENat (#β) := by
+  rw [← toPartENat_lift, lift_mk_eq.{_, _,v}.mpr ⟨e⟩, toPartENat_lift]
+#align cardinal.to_part_enat_congr Cardinal.toPartENat_congr
+
 theorem mk_toPartENat_eq_coe_card [Fintype α] : toPartENat (#α) = Fintype.card α := by simp
 #align cardinal.mk_to_part_enat_eq_coe_card Cardinal.mk_toPartENat_eq_coe_card
 
diff --git a/Mathlib/SetTheory/Cardinal/Finite.lean b/Mathlib/SetTheory/Cardinal/Finite.lean
index 1bdaeffd7dffa..f776f85b3b1bd 100644
--- a/Mathlib/SetTheory/Cardinal/Finite.lean
+++ b/Mathlib/SetTheory/Cardinal/Finite.lean
@@ -149,4 +149,86 @@ theorem card_eq_top_of_infinite [Infinite α] : card α = ⊤ :=
   mk_toPartENat_of_infinite
 #align part_enat.card_eq_top_of_infinite PartENat.card_eq_top_of_infinite
 
+theorem card_congr {α : Type _} {β : Type _} (f : α ≃ β) : PartENat.card α = PartENat.card β :=
+  Cardinal.toPartENat_congr f
+#align part_enat.card_congr PartENat.card_congr
+
+theorem card_uLift (α : Type _) : card (ULift α) = card α :=
+  card_congr Equiv.ulift
+#align part_enat.card_ulift PartENat.card_uLift
+
+@[simp]
+theorem card_pLift (α : Type _) : card (PLift α) = card α :=
+  card_congr Equiv.plift
+#align part_enat.card_plift PartENat.card_pLift
+
+theorem card_image_of_injOn {α : Type u} {β : Type v} {f : α → β} {s : Set α} (h : Set.InjOn f s) :
+    card (f '' s) = card s :=
+  card_congr (Equiv.Set.imageOfInjOn f s h).symm
+#align part_enat.card_image_of_inj_on PartENat.card_image_of_injOn
+
+theorem card_image_of_injective {α : Type u} {β : Type v} (f : α → β) (s : Set α)
+    (h : Function.Injective f) : card (f '' s) = card s :=
+  card_image_of_injOn (Set.injOn_of_injective h s)
+#align part_enat.card_image_of_injective PartENat.card_image_of_injective
+
+-- Should I keeep the 6 following lemmas ?
+@[simp]
+theorem _root_.Cardinal.natCast_le_toPartENat_iff {n : ℕ} {c : Cardinal} :
+  ↑n ≤ toPartENat c ↔ ↑n ≤ c := by
+  rw [← toPartENat_cast n, toPartENat_le_iff_of_le_aleph0 (le_of_lt (nat_lt_aleph0 n))]
+#align cardinal.coe_nat_le_to_part_enat_iff Cardinal.natCast_le_toPartENat_iff
+
+@[simp]
+theorem _root_.Cardinal.toPartENat_le_natCast_iff {c : Cardinal} {n : ℕ} :
+  toPartENat c ≤ n ↔ c ≤ n := by
+  rw [← toPartENat_cast n, toPartENat_le_iff_of_lt_aleph0 (nat_lt_aleph0 n)]
+#align cardinal.to_part_enat_le_coe_nat_iff Cardinal.toPartENat_le_natCast_iff
+
+@[simp]
+theorem _root_.Cardinal.natCast_eq_toPartENat_iff {n : ℕ} {c : Cardinal} :
+  ↑n = toPartENat c ↔ ↑n = c := by
+  rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toPartENat_le_natCast_iff,
+    Cardinal.natCast_le_toPartENat_iff]
+#align cardinal.coe_nat_eq_to_part_enat_iff Cardinal.natCast_eq_toPartENat_iff
+
+@[simp]
+theorem _root_.Cardinal.toPartENat_eq_natCast_iff {c : Cardinal} {n : ℕ} :
+  Cardinal.toPartENat c = n ↔ c = n := by
+rw [eq_comm, Cardinal.natCast_eq_toPartENat_iff, eq_comm]
+#align cardinal.to_part_nat_eq_coe_nat_iff_eq Cardinal.toPartENat_eq_natCast_iff
+
+@[simp]
+theorem _root_.Cardinal.natCast_lt_toPartENat_iff {n : ℕ} {c : Cardinal} :
+  ↑n < toPartENat c ↔ ↑n < c := by
+  simp only [← not_le, Cardinal.toPartENat_le_natCast_iff]
+#align part_enat.coe_nat_lt_coe_iff_lt Cardinal.natCast_lt_toPartENat_iff
+
+@[simp]
+theorem _root_.Cardinal.toPartENat_lt_natCast_iff {n : ℕ} {c : Cardinal} :
+   toPartENat c < ↑n ↔ c < ↑n :=
+by simp only [← not_le, Cardinal.natCast_le_toPartENat_iff]
+#align lt_coe_nat_iff_lt Cardinal.toPartENat_lt_natCast_iff
+
+theorem card_eq_zero_iff_empty (α : Type _) : card α = 0 ↔ IsEmpty α := by
+  rw [← Cardinal.mk_eq_zero_iff]
+  conv_rhs => rw [← Nat.cast_zero]
+  simp only [← Cardinal.toPartENat_eq_natCast_iff]
+  simp only [PartENat.card, Nat.cast_zero]
+#align part_enat.card_eq_zero_iff_empty PartENat.card_eq_zero_iff_empty
+
+theorem card_le_one_iff_subsingleton (α : Type _) : card α ≤ 1 ↔ Subsingleton α := by
+  rw [← le_one_iff_subsingleton]
+  conv_rhs => rw [← Nat.cast_one]
+  rw [← Cardinal.toPartENat_le_natCast_iff]
+  simp only [PartENat.card, Nat.cast_one]
+#align part_enat.card_le_one_iff_subsingleton PartENat.card_le_one_iff_subsingleton
+
+theorem one_lt_card_iff_nontrivial (α : Type _) : 1 < card α ↔ Nontrivial α := by
+  rw [← Cardinal.one_lt_iff_nontrivial]
+  conv_rhs => rw [← Nat.cast_one]
+  rw [← natCast_lt_toPartENat_iff]
+  simp only [PartENat.card, Nat.cast_one]
+#align part_enat.one_lt_card_iff_nontrivial PartENat.one_lt_card_iff_nontrivial
+
 end PartENat