Prop3d12

lemma prop3d12 {R : Type*} [CommRing R] [IsNoetherianRing R]{M : Type*} [Nontrivial M] [AddCommGroup M] [Module R M] [Module.Finite R M] :∀ I : {z: (ℒ R M) × (ℒ R M) // z.1 < z.2}, μA (μ R M) I =  ({(((_μ R M) I).toFinset.min' (μ_nonempty I))} : S₀ R) := by  intro I  simp only [Function.Embedding.toFun_eq_coe, RelEmbedding.coe_toEmbedding]  unfold μA  simp only [μmax_eq_μ, ne_eq]  unfold μ  have res1 : (OrderTheory.coe' {(_μ R M I).toFinset.min' (μ_nonempty I)} : S R) ∈    {x | ∃ a, ∃ (h : InIntvl I a ∧ ¬a = I.val.2), OrderTheory.coe'    (_μ R M ⟨(a, I.val.2), lt_of_le_of_ne h.1.2 h.2⟩).toFinset = x} := by    simp only [Set.mem_setOf_eq, EmbeddingLike.apply_eq_iff_eq]    use ker_of_quot_comp_localization I    constructor    · conv_lhs => unfold _μ      simp only [associated_primes_quot_koqcl I, Set.mem_singleton_iff, exists_prop_eq,        Set.setOf_eq_eq_singleton', Set.toFinset_singleton, Finset.singleton_inj]      rfl    · constructor      · constructor        · unfold ker_of_quot_comp_localization          intro z hz          simp only [Submodule.mem_map, LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk,            AddHom.coe_mk, Function.comp_apply, Submodule.subtype_apply, Subtype.exists,            exists_and_right, exists_eq_right]          use (le_of_lt I.prop) hz          have : Submodule.Quotient.mk ⟨z, (Iff.of_eq (Eq.refl (z ∈ I.val.2))).mpr            (le_of_lt (Subtype.prop I) hz) ⟩ =            (0 : ↥I.val.2 ⧸ Submodule.submoduleOf I.val.1 I.val.2)            := by simpa only [Submodule.Quotient.mk_eq_zero]          simp only [Submodule.mkQ_apply, this, LocalizedModule.mkLinearMap_apply,            LocalizedModule.zero_mk]        · unfold ker_of_quot_comp_localization          simp only [Submodule.map_subtype_le]      · by_contra hc        have := (((_μ R M) I).toFinset.min'_mem (μ_nonempty I))        simp only [Set.mem_toFinset, Set.mem_setOf_eq] at this        rcases this with ⟨p,⟨hp1,hp2⟩⟩        apply mem_support_of_mem_associatedPrimes at hp1        replace hp1 := hp1.out        have : LinearMap.ker (CP.f1 I) ≠ ⊤ := by          by_contra hc          apply LocalizedModule.subsingleton_iff_ker_eq_top.2 at hc          rw [hp2] at hp1          exact false_of_nontrivial_of_subsingleton (LocalizedModule            ((_μ R M I).toFinset.min' (μ_nonempty I)).asIdeal.primeCompl            (↥I.val.2 ⧸ Submodule.submoduleOf I.val.1 I.val.2))        have : ∃ m : (↥I.val.2 ⧸ Submodule.submoduleOf I.val.1 I.val.2), (CP.f1 I) m ≠ 0 := by          by_contra hc          push Not at hc          have this' : LinearMap.ker (CP.f1 I) = ⊤ := Submodule.ext fun z ↦            { mp := fun hz ↦ True.intro, mpr := fun hz ↦ hc z }          exact this this'        rcases this with ⟨m,hm⟩        unfold ker_of_quot_comp_localization at hc        have this' : (CP.f1 I ∘ₗ CP.f2 I) m.out = 0 := by          have : m.out.val ∈ Submodule.map (Submodule.subtype I.val.2)            (LinearMap.ker (CP.f1 I ∘ₗ CP.f2 I)) := by            have := m.out.prop            conv at this =>              arg 1; simp only [← hc]            exact this          simp only [ne_eq, LinearMap.ker_eq_top, LocalizedModule.mkLinearMap_apply,            Submodule.mem_map, LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk,            Submodule.mkQ_apply, AddHom.coe_mk, Function.comp_apply, Submodule.subtype_apply,            SetLike.coe_eq_coe, exists_eq_right] at *          exact this        unfold CP.f2 at this'        simp only [Submodule.mkQ_apply, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk,          Function.comp_apply] at this'        unfold Submodule.Quotient.mk Quotient.mk'' at this'        rw [Quotient.out_eq] at this'        exact hm this'  apply IsLeast.csInf_eq  refine ⟨res1,?_⟩  apply mem_lowerBounds.2  rintro N ⟨a,ha1,ha2⟩  rw [← ha2]  simp only [Function.Embedding.toFun_eq_coe, RelEmbedding.coe_toEmbedding,    OrderEmbedding.le_iff_le]  exact prop3d12p2 I a ha1.1 ha1.2