refactor: deduplicate PartialOrder (Order.Ideal P) instances (leanprover-community#37467)

These cause a problem in leanprover-community#34820.

The latter instance `Order.Ideal.instPartialOrderIdeal` is unnecessary, because `PartialOrder.ofSetLike` is required to use `IsConcreteLE`-related results.

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Author: Komyyy

Mathlib/Order/Ideal.lean

@@ -107,8 +107,11 @@ instance : SetLike (Ideal P) P where
   coe s := s.carrier
   coe_injective' _ _ h := toLowerSet_injective <| SetLike.coe_injective h
 
+/-- The partial ordering by subset inclusion, inherited from `Set P`. -/
 instance : PartialOrder (Ideal P) := .ofSetLike (Ideal P) P
 
+@[deprecated (since := "2026-04-01")] alias instPartialOrderIdeal := Order.Ideal.instPartialOrder
+
 @[ext]
 theorem ext {s t : Ideal P} : (s : Set P) = t → s = t :=
   SetLike.ext'
@@ -136,10 +139,6 @@ protected theorem isIdeal (s : Ideal P) : IsIdeal (s : Set P) :=
 theorem mem_compl_of_ge {x y : P} : x ≤ y → x ∈ (I : Set P)ᶜ → y ∈ (I : Set P)ᶜ := fun h ↦
   mt <| I.lower h
 
-/-- The partial ordering by subset inclusion, inherited from `Set P`. -/
-instance instPartialOrderIdeal : PartialOrder (Ideal P) :=
-  PartialOrder.lift SetLike.coe SetLike.coe_injective
-
 theorem coe_subset_coe : (s : Set P) ⊆ t ↔ s ≤ t :=
   Iff.rfl
 
@@ -358,21 +357,20 @@ instance : Max (Ideal P) :=
           le_sup_left, le_sup_right⟩
       lower' := fun _ _ h ⟨yi, hi, yj, hj, hxy⟩ ↦ ⟨yi, hi, yj, hj, h.trans hxy⟩ }⟩
 
-instance : Lattice (Ideal P) :=
-  { Ideal.instPartialOrderIdeal with
-    sup := (· ⊔ ·)
-    le_sup_left := fun _ J i hi ↦
-      let ⟨w, hw⟩ := J.nonempty
-      ⟨i, hi, w, hw, le_sup_left⟩
-    le_sup_right := fun I _ j hj ↦
-      let ⟨w, hw⟩ := I.nonempty
-      ⟨w, hw, j, hj, le_sup_right⟩
-    sup_le := fun _ _ K hIK hJK _ ⟨_, hi, _, hj, ha⟩ ↦
-      K.lower ha <| sup_mem (mem_of_mem_of_le hi hIK) (mem_of_mem_of_le hj hJK)
-    inf := (· ⊓ ·)
-    inf_le_left := fun _ _ ↦ inter_subset_left
-    inf_le_right := fun _ _ ↦ inter_subset_right
-    le_inf := fun _ _ _ ↦ subset_inter }
+instance : Lattice (Ideal P) where
+  sup := (· ⊔ ·)
+  le_sup_left := fun _ J i hi ↦
+    let ⟨w, hw⟩ := J.nonempty
+    ⟨i, hi, w, hw, le_sup_left⟩
+  le_sup_right := fun I _ j hj ↦
+    let ⟨w, hw⟩ := I.nonempty
+    ⟨w, hw, j, hj, le_sup_right⟩
+  sup_le := fun _ _ K hIK hJK _ ⟨_, hi, _, hj, ha⟩ ↦
+    K.lower ha <| sup_mem (mem_of_mem_of_le hi hIK) (mem_of_mem_of_le hj hJK)
+  inf := (· ⊓ ·)
+  inf_le_left := fun _ _ ↦ inter_subset_left
+  inf_le_right := fun _ _ ↦ inter_subset_right
+  le_inf := fun _ _ _ ↦ subset_inter
 
 @[simp]
 theorem coe_sup : ↑(s ⊔ t) = { x | ∃ a ∈ s, ∃ b ∈ t, x ≤ a ⊔ b } :=