chore(Order/SuccPred/Archimedean): use to_dual (leanprover-community#34882)

Co-authored-by: vihdzp <vi.hdz.p@mgmail.com>

Author: vihdzp

Mathlib/Order/MinMax.lean

@@ -197,18 +197,14 @@ theorem AntitoneOn.map_max (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) :
 theorem AntitoneOn.map_min (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (min a b) =
     max (f a) (f b) := hf.dual.map_max ha hb
 
+@[to_dual]
 theorem Monotone.map_max (hf : Monotone f) : f (max a b) = max (f a) (f b) := by
   rcases le_total a b with h | h <;> simp [h, hf h]
 
-theorem Monotone.map_min (hf : Monotone f) : f (min a b) = min (f a) (f b) :=
-  hf.dual.map_max
-
+@[to_dual]
 theorem Antitone.map_max (hf : Antitone f) : f (max a b) = min (f a) (f b) := by
   rcases le_total a b with h | h <;> simp [h, hf h]
 
-theorem Antitone.map_min (hf : Antitone f) : f (min a b) = max (f a) (f b) :=
-  hf.dual.map_max
-
 theorem min_choice (a b : α) : min a b = a ∨ min a b = b := by cases le_total a b <;> simp [*]
 
 theorem max_choice (a b : α) : max a b = a ∨ max a b = b :=

Mathlib/Order/SuccPred/Archimedean.lean

@@ -30,35 +30,46 @@ class IsSuccArchimedean (α : Type*) [Preorder α] [SuccOrder α] : Prop where
 
 /-- A `PredOrder` is pred-archimedean if one can go from any two comparable elements by iterating
 `pred` -/
+@[to_dual existing]
 class IsPredArchimedean (α : Type*) [Preorder α] [PredOrder α] : Prop where
   /-- If `a ≤ b` then one can get to `b` from `a` by iterating `pred` -/
   exists_pred_iterate_of_le {a b : α} (h : a ≤ b) : ∃ n, pred^[n] b = a
 
 export IsSuccArchimedean (exists_succ_iterate_of_le)
-
 export IsPredArchimedean (exists_pred_iterate_of_le)
 
+attribute [to_dual existing] exists_succ_iterate_of_le
+
 section Preorder
 
 variable [Preorder α]
 
+-- `to_dual` cannot yet reorder arguments of arguments
+instance [SuccOrder α] [IsSuccArchimedean α] : IsPredArchimedean αᵒᵈ :=
+  ⟨fun {a b} h => by convert exists_succ_iterate_of_le h.ofDual⟩
+
+@[to_dual existing]
+instance [PredOrder α] [IsPredArchimedean α] : IsSuccArchimedean αᵒᵈ :=
+  ⟨fun {a b} h => by convert exists_pred_iterate_of_le h.ofDual⟩
+
 section SuccOrder
 
 variable [SuccOrder α] [IsSuccArchimedean α] {a b : α}
 
-instance : IsPredArchimedean αᵒᵈ :=
-  ⟨fun {a b} h => by convert exists_succ_iterate_of_le h.ofDual⟩
-
+@[to_dual]
 theorem LE.le.exists_succ_iterate (h : a ≤ b) : ∃ n, succ^[n] a = b :=
   exists_succ_iterate_of_le h
 
+@[to_dual]
 theorem exists_succ_iterate_iff_le : (∃ n, succ^[n] a = b) ↔ a ≤ b := by
   refine ⟨?_, exists_succ_iterate_of_le⟩
   rintro ⟨n, rfl⟩
   exact id_le_iterate_of_id_le le_succ n a
 
+-- TODO: rename to `Order.succ_rec`?
 /-- Induction principle on a type with a `SuccOrder` for all elements above a given element `m`. -/
-@[elab_as_elim]
+@[to_dual (attr := elab_as_elim) Pred.rec
+/-- Induction principle on a type with a `PredOrder` for all elements below a given element `m`. -/]
 theorem Succ.rec {m : α} {P : ∀ n, m ≤ n → Prop} (rfl : P m le_rfl)
     (succ : ∀ n (hmn : m ≤ n), P n hmn → P (succ n) (hmn.trans <| le_succ _)) ⦃n : α⦄
     (hmn : m ≤ n) : P n hmn := by
@@ -69,11 +80,13 @@ theorem Succ.rec {m : α} {P : ∀ n, m ≤ n → Prop} (rfl : P m le_rfl)
     simp_rw [Function.iterate_succ_apply']
     exact succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)
 
+@[to_dual Pred.rec_iff]
 theorem Succ.rec_iff {p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) {a b : α} (h : a ≤ b) :
     p a ↔ p b := by
   obtain ⟨n, rfl⟩ := h.exists_succ_iterate
   exact Iterate.rec (fun b => p a ↔ p b) Iff.rfl (fun c hc => hc.trans (hsucc _)) n
 
+@[to_dual le_total_of_directed]
 lemma le_total_of_codirected {r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r ≤ v₂) : v₁ ≤ v₂ ∨ v₂ ≤ v₁ := by
   obtain ⟨n, rfl⟩ := h₁.exists_succ_iterate
   obtain ⟨m, rfl⟩ := h₂.exists_succ_iterate
@@ -89,41 +102,13 @@ lemma le_total_of_codirected {r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r 
 
 end SuccOrder
 
-section PredOrder
-
-variable [PredOrder α] [IsPredArchimedean α] {a b : α}
-
-instance : IsSuccArchimedean αᵒᵈ :=
-  ⟨fun {a b} h => by convert exists_pred_iterate_of_le h.ofDual⟩
-
-theorem LE.le.exists_pred_iterate (h : a ≤ b) : ∃ n, pred^[n] b = a :=
-  exists_pred_iterate_of_le h
-
-theorem exists_pred_iterate_iff_le : (∃ n, pred^[n] b = a) ↔ a ≤ b :=
-  exists_succ_iterate_iff_le (α := αᵒᵈ)
-
-/-- Induction principle on a type with a `PredOrder` for all elements below a given element `m`. -/
-@[elab_as_elim]
-theorem Pred.rec {m : α} {P : ∀ n, n ≤ m → Prop} (rfl : P m le_rfl)
-    (pred : ∀ n (hnm : n ≤ m), P n hnm → P (pred n) ((pred_le _).trans hnm)) ⦃n : α⦄
-    (hnm : n ≤ m) : P n hnm :=
-  Succ.rec (α := αᵒᵈ) (P := P) rfl pred hnm
-
-theorem Pred.rec_iff {p : α → Prop} (hsucc : ∀ a, p a ↔ p (pred a)) {a b : α} (h : a ≤ b) :
-    p a ↔ p b :=
-  (Succ.rec_iff (α := αᵒᵈ) hsucc h).symm
-
-lemma le_total_of_directed {r v₁ v₂ : α} (h₁ : v₁ ≤ r) (h₂ : v₂ ≤ r) : v₁ ≤ v₂ ∨ v₂ ≤ v₁ :=
-  Or.symm (le_total_of_codirected (α := αᵒᵈ) h₁ h₂)
-
-end PredOrder
-
 end Preorder
 
 section PartialOrder
 
 variable [PartialOrder α]
 
+@[to_dual (reorder := h₁ h₂) lt_or_le_of_directed]
 lemma lt_or_le_of_codirected [SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂ : α} (h₁ : r ≤ v₁)
     (h₂ : r ≤ v₂) : v₁ < v₂ ∨ v₂ ≤ v₁ := by
   rw [Classical.or_iff_not_imp_right]
@@ -132,6 +117,7 @@ lemma lt_or_le_of_codirected [SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂
   · apply lt_of_le_of_ne h (ne_of_not_le nh).symm
   · contradiction
 
+-- `to_dual` cannot yet reorder arguments of arguments
 /--
 This isn't an instance due to a loop with `LinearOrder`.
 -/
@@ -146,18 +132,11 @@ abbrev IsSuccArchimedean.linearOrder [SuccOrder α] [IsSuccArchimedean α]
   toDecidableLE := inferInstance
   toDecidableLT := inferInstance
 
-lemma lt_or_le_of_directed [PredOrder α] [IsPredArchimedean α] {r v₁ v₂ : α} (h₁ : v₁ ≤ r)
-    (h₂ : v₂ ≤ r) : v₁ < v₂ ∨ v₂ ≤ v₁ := by
-  rw [Classical.or_iff_not_imp_right]
-  intro nh
-  rcases le_total_of_directed h₁ h₂ with h | h
-  · apply lt_of_le_of_ne h (ne_of_not_le nh).symm
-  · contradiction
-
 /--
 This isn't an instance due to a loop with `LinearOrder`.
 -/
 -- See note [reducible non-instances]
+@[to_dual existing]
 abbrev IsPredArchimedean.linearOrder [PredOrder α] [IsPredArchimedean α]
      [DecidableEq α] [DecidableLE α] [DecidableLT α]
      [IsDirectedOrder α] : LinearOrder α :=
@@ -173,40 +152,30 @@ variable [LinearOrder α]
 section SuccOrder
 variable [SuccOrder α]
 
-lemma succ_max (a b : α) : succ (max a b) = max (succ a) (succ b) := succ_mono.map_max
-lemma succ_min (a b : α) : succ (min a b) = min (succ a) (succ b) := succ_mono.map_min
+@[deprecated (since := "2026-02-05")] alias succ_max := Order.succ_max
+@[deprecated (since := "2026-02-05")] alias succ_min := Order.succ_min
+
+@[deprecated (since := "2026-02-05")] alias pred_max := Order.pred_max
+@[deprecated (since := "2026-02-05")] alias pred_min := Order.pred_min
 
 variable [IsSuccArchimedean α] {a b : α}
 
+@[to_dual]
 theorem exists_succ_iterate_or : (∃ n, succ^[n] a = b) ∨ ∃ n, succ^[n] b = a :=
   (le_total a b).imp exists_succ_iterate_of_le exists_succ_iterate_of_le
 
+@[to_dual Pred.rec_linear]
 theorem Succ.rec_linear {p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) (a b : α) : p a ↔ p b :=
   (le_total a b).elim (Succ.rec_iff hsucc) fun h => (Succ.rec_iff hsucc h).symm
 
 end SuccOrder
 
-section PredOrder
-variable [PredOrder α]
-
-lemma pred_max (a b : α) : pred (max a b) = max (pred a) (pred b) := pred_mono.map_max
-lemma pred_min (a b : α) : pred (min a b) = min (pred a) (pred b) := pred_mono.map_min
-
-variable [IsPredArchimedean α] {a b : α}
-
-theorem exists_pred_iterate_or : (∃ n, pred^[n] b = a) ∨ ∃ n, pred^[n] a = b :=
-  (le_total a b).imp exists_pred_iterate_of_le exists_pred_iterate_of_le
-
-theorem Pred.rec_linear {p : α → Prop} (hsucc : ∀ a, p a ↔ p (pred a)) (a b : α) : p a ↔ p b :=
-  (le_total a b).elim (Pred.rec_iff hsucc) fun h => (Pred.rec_iff hsucc h).symm
-
-end PredOrder
-
 end LinearOrder
 
 section bdd_range
 variable [Preorder α] [Nonempty α] [Preorder β] {f : α → β}
 
+@[to_dual]
 lemma StrictMono.not_bddAbove_range_of_isSuccArchimedean [NoMaxOrder α] [SuccOrder β]
     [IsSuccArchimedean β] (hf : StrictMono f) : ¬ BddAbove (Set.range f) := by
   rintro ⟨m, hm⟩
@@ -221,24 +190,22 @@ lemma StrictMono.not_bddAbove_range_of_isSuccArchimedean [NoMaxOrder α] [SuccOr
   rintro b _ ⟨a, hba⟩
   exact (h a).imp (fun a' ↦ (succ_le_of_lt hba).trans_lt)
 
-lemma StrictMono.not_bddBelow_range_of_isPredArchimedean [NoMinOrder α] [PredOrder β]
-    [IsPredArchimedean β] (hf : StrictMono f) : ¬ BddBelow (Set.range f) :=
-  hf.dual.not_bddAbove_range_of_isSuccArchimedean
-
-lemma StrictAnti.not_bddBelow_range_of_isSuccArchimedean [NoMinOrder α] [SuccOrder β]
+@[to_dual]
+lemma StrictAnti.not_bddAbove_range_of_isSuccArchimedean [NoMinOrder α] [SuccOrder β]
     [IsSuccArchimedean β] (hf : StrictAnti f) : ¬ BddAbove (Set.range f) :=
   hf.dual_right.not_bddBelow_range_of_isPredArchimedean
 
-lemma StrictAnti.not_bddBelow_range_of_isPredArchimedean [NoMaxOrder α] [PredOrder β]
-    [IsPredArchimedean β] (hf : StrictAnti f) : ¬ BddBelow (Set.range f) :=
-  hf.dual_right.not_bddAbove_range_of_isSuccArchimedean
+@[deprecated (since := "2026-02-05")]
+alias StrictMono.not_bddBelow_range_of_isSuccArchimedean :=
+  StrictMono.not_bddAbove_range_of_isSuccArchimedean
 
 end bdd_range
 
 section IsWellFounded
 
 variable [PartialOrder α]
 
+-- `to_dual` cannot yet reorder arguments of arguments
 instance (priority := 100) WellFoundedLT.toIsPredArchimedean [h : WellFoundedLT α]
     [PredOrder α] : IsPredArchimedean α :=
   ⟨fun {a b} => by
@@ -255,6 +222,7 @@ instance (priority := 100) WellFoundedLT.toIsPredArchimedean [h : WellFoundedLT
     refine ⟨k + 1, ?_⟩
     rw [iterate_add_apply, iterate_one, hk]⟩
 
+@[to_dual existing]
 instance (priority := 100) WellFoundedGT.toIsSuccArchimedean [h : WellFoundedGT α]
     [SuccOrder α] : IsSuccArchimedean α :=
   let h : IsPredArchimedean αᵒᵈ := by infer_instance
@@ -266,20 +234,13 @@ section OrderBot
 
 variable [Preorder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α]
 
+@[to_dual Pred.rec_top]
 theorem Succ.rec_bot (p : α → Prop) (hbot : p ⊥) (hsucc : ∀ a, p a → p (succ a)) (a : α) : p a :=
   Succ.rec hbot (fun x _ h => hsucc x h) (bot_le : ⊥ ≤ a)
 
 end OrderBot
 
-section OrderTop
-
-variable [Preorder α] [OrderTop α] [PredOrder α] [IsPredArchimedean α]
-
-theorem Pred.rec_top (p : α → Prop) (htop : p ⊤) (hpred : ∀ a, p a → p (pred a)) (a : α) : p a :=
-  Pred.rec htop (fun x _ h => hpred x h) (le_top : a ≤ ⊤)
-
-end OrderTop
-
+@[to_dual]
 lemma SuccOrder.forall_ne_bot_iff
     [Nontrivial α] [PartialOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α]
     (P : α → Prop) :
@@ -293,7 +254,8 @@ lemma SuccOrder.forall_ne_bot_iff
 
 section IsLeast
 
--- TODO: generalize to PartialOrder and `DirectedOn` after https://github.com/leanprover-community/mathlib4/pull/16272
+-- TODO: generalize to PartialOrder and `DirectedOn`
+@[to_dual]
 lemma BddAbove.exists_isGreatest_of_nonempty {X : Type*} [LinearOrder X] [SuccOrder X]
     [IsSuccArchimedean X] {S : Set X} (hS : BddAbove S) (hS' : S.Nonempty) :
     ∃ x, IsGreatest S x := by
@@ -317,18 +279,13 @@ lemma BddAbove.exists_isGreatest_of_nonempty {X : Type*} [LinearOrder X] [SuccOr
   · exact ⟨m, hmS, hm⟩
   · exact IH hm hn hmS
 
-lemma BddBelow.exists_isLeast_of_nonempty {X : Type*} [LinearOrder X] [PredOrder X]
-    [IsPredArchimedean X] {S : Set X} (hS : BddBelow S) (hS' : S.Nonempty) :
-    ∃ x, IsLeast S x :=
-  hS.dual.exists_isGreatest_of_nonempty hS'
-
 end IsLeast
 
 section OrderIso
 
 variable {X Y : Type*} [PartialOrder X] [PartialOrder Y]
 
-set_option backward.isDefEq.respectTransparency false in
+-- `to_dual` cannot yet reorder arguments of arguments
 /-- `IsSuccArchimedean` transfers across equivalences between `SuccOrder`s. -/
 protected lemma IsSuccArchimedean.of_orderIso [SuccOrder X] [IsSuccArchimedean X] [SuccOrder Y]
     (f : X ≃o Y) : IsSuccArchimedean Y where
@@ -342,8 +299,8 @@ protected lemma IsSuccArchimedean.of_orderIso [SuccOrder X] [IsSuccArchimedean X
     | zero => simp
     | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- `IsPredArchimedean` transfers across equivalences between `PredOrder`s. -/
+@[to_dual existing]
 protected lemma IsPredArchimedean.of_orderIso [PredOrder X] [IsPredArchimedean X] [PredOrder Y]
     (f : X ≃o Y) : IsPredArchimedean Y where
   exists_pred_iterate_of_le {a b} h := by

Mathlib/Order/SuccPred/Basic.lean

@@ -222,6 +222,7 @@ theorem succ_le_succ (h : a ≤ b) : succ a ≤ succ b := by
   · rw [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h]
     apply lt_succ_of_le_of_not_isMax h hb
 
+@[to_dual]
 theorem succ_mono : Monotone (succ : α → α) := fun _ _ => succ_le_succ
 
 /-- See also `Order.succ_eq_of_covBy`. -/
@@ -421,6 +422,9 @@ section LinearOrder
 
 variable [LinearOrder α] [SuccOrder α] {a b : α}
 
+@[to_dual] lemma succ_max (a b : α) : succ (max a b) = max (succ a) (succ b) := succ_mono.map_max
+@[to_dual] lemma succ_min (a b : α) : succ (min a b) = min (succ a) (succ b) := succ_mono.map_min
+
 @[to_dual le_of_pred_lt]
 theorem le_of_lt_succ {a b : α} : a < succ b → a ≤ b := fun h ↦ by
   by_contra! nh
@@ -620,9 +624,6 @@ theorem pred_covBy_of_not_isMin (h : ¬IsMin a) : pred a ⋖ a :=
 theorem pred_lt_of_not_isMin_of_le (ha : ¬IsMin a) : a ≤ b → pred a < b :=
   (pred_lt_of_not_isMin ha).trans_le
 
-@[to_dual existing]
-theorem pred_mono : Monotone (pred : α → α) := fun _ _ => pred_le_pred
-
 @[deprecated (since := "2025-12-04")]
 alias pred_le_pred_of_not_isMin_of_le := pred_mono