feat(RingTheory): golf IsPrincipalIdealRing.of_prime (leanprover-community#28477)

In complement to leanprover-community#28451 and as discussed in leanprover-community#27200, this PR uses the newly added Oka predicates to golf the proof of `IsPrincipalIdealRing.of_prime`.

Co-authored-by: Marc Robin <[email protected]>

Author: yapudpill

Mathlib/RingTheory/PrincipalIdealDomain.lean

@@ -18,7 +18,7 @@ principal ideal domain (PID) is an integral domain which is a principal ideal ri
 
 The definition of `IsPrincipalIdealRing` can be found in `Mathlib/RingTheory/Ideal/Span.lean`.
 
-# Main definitions
+## Main definitions
 
 Note that for principal ideal domains, one should use
 `[IsDomain R] [IsPrincipalIdealRing R]`. There is no explicit definition of a PID.
@@ -28,7 +28,7 @@ Theorems about PID's are in the `PrincipalIdealRing` namespace.
 - `generator`: a generator of a principal ideal (or more generally submodule)
 - `to_uniqueFactorizationMonoid`: a PID is a unique factorization domain
 
-# Main results
+## Main results
 
 - `Ideal.IsPrime.to_maximal_ideal`: a non-zero prime ideal in a PID is maximal.
 - `EuclideanDomain.to_principal_ideal_domain` : a Euclidean domain is a PID.
@@ -482,35 +482,77 @@ end
 
 section PrincipalOfPrime
 
-open Set Ideal
+namespace Ideal
+
+variable (R) [Semiring R]
+
+/-- `nonPrincipals R` is the set of all ideals of `R` that are not principal ideals. -/
+abbrev nonPrincipals := { I : Ideal R | ¬I.IsPrincipal }
+
+variable {R}
+
+theorem nonPrincipals_eq_empty_iff : nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R := by
+  simp [Set.eq_empty_iff_forall_notMem, isPrincipalIdealRing_iff]
+
+/-- Any chain in the set of non-principal ideals has an upper bound which is non-principal.
+(Namely, the union of the chain is such an upper bound.)
+
+If you want the existence of a maximal non-principal ideal see
+`Ideal.exists_maximal_not_isPrincipal`. -/
+theorem nonPrincipals_zorn (hR : ¬IsPrincipalIdealRing R) (c : Set (Ideal R))
+    (hs : c ⊆ nonPrincipals R) (hchain : IsChain (· ≤ ·) c) :
+    ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I := by
+  by_cases H : c.Nonempty
+  · obtain ⟨K, hKmem⟩ := Set.nonempty_def.1 H
+    refine ⟨sSup c, fun ⟨x, hx⟩ ↦ ?_, fun _ ↦ le_sSup⟩
+    have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
+    obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem
+    have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
+    exact hs hJc ⟨hsSupJ ▸ ⟨x, hx⟩⟩
+  · simpa [Set.not_nonempty_iff_eq_empty.1 H, isPrincipalIdealRing_iff] using hR
+
+theorem exists_maximal_not_isPrincipal (hR : ¬IsPrincipalIdealRing R) :
+    ∃ I : Ideal R, Maximal (¬·.IsPrincipal) I :=
+  zorn_le₀ _ (nonPrincipals_zorn hR)
+
+end Ideal
+
+end PrincipalOfPrime
+
+section PrincipalOfPrime_old
 
 variable (R) [CommRing R]
 
 /-- `nonPrincipals R` is the set of all ideals of `R` that are not principal ideals. -/
+@[deprecated Ideal.nonPrincipals (since := "2025-09-30")]
 def nonPrincipals :=
   { I : Ideal R | ¬I.IsPrincipal }
 
-theorem nonPrincipals_def {I : Ideal R} : I ∈ nonPrincipals R ↔ ¬I.IsPrincipal :=
+@[deprecated "Not necessary anymore since Ideal.nonPrincipals is an abrev." (since := "2025-09-30")]
+theorem nonPrincipals_def {I : Ideal R} : I ∈ { I : Ideal R | ¬I.IsPrincipal } ↔ ¬I.IsPrincipal :=
   Iff.rfl
 
 variable {R}
 
-theorem nonPrincipals_eq_empty_iff : nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R := by
-  simp [Set.eq_empty_iff_forall_notMem, isPrincipalIdealRing_iff, nonPrincipals_def]
+@[deprecated Ideal.nonPrincipals_eq_empty_iff (since := "2025-09-30")]
+theorem nonPrincipals_eq_empty_iff :
+    { I : Ideal R | ¬I.IsPrincipal } = ∅ ↔ IsPrincipalIdealRing R := by
+  simp [Set.eq_empty_iff_forall_notMem, isPrincipalIdealRing_iff]
 
 /-- Any chain in the set of non-principal ideals has an upper bound which is non-principal.
 (Namely, the union of the chain is such an upper bound.)
 -/
-theorem nonPrincipals_zorn (c : Set (Ideal R)) (hs : c ⊆ nonPrincipals R)
+@[deprecated Ideal.nonPrincipals_zorn (since := "2025-09-30")]
+theorem nonPrincipals_zorn (c : Set (Ideal R)) (hs : c ⊆ { I : Ideal R | ¬I.IsPrincipal })
     (hchain : IsChain (· ≤ ·) c) {K : Ideal R} (hKmem : K ∈ c) :
-    ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I := by
+    ∃ I ∈ { I : Ideal R | ¬I.IsPrincipal }, ∀ J ∈ c, J ≤ I := by
   refine ⟨sSup c, ?_, fun J hJ => le_sSup hJ⟩
   rintro ⟨x, hx⟩
   have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
   obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem
   have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
   specialize hs hJc
-  rw [← hsSupJ, hx, nonPrincipals_def] at hs
+  rw [← hsSupJ, hx] at hs
   exact hs ⟨⟨x, rfl⟩⟩
 
-end PrincipalOfPrime
+end PrincipalOfPrime_old

Mathlib/RingTheory/PrincipalIdealDomainOfPrime.lean

@@ -3,63 +3,49 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
-import Mathlib.RingTheory.Ideal.Colon
+import Mathlib.RingTheory.Ideal.Oka
 import Mathlib.RingTheory.PrincipalIdealDomain
 
 /-!
 # Principal ideal domains and prime ideals
 
-# Main results
+## Main results
 
-- `IsPrincipalIdeal.of_prime`: a ring where all prime ideals are principal is a principal ideal ring
+- `IsPrincipalIdealRing.of_prime`: a ring where all prime ideals are principal is a principal ideal
+  ring.
 -/
 
-open Ideal
+variable {R : Type*} [CommSemiring R]
+
+namespace Ideal
+
+/-- `Submodule.IsPrincipal` is an Oka predicate. -/
+theorem isOka_isPrincipal : IsOka (Submodule.IsPrincipal (R := R)) where
+  top := top_isPrincipal
+  oka {I a} := by
+    intro ⟨x, hx⟩ ⟨y, hy⟩
+    refine ⟨x * y, le_antisymm ?_ ?_⟩ <;> rw [submodule_span_eq] at *
+    · intro i hi
+      have hisup : i ∈ I ⊔ span {a} := mem_sup_left hi
+      have hasup : a ∈ I ⊔ span {a} := mem_sup_right (mem_span_singleton_self a)
+      rw [hx, mem_span_singleton'] at hisup hasup
+      obtain ⟨u, rfl⟩ := hisup
+      obtain ⟨v, rfl⟩ := hasup
+      obtain ⟨z, rfl⟩ : ∃ z, z * y = u := by
+        rw [← mem_span_singleton', ← hy, mem_colon_singleton, mul_comm v, ← mul_assoc]
+        exact mul_mem_right _ _ hi
+      exact mem_span_singleton'.2 ⟨z, by rw [mul_assoc, mul_comm y]⟩
+    · rw [← span_singleton_mul_span_singleton, ← hx, Ideal.sup_mul, sup_le_iff,
+        span_singleton_mul_span_singleton, mul_comm a, span_singleton_le_iff_mem]
+      exact ⟨mul_le_right, mem_colon_singleton.1 <| hy ▸ mem_span_singleton_self y⟩
 
-variable {R : Type*} [CommRing R]
+end Ideal
+
+open Ideal
 
 /-- If all prime ideals in a commutative ring are principal, so are all other ideals. -/
 theorem IsPrincipalIdealRing.of_prime (H : ∀ P : Ideal R, P.IsPrime → P.IsPrincipal) :
     IsPrincipalIdealRing R := by
-  -- Suppose the set of `nonPrincipals` is not empty.
-  rw [← nonPrincipals_eq_empty_iff, Set.eq_empty_iff_forall_notMem]
-  intro J hJ
-  -- We will show a maximal element `I ∈ nonPrincipals R` (which exists by Zorn) is prime.
-  obtain ⟨I, hJI, hI⟩ := zorn_le_nonempty₀ (nonPrincipals R) nonPrincipals_zorn _ hJ
-  have Imax' : ∀ {J}, I < J → J.IsPrincipal := by
-    intro K hK
-    simpa [nonPrincipals] using hI.not_prop_of_gt hK
-  by_cases hI1 : I = ⊤
-  · subst hI1
-    exact hI.prop top_isPrincipal
-  -- Let `x y : R` with `x * y ∈ I` and suppose WLOG `y ∉ I`.
-  refine hI.prop (H I ⟨hI1, fun {x y} hxy => or_iff_not_imp_right.mpr fun hy => ?_⟩)
-  obtain ⟨a, ha⟩ : (I ⊔ span {y}).IsPrincipal :=
-    Imax' (left_lt_sup.mpr (mt I.span_singleton_le_iff_mem.mp hy))
-  -- Then `x ∈ I.colon (span {y})`, which is equal to `I` if it's not principal.
-  suffices He : ¬(I.colon (span {y})).IsPrincipal by
-    rw [hI.eq_of_le ((nonPrincipals_def R).2 He) fun a ha ↦
-      Ideal.mem_colon_singleton.2 (mul_mem_right _ _ ha)]
-    exact Ideal.mem_colon_singleton.2 hxy
-  -- So suppose for the sake of contradiction that both `I ⊔ span {y}` and `I.colon (span {y})`
-  -- are principal.
-  rintro ⟨b, hb⟩
-  -- We will show `I` is generated by `a * b`.
-  refine (nonPrincipals_def _).1 hI.prop ⟨a * b, ?_⟩
-  refine
-    le_antisymm (α := Ideal R) (fun i hi => ?_) <|
-      (span_singleton_mul_span_singleton a b).ge.trans ?_
-  · have hisup : i ∈ I ⊔ span {y} := Ideal.mem_sup_left hi
-    have : y ∈ I ⊔ span {y} := Ideal.mem_sup_right (Ideal.mem_span_singleton_self y)
-    rw [ha, Ideal.submodule_span_eq, mem_span_singleton'] at hisup this
-    obtain ⟨v, rfl⟩ := this
-    obtain ⟨u, rfl⟩ := hisup
-    have hucolon : u ∈ I.colon (span {v * a}) := by
-      rw [Ideal.mem_colon_singleton, mul_comm v, ← mul_assoc]
-      exact mul_mem_right _ _ hi
-    rw [hb, Ideal.submodule_span_eq, mem_span_singleton'] at hucolon
-    obtain ⟨z, rfl⟩ := hucolon
-    exact mem_span_singleton'.2 ⟨z, by ring⟩
-  · rw [← Ideal.submodule_span_eq, ← ha, Ideal.sup_mul, sup_le_iff,
-      span_singleton_mul_span_singleton, mul_comm y, Ideal.span_singleton_le_iff_mem]
-    exact ⟨mul_le_right, Ideal.mem_colon_singleton.1 <| hb.symm ▸ Ideal.mem_span_singleton_self b⟩
+  refine ⟨isOka_isPrincipal.forall_of_forall_prime (fun I hI ↦ exists_maximal_not_isPrincipal ?_) H⟩
+  rw [isPrincipalIdealRing_iff, not_forall]
+  exact ⟨I, hI⟩