fix(RingTheory/Ideal): quick fix Oka.lean (#28525)

I just noticed a naming discrepancy between the doc and the actual name of results in `Oka.lean` that I missed in #27200.

The deprecation may not *really* be necessary since the theorem was added yesterday but better be safe.

This PR is also the occasion to clean a little bit the proof of `IsOka.isPrime_of_maximal_not_isOka`.

Author: yapudpill

Mathlib/RingTheory/Ideal/Oka.lean

@@ -8,14 +8,14 @@ import Mathlib.RingTheory.Ideal.Colon
 /-!
 # Oka predicates
 
-This file introduces the notion of oka predicates and standard results about them.
+This file introduces the notion of Oka predicates and standard results about them.
 
 ## Main results
 
-- `Ideal.isPrime_of_maximal_not_isOka`: if an ideal is maximal for not satisfying an oka predicate
+- `Ideal.IsOka.isPrime_of_maximal_not`: if an ideal is maximal for not satisfying an Oka predicate,
   then it is prime.
-- `IsOka.forall_of_forall_prime`: if all prime ideals of a ring satisfy an oka predicate, then all
-  its ideals also satisfy the predicate.
+- `Ideal.IsOka.forall_of_forall_prime`: if all prime ideals of a ring satisfy an Oka predicate,
+  then all its ideals also satisfy the predicate.
 
 ## References
 
@@ -39,25 +39,26 @@ namespace IsOka
 
 variable {P : Ideal R → Prop}
 
-/-- If an ideal is maximal for not satisfying an oka predicate then it is prime. -/
+/-- If an ideal is maximal for not satisfying an Oka predicate then it is prime. -/
 @[stacks 05KE]
-theorem isPrime_of_maximal_not_isOka (hP : IsOka P) {I : Ideal R}
-    (hI : Maximal (¬P ·) I) : I.IsPrime := by
-  by_contra h
-  have I_ne_top : I ≠ ⊤ := fun hI' ↦ hI.prop (hI' ▸ hP.top)
-  obtain ⟨a, ha, b, hb, hab⟩ := (not_isPrime_iff.1 h).resolve_left I_ne_top
-  have h₁ : P (I ⊔ span {a}) := of_not_not <| hI.not_prop_of_gt (Submodule.lt_sup_iff_notMem.2 ha)
-  have h₂ : P (I.colon (span {a})) := of_not_not <| hI.not_prop_of_gt <| lt_of_le_of_ne le_colon
-    (fun H ↦ hb <| H ▸ mem_colon_singleton.2 (mul_comm a b ▸ hab))
-  exact hI.prop (hP.oka h₁ h₂)
+theorem isPrime_of_maximal_not (hP : IsOka P) {I : Ideal R}
+    (hI : Maximal (¬P ·) I) : I.IsPrime where
+  ne_top' hI' := hI.prop (hI' ▸ hP.top)
+  mem_or_mem' := by
+    by_contra!
+    obtain ⟨a, b, hab, ha, hb⟩ := this
+    have h₁ : P (I ⊔ span {a}) := of_not_not <| hI.not_prop_of_gt (Submodule.lt_sup_iff_notMem.2 ha)
+    have h₂ : P (I.colon (span {a})) := of_not_not <| hI.not_prop_of_gt <| lt_of_le_of_ne le_colon
+      (fun H ↦ hb <| H ▸ mem_colon_singleton.2 (mul_comm a b ▸ hab))
+    exact hI.prop (hP.oka h₁ h₂)
 
-/-- If all prime ideals of a ring satisfy an oka predicate, then all its ideals also satisfy the
+/-- If all prime ideals of a ring satisfy an Oka predicate, then all its ideals also satisfy the
 predicate. `hmax` is generaly obtained using Zorn's lemma. -/
-theorem forall_of_forall_prime_isOka (hP : IsOka P)
+theorem forall_of_forall_prime (hP : IsOka P)
     (hmax : (∃ I, ¬P I) → ∃ I, Maximal (¬P ·) I) (hprime : ∀ I, I.IsPrime → P I) : ∀ I, P I := by
   by_contra!
   obtain ⟨I, hI⟩ := hmax this
-  exact hI.prop <| hprime I (hP.isPrime_of_maximal_not_isOka hI)
+  exact hI.prop <| hprime I (hP.isPrime_of_maximal_not hI)
 
 end IsOka