chore: deprecate duplicate Set.dual_ordConnected_iff (#31000)

Author: Ruben-VandeVelde

Mathlib/Order/Interval/Set/OrdConnected.lean

@@ -127,9 +127,16 @@ theorem OrdConnected.dual {s : Set α} (hs : OrdConnected s) :
     OrdConnected (OrderDual.ofDual ⁻¹' s) :=
   ⟨fun _ hx _ hy _ hz => hs.out hy hx ⟨hz.2, hz.1⟩⟩
 
+@[instance]
+theorem dual_ordConnected {s : Set α} [OrdConnected s] : OrdConnected (ofDual ⁻¹' s) :=
+  .dual ‹OrdConnected s›
+
+@[simp]
 theorem ordConnected_dual {s : Set α} : OrdConnected (OrderDual.ofDual ⁻¹' s) ↔ OrdConnected s :=
   ⟨fun h => by simpa only [ordConnected_def] using h.dual, fun h => h.dual⟩
 
+@[deprecated (since := "2025-10-28")] alias dual_ordConnected_iff := ordConnected_dual
+
 theorem ordConnected_sInter {S : Set (Set α)} (hS : ∀ s ∈ S, OrdConnected s) :
     OrdConnected (⋂₀ S) :=
   ⟨fun _x hx _y hy _z hz s hs => (hS s hs).out (hx s hs) (hy s hs) hz⟩
@@ -224,15 +231,6 @@ theorem ordConnected_range {E : Type*} [EquivLike E α β] [OrderIsoClass E α 
   simp_rw [← image_univ]
   exact ordConnected_image (e : α ≃o β)
 
-@[simp]
-theorem dual_ordConnected_iff {s : Set α} : OrdConnected (ofDual ⁻¹' s) ↔ OrdConnected s := by
-  simp_rw [ordConnected_def, toDual.surjective.forall, Icc_toDual, Subtype.forall']
-  exact forall_swap
-
-@[instance]
-theorem dual_ordConnected {s : Set α} [OrdConnected s] : OrdConnected (ofDual ⁻¹' s) :=
-  dual_ordConnected_iff.2 ‹_›
-
 /-- The preimage of an `OrdConnected` set under a map which is monotone on a set `t`,
 when intersected with `t`, is `OrdConnected`. More precisely, it is the intersection with `t`
 of an `OrdConnected` set. -/