From 3aab45877b8a15f3ee24ab321d6f79b72401c916 Mon Sep 17 00:00:00 2001
From: yuanyi-350 <kysyy1@126.com>
Date: Sat, 26 Oct 2024 16:16:12 +0800
Subject: [PATCH] Update Finite.lean

---
 Others/Finite.lean | 36 ++++++++++--------------------------
 1 file changed, 10 insertions(+), 26 deletions(-)

diff --git a/Others/Finite.lean b/Others/Finite.lean
index db8df34..e441e8a 100644
--- a/Others/Finite.lean
+++ b/Others/Finite.lean
@@ -35,38 +35,22 @@ def Module.Finite.finiteOfFinite {R M : Type*} [CommRing R] [Finite R] [AddCommM
 
 variable {R : Type*} [CommRing R] [h : Module.Finite ℤ R]
 
-lemma My_Module.Finite.exists_fin' (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M]
+--Version issue: it's available in mathlib, but not in our library.
+lemma My_copy_Module.finite_of_finite (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M]
   [Finite R] [Module.Finite R M] : Finite M := by
   obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M;
-   exact .of_surjective f hf
+  exact .of_surjective f hf
 
 theorem Ideal.Quotient.finite_of_module_finite_int [IsDomain R]{I : Ideal R} (hp : I ≠ ⊥) : Finite (R ⧸ I) := by
   have : I.comap (algebraMap ℤ R) ≠ ⊥ := by
-    obtain ⟨x, hx1, hx2⟩ : ∃ x : R ,x ∈ I ∧ x ≠ 0 := by
-      have := mt (Submodule.eq_bot_iff I).mpr hp
-      push_neg at this
-      exact this
+    obtain ⟨x, hx1, hx2⟩ : ∃ x : R ,x ∈ I ∧ x ≠ 0 :=
+      Set.not_subset.mp <| mt (Submodule.eq_bot_iff I).mpr hp
     apply Ideal.comap_ne_bot_of_integral_mem hx2 hx1 <| Algebra.IsIntegral.isIntegral x
-
-  -- let f := (Ideal.Quotient.mk I).comp <| algebraMap ℤ R
-  -- have : ℤ ⧸ (f.toAddMonoidHom).ker ≃+ (f.toAddMonoidHom).range := by
-  --   exact QuotientAddGroup.quotientKerEquivRange f.toAddMonoidHom
-
-  have t1 : Module.Finite (ℤ ⧸ I.comap (algebraMap ℤ R)) (R ⧸ I) := by
-
-    sorry
-  have t2 : Finite (ℤ ⧸ I.comap (algebraMap ℤ R)) := by
-    -- have : IsPrincipalIdealRing ℤ := EuclideanDomain.to_principal_ideal_domain
-    have : Submodule.IsPrincipal (I.comap (algebraMap ℤ R)) :=
-      IsPrincipalIdealRing.principal (comap (algebraMap ℤ R) I)
-    have : ∃ a : ℤ , (I.comap (algebraMap ℤ R)) = span ({a}: Set ℤ) :=
-      Submodule.IsPrincipal.principal'
-    obtain ⟨a,ha⟩ := this
-    rw [ha]
-    -- refine finite_iff_exists_equiv_fin.mpr ?intro.a
-
-    sorry
-  exact My_Module.Finite.exists_fin' (ℤ ⧸ comap (algebraMap ℤ R) I)
+  have t1 : Module.Finite (ℤ ⧸ I.comap (algebraMap ℤ R)) (R ⧸ I) :=
+    Module.Finite.of_restrictScalars_finite ℤ (ℤ ⧸ I.comap (algebraMap ℤ R)) (R ⧸ I)
+  have t2 : Finite (ℤ ⧸ I.comap (algebraMap ℤ R)) :=
+    Int.Quotient.finite_of_ne_bot this
+  exact My_copy_Module.finite_of_finite (ℤ ⧸ comap (algebraMap ℤ R) I)
 
 -- `NoZeroSMulDivisors` can be removed
 instance Ideal.Quotient.finite_of_module_finite_int_of_isMaxiaml [NoZeroSMulDivisors ℤ R] [IsDomain R]