Modify proof of Finite_as_lt_cardinal_ens

Moves a large part into a separate lemma.

theories/ZornsLemma/CardinalsEns.v

@@ -17,7 +17,7 @@ From Coq Require Import ClassicalChoice Description Program.Subset Lia.
 From ZornsLemma Require Import
   Cardinals CountableTypes CSB DecidableDec EnsemblesImplicit
   Families FunctionProperties FunctionPropertiesEns Image InverseImage
-  Powerset_facts Proj1SigInjective.
+  Powerset_facts Proj1SigInjective ReverseMath.AddSubtract.
 From Coq Require Import RelationClasses.
 
 Definition eq_cardinal_ens {A B : Type}
@@ -672,12 +672,14 @@ Proof.
     - specialize (Hf2 x1 Hx1 x0 Hx0 Hxx).
       specialize (Hf1 x0 Hx0). lia.
   }
-  assert (forall x : nat, In U x -> x = u \/ exists y : nat, In U y /\ x = f y) as HU0.
+  assert (forall x : nat,
+             In U x -> x = u \/ exists y : nat, In U y /\ x = f y) as HU0.
   { intros x Hx.
     destruct (Nat.eq_dec x u); auto.
     right.
     (* [y] must be the greatest element of [U] which satisfies [y < x]. *)
-    unshelve epose proof (nat_bounded_ens_has_max_dec (fun y => In U y /\ y < x) _ x)
+    unshelve epose proof (nat_bounded_ens_has_max_dec
+                            (fun y => In U y /\ y < x) _ x)
       as [y Hy].
     - intros k. unfold In.
       destruct (Nat.lt_ge_cases k x).
@@ -728,6 +730,78 @@ Proof.
   intros ?. apply classic.
 Qed.
 
+Lemma Finite_injective_image_dec {X Y : Type} (f : X -> Y)
+  (U : Ensemble X)
+  (HUdec : forall x y : X, In U x -> In U y -> x = y \/ x <> y) :
+  injective_ens f U -> Finite (Im U f) -> Finite U.
+Proof.
+  intros Hf Himg.
+  remember (Im U f) as V.
+  revert U Hf HUdec HeqV.
+  induction Himg as [|? ? ? y HAy].
+  { intros U Hf HUdec HeqV.
+    replace U with (@Empty_set X).
+    { constructor. }
+    apply Extensionality_Ensembles; split.
+    1: intros ? ?; contradiction.
+    intros x Hx.
+    apply (Im_def U f) in Hx.
+    rewrite <- HeqV in Hx.
+    contradiction.
+  }
+  intros U Hf HUdec HeqV.
+  assert (exists x, In U x /\ f x = y) as [x [Hx Hxy]].
+  { apply Im_inv. rewrite <- HeqV. right. constructor. }
+  subst.
+  replace U with (Add (Subtract U x) x).
+  2: {
+    symmetry.
+    apply Extensionality_Ensembles.
+    (* here we use [HUdec] *)
+    apply Add_Subtract_discouraging.
+    split; auto.
+  }
+  constructor.
+  2: apply Subtract_not_in.
+  apply IHHimg.
+  { intros x0 x1 Hx0 Hx1 Hxx.
+    destruct Hx0, Hx1.
+    apply Hf; assumption.
+  }
+  { intros x0 x1 Hx0 Hx1.
+    destruct Hx0, Hx1.
+    apply HUdec; assumption.
+  }
+  apply Extensionality_Ensembles; split.
+  - intros y Hy.
+    pose proof (Add_intro1 _ A (f x) y Hy) as Hy0.
+    rewrite HeqV in Hy0.
+    destruct Hy0 as [x0 Hx0 y Hy0].
+    subst. apply Im_def.
+    split; auto. intros ?.
+    destruct H. auto.
+  - intros y Hy.
+    destruct Hy as [x0 Hx0 y Hy].
+    subst. destruct Hx0.
+    pose proof (Im_def _ f x0 H).
+    rewrite <- HeqV in H1.
+    inversion H1; subst; clear H1; auto.
+    inversion H2; subst; clear H2.
+    (* here we use injectivity of [f] *)
+    apply Hf in H3; auto.
+    subst. contradict H0; constructor.
+Qed.
+
+Lemma Finite_injective_image {X Y : Type} (f : X -> Y)
+  (U : Ensemble X) :
+  injective_ens f U -> Finite (Im U f) -> Finite U.
+Proof.
+  intros Hf Himg.
+  apply Finite_injective_image_dec with f; auto.
+  intros ? ? ? ?.
+  apply classic.
+Qed.
+
 Lemma Finite_as_lt_cardinal_ens
   {X : Type} (U : Ensemble X) :
   Finite U <-> lt_cardinal_ens U (@Full_set nat).
@@ -803,60 +877,14 @@ Proof.
     }
     destruct H as [n Hn].
     (* [n] is an upper bound of the image of [U] under [f] *)
-    clear H2.
-    revert U Hf0 Hf1 Hn.
-    induction n.
-    { (* n = 0 *)
-      intros.
-      assert (U = Empty_set).
-      { apply Extensionality_Ensembles; split.
-        2: intros x Hx; contradiction.
-        intros x Hx.
-        specialize (Hn x Hx).
-        apply Nat.nlt_0_r in Hn.
-        contradiction.
-      }
-      subst. constructor.
+    assert (Finite (Im U f)).
+    { apply nat_Finite_bounded_char.
+      exists n. intros m Hm.
+      destruct Hm as [x Hx m Hm]; subst.
+      apply Hn; auto.
     }
-    (* n = S _ *)
-    intros U Hf0 Hf1 Hn.
-    destruct (classic (exists x : X, In U x /\ f x = n)) as [H|H].
-    2: {
-      (* apply the inductive hypothesis directly *)
-      apply IHn; auto.
-      intros x Hx.
-      specialize (Hn x Hx).
-      rewrite Nat.lt_succ_r in Hn.
-      destruct Hn.
-      - contradiction H.
-        exists x; split; auto.
-      - apply Arith_prebase.le_lt_n_Sm.
-        assumption.
-    }
-    destruct H as [x [HUx Hfx]].
-    assert (U = Add (Subtract U x) x).
-    { apply Extensionality_Ensembles; split;
-        auto using add_soustr_1, add_soustr_2.
-    }
-    rewrite H.
-    constructor.
-    2: now apply Subtract_not_in.
-    apply IHn.
-    + apply range_char_Im.
-      intros ? ?. constructor.
-    + intros x0 x1 Hx0 Hx1 Hx.
-      apply Hf1; auto.
-      * apply Hx0.
-      * apply Hx1.
-    + intros y Hy.
-      destruct Hy.
-      specialize (Hn y H0).
-      rewrite Nat.lt_succ_r in Hn.
-      destruct Hn.
-      * apply Hf1 in Hfx; auto. subst.
-        contradict H1. constructor.
-      * apply Arith_prebase.le_lt_n_Sm.
-        assumption.
+    apply Finite_injective_image with f;
+      auto.
 Qed.
 
 Lemma Countable_as_le_cardinal_ens {X : Type} (U : Ensemble X) :