Trigger CI for leanprover-community/batteries#1690

Author: mathlib-nightly-testing[bot]

Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Relations.lean

@@ -95,7 +95,9 @@ private lemma lie_e_f_same_aux (k : ι) (hki : k ≠ i) (hki' : k ≠ P.reflecti
     ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k) := by
   classical
   have h_lin_ind : LinearIndependent R ![P.root i, P.root k] := by
-    rw [LinearIndependent.pair_symm_iff, IsReduced.linearIndependent_iff]; aesop
+    rw [LinearIndependent.pair_symm_iff, IsReduced.linearIndependent_iff]
+    refine ⟨hki, ?_⟩
+    rwa [ne_eq, root_eq_neg_iff]
   suffices (∑ x, if P.root k = P.root i + P.root x then
               (P.chainBotCoeff i x + 1 : R) * (P.chainTopCoeff i k + 1) else 0) -
             (∑ x, if P.root k = P.root x - P.root i then
@@ -220,14 +222,15 @@ include hij
 /-- An auxiliary lemma en route to `RootPairing.Base.lie_e_f_ne`. -/
 private lemma lie_e_f_ne_aux₁ :
     ⁅e i, f j⁆ᵀ (Sum.inr j) = 0 := by
+  have hij' : (i : ι) ≠ (j : ι) := hij ∘ SetLike.coe_eq_coe.mp
   letI := P.indexNeg
   classical
   ext (k | k)
   · rw [Matrix.transpose_apply, lie_e_f_ne_aux₀, Pi.zero_apply]
   · suffices ((if k = i then ↑|b.cartanMatrix i j| else (0 : R)) -
         ∑ x, if P.root x = P.root i + P.root j ∧ P.root k = P.root x - P.root j then
           (P.chainTopCoeff j x : R) + 1 else 0) = 0 by
-      have hij : (j : ι) ≠ -i := by simpa using b.root_ne_neg_of_ne j.property i.property (by aesop)
+      have hij : (j : ι) ≠ -i := by simpa using b.root_ne_neg_of_ne j.property i.property hij'.symm
       have aux : ∀ x ∈ Finset.univ,
         x ≠ j → (if x = j ∧ k = i then ↑|b.cartanMatrix i x| else 0) = (0 : R) := by aesop
       simpa [e, f, P.ne_zero, hij, -indexNeg_neg, -Finset.univ_eq_attach, ← ite_and,
@@ -265,10 +268,12 @@ set_option backward.isDefEq.respectTransparency false in
 /-- Lemma 3.5 from [Geck](Geck2017). -/
 lemma lie_e_f_ne [P.IsReduced] [P.IsIrreducible] :
     ⁅e i, f j⁆ = 0 := by
+  have hij' : (i : ι) ≠ (j : ι) := hij ∘ SetLike.coe_eq_coe.mp
   letI := P.indexNeg
   classical
   ext (k | k) (l | l)
-  · aesop (erase simp indexNeg_neg) (add simp [e, f, Matrix.mul_apply, mul_ite, ite_mul])
+  · rw [ne_comm] at hij
+    simp_all [-indexNeg_neg, e, f]
   · exact lie_e_f_ne_aux₀ k l
   · have aux₁ : P.root k ≠ P.root i - P.root j :=
       fun contra ↦ b.sub_notMem_range_root i.property j.property ⟨k, contra⟩
@@ -303,8 +308,8 @@ lemma lie_e_f_ne [P.IsReduced] [P.IsIrreducible] :
       simp [Finset.sum_ite_of_false aux₃, Finset.sum_ite_of_false aux₄]
     by_cases h₆ : P.root l + P.root i ∈ range P.root; swap
     · have h₇ : P.root l - P.root j ∉ range P.root := by
-        rwa [b.root_sub_mem_iff_root_add_mem i j l (by aesop) i.property j.property
-          (by aesop) (by aesop) h₅]
+        rwa [b.root_sub_mem_iff_root_add_mem i j l hij' i.property j.property h₃ _ h₅]
+        simpa
       have aux₃ : ∀ x ∈ Finset.univ,
           ¬ (P.root x = P.root i + P.root l ∧ P.root k = P.root x - P.root j) := by
         rintro x - ⟨hx, -⟩; exact h₆ ⟨x, by rw [hx]; abel⟩
@@ -313,7 +318,7 @@ lemma lie_e_f_ne [P.IsReduced] [P.IsIrreducible] :
         rintro x - ⟨hx, hx'⟩; exact h₇ ⟨x, hx⟩
       simp [Finset.sum_ite_of_false aux₃, Finset.sum_ite_of_false aux₄]
     obtain ⟨m, hm : P.root m = P.root l - P.root j⟩ :=
-      b.root_sub_root_mem_of_mem_of_mem i j l (by aesop) i.property j.property h₅ h₃ h₆
+      b.root_sub_root_mem_of_mem_of_mem i j l hij' i.property j.property h₅ h₃ h₆
     obtain ⟨l', hl'⟩ := h₆
     by_cases hk : P.root k = P.root l + P.root i - P.root j; swap
     · grind
@@ -326,7 +331,7 @@ lemma lie_e_f_ne [P.IsReduced] [P.IsIrreducible] :
     rw [Finset.sum_eq_single_of_mem m (Finset.mem_univ _) (by rintro x - h; rw [if_neg (aux₃ _ h)]),
       Finset.sum_eq_single_of_mem l' (Finset.mem_univ _) (by rintro x - h; rw [if_neg (aux₄ _ h)]),
       if_pos (⟨hm, by rw [hm, hk]; abel⟩), if_pos ⟨by rw [hl', add_comm], by rw [hl', hk]⟩]
-    have := chainBotCoeff_mul_chainTopCoeff i.property j.property (by aesop) hl'.symm hm.symm h₅
+    have := chainBotCoeff_mul_chainTopCoeff i.property j.property hij' hl'.symm hm.symm h₅
     norm_cast
 
 end lie_e_f_ne

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