Act on reviews

Author: linesthatinterlace

src/Init/Core.lean

@@ -2543,9 +2543,9 @@ class Irrefl (r : α → α → Prop) : Prop where
   /-- An irreflexive relation satisfies `¬ r a a`. -/
   irrefl : ∀ a, ¬r a a
 
-/-- `Tricho r` says that `r` is trichotomous, that is, `¬ r a b → ¬ r b a → a = b`. -/
-class Tricho (r : α → α → Prop) : Prop where
+/-- `Trichotomous r` says that `r` is trichotomous, that is, `¬ r a b → ¬ r b a → a = b`. -/
+class Trichotomous (r : α → α → Prop) : Prop where
   /-- An trichotomous relation `r` satisfies `¬ r a b → ¬ r b a → a = b`. -/
-  tricho (a b : α) : ¬ r a b → ¬ r b a → a = b
+  trichotomous (a b : α) : ¬ r a b → ¬ r b a → a = b
 
 end Std

src/Init/Data/Array/Lex/Lemmas.lean

@@ -140,7 +140,7 @@ protected theorem lt_of_le_of_lt [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrd
 @[deprecated Array.lt_of_le_of_lt (since := "2025-08-01")]
 protected theorem lt_of_le_of_lt' [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Tricho (· < · : α → α → Prop)]
+    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
     [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
   letI := LE.ofLT α
@@ -154,7 +154,7 @@ protected theorem le_trans [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α]
 @[deprecated Array.le_trans (since := "2025-08-01")]
 protected theorem le_trans' [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Tricho (· < · : α → α → Prop)]
+    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
     [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
   letI := LE.ofLT α
@@ -191,7 +191,7 @@ protected theorem le_of_lt [LT α]
 
 protected theorem le_iff_lt_or_eq [LT α]
     [Std.Irrefl (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)]
+    [Std.Trichotomous (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Array α} : xs ≤ ys ↔ xs < ys ∨ xs = ys := by
   simpa using List.le_iff_lt_or_eq (l₁ := xs.toList) (l₂ := ys.toList)
@@ -280,7 +280,7 @@ protected theorem lt_iff_exists [LT α] {xs ys : Array α} :
 
 protected theorem le_iff_exists [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)] {xs ys : Array α} :
+    [Std.Trichotomous (· < · : α → α → Prop)] {xs ys : Array α} :
     xs ≤ ys ↔
       (xs = ys.take xs.size) ∨
         (∃ (i : Nat) (h₁ : i < xs.size) (h₂ : i < ys.size),
@@ -299,7 +299,7 @@ theorem append_left_lt [LT α] {xs ys zs : Array α} (h : ys < zs) :
 
 theorem append_left_le [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)]
+    [Std.Trichotomous (· < · : α → α → Prop)]
     {xs ys zs : Array α} (h : ys ≤ zs) :
     xs ++ ys ≤ xs ++ zs := by
   cases xs
@@ -322,9 +322,9 @@ protected theorem map_lt [LT α] [LT β]
 
 protected theorem map_le [LT α] [LT β]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)]
+    [Std.Trichotomous (· < · : α → α → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
-    [Std.Tricho (· < · : β → β → Prop)]
+    [Std.Trichotomous (· < · : β → β → Prop)]
     {xs ys : Array α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : xs ≤ ys) :
     map f xs ≤ map f ys := by
   cases xs

src/Init/Data/Char/Lemmas.lean

@@ -51,8 +51,12 @@ instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
   antisymm _ _ := Char.le_antisymm
 
 -- This instance is useful while setting up instances for `String`.
-def ltTricho : Std.Tricho (· < · : Char → Char → Prop) where
-  tricho _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
+instance ltTrichotomous : Std.Trichotomous (· < · : Char → Char → Prop) where
+  trichotomous _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
+
+@[deprecated ltTrichotomous (since := "2025-10-27")]
+def notLtAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where
+  antisymm := Char.ltTrichotomous.trichotomous
 
 instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
   asymm _ _ := Char.lt_asymm

src/Init/Data/List/BasicAux.lean

@@ -272,8 +272,8 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
     apply Nat.lt_trans ih
     simp +arith
 
-theorem lex_tricho [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
-    (tricho : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
+theorem lex_trichotomous [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
+    (trichotomous : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
     {as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
   match as, bs with
   | [],    []    => rfl
@@ -286,20 +286,26 @@ theorem lex_tricho [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
       · subst eq
         have h₁ : ¬ Lex r bs as := fun h => h₁ (List.Lex.cons h)
         have h₂ : ¬ Lex r as bs := fun h => h₂ (List.Lex.cons h)
-        simp [lex_tricho tricho h₁ h₂]
+        simp [lex_trichotomous trichotomous h₁ h₂]
       · exfalso
         by_cases hba : r b a
         · exact h₁ (Lex.rel hba)
-        · exact eq (tricho _ _ hab hba)
+        · exact eq (trichotomous _ _ hab hba)
+
+@[deprecated lex_trichotomous (since := "2025-10-27")]
+theorem lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
+    (antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
+    {as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
+  lex_trichotomous antisymm h₁ h₂
 
 protected theorem le_antisymm [LT α]
-    [i : Std.Tricho (· < · : α → α → Prop)]
+    [i : Std.Trichotomous (· < · : α → α → Prop)]
     {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
   open Classical in
-  lex_tricho i.tricho h₁ h₂
+  lex_trichotomous i.trichotomous h₁ h₂
 
 instance [LT α]
-    [s : Std.Tricho (· < · : α → α → Prop)] :
+    [s : Std.Trichotomous (· < · : α → α → Prop)] :
     Std.Antisymm (· ≤ · : List α → List α → Prop) where
   antisymm _ _ h₁ h₂ := List.le_antisymm h₁ h₂
 

src/Init/Data/List/Lex.lean

@@ -87,7 +87,7 @@ theorem not_cons_lex_cons_iff [DecidableEq α] [DecidableRel r] {a b} {l₁ l₂
 
 theorem cons_le_cons_iff [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Tricho (· < · : α → α → Prop)]
+    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
     {a b} {l₁ l₂ : List α} :
     (a :: l₁) ≤ (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ ≤ l₂ := by
   dsimp only [instLE, instLT, List.le, List.lt]
@@ -99,12 +99,12 @@ theorem cons_le_cons_iff [LT α]
       apply Decidable.byContradiction
       intro h₃
       apply h₂
-      exact i₂.tricho _ _ h₁ h₃
+      exact i₂.trichotomous _ _ h₁ h₃
     · if h₃ : a < b then
         exact .inl h₃
       else
         right
-        exact ⟨i₂.tricho _ _ h₃ h₁, h₂⟩
+        exact ⟨i₂.trichotomous _ _ h₃ h₁, h₂⟩
   · rintro (h | ⟨h₁, h₂⟩)
     · left
       exact ⟨i₁.asymm _ _ h, fun w => Irrefl.irrefl _ (w ▸ h)⟩
@@ -113,7 +113,7 @@ theorem cons_le_cons_iff [LT α]
 
 theorem not_lt_of_cons_le_cons [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Tricho (· < · : α → α → Prop)]
+    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
     {a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : ¬ b < a := by
   rw [cons_le_cons_iff] at h
   rcases h with h | ⟨rfl, h⟩
@@ -127,7 +127,7 @@ theorem left_le_left_of_cons_le_cons [LT α] [LE α] [IsLinearOrder α]
 theorem le_of_cons_le_cons [LT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Tricho (· < · : α → α → Prop)]
+    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
     {a} {l₁ l₂ : List α} (h : a :: l₁ ≤ a :: l₂) : l₁ ≤ l₂ := by
   rw [cons_le_cons_iff] at h
   rcases h with h | ⟨_, h⟩
@@ -201,7 +201,7 @@ protected theorem lt_of_le_of_lt [LT α] [LE α] [IsLinearOrder α] [LawfulOrder
 @[deprecated List.lt_of_le_of_lt (since := "2025-08-01")]
 protected theorem lt_of_le_of_lt' [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)]
+    [Std.Trichotomous (· < · : α → α → Prop)]
     [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
   letI : LE α := .ofLT α
@@ -215,7 +215,7 @@ protected theorem le_trans [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α]
 @[deprecated List.le_trans (since := "2025-08-01")]
 protected theorem le_trans' [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)]
+    [Std.Trichotomous (· < · : α → α → Prop)]
     [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
   letI := LE.ofLT α
@@ -293,7 +293,7 @@ protected theorem le_of_lt [LT α]
 
 protected theorem le_iff_lt_or_eq [LT α]
     [Std.Irrefl (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)]
+    [Std.Trichotomous (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     {l₁ l₂ : List α} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂ := by
   constructor
@@ -479,7 +479,7 @@ protected theorem lt_iff_exists [LT α] {l₁ l₂ : List α} :
 
 protected theorem le_iff_exists [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)] {l₁ l₂ : List α} :
+    [Std.Trichotomous (· < · : α → α → Prop)] {l₁ l₂ : List α} :
     l₁ ≤ l₂ ↔
       (l₁ = l₂.take l₁.length) ∨
         (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
@@ -492,7 +492,7 @@ protected theorem le_iff_exists [LT α]
     conv => lhs; simp +singlePass [exists_comm]
   · simpa using Std.Irrefl.irrefl
   · simpa using Std.Asymm.asymm
-  · simpa using Std.Tricho.tricho
+  · simpa using Std.Trichotomous.trichotomous
 
 theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
     l₁ ++ l₂ < l₁ ++ l₃ := by
@@ -502,7 +502,7 @@ theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
 
 theorem append_left_le [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)]
+    [Std.Trichotomous (· < · : α → α → Prop)]
     {l₁ l₂ l₃ : List α} (h : l₂ ≤ l₃) :
     l₁ ++ l₂ ≤ l₁ ++ l₃ := by
   induction l₁ with
@@ -535,9 +535,9 @@ protected theorem map_lt [LT α] [LT β]
 
 protected theorem map_le [LT α] [LT β]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Tricho (· < · : α → α → Prop)]
+    [Std.Trichotomous (· < · : α → α → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
-    [Std.Tricho (· < · : β → β → Prop)]
+    [Std.Trichotomous (· < · : β → β → Prop)]
     {l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :
     map f l₁ ≤ map f l₂ := by
   rw [List.le_iff_exists] at h ⊢

src/Init/Data/Nat/Basic.lean

@@ -468,8 +468,13 @@ protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤
 instance : Std.Antisymm ( . ≤ . : Nat → Nat → Prop) where
   antisymm _ _ h₁ h₂ := Nat.le_antisymm h₁ h₂
 
-instance : Std.Tricho (. < . : Nat → Nat → Prop) where
-  tricho _ _ h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
+instance : Std.Trichotomous (. < . : Nat → Nat → Prop) where
+  trichotomous _ _ h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
+
+set_option linter.missingDocs false in
+@[deprecated Nat.instTrichotomousLt (since := "2025-10-27")]
+def Nat.instAntisymmNotLt : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
+  antisymm := Nat.instTrichotomousLt.trichotomous
 
 protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=
   match le.dest h with

src/Init/Data/Order/Factories.lean

@@ -234,13 +234,13 @@ If an `LT α` instance is asymmetric and its negation is transitive and antisymm
 public theorem IsLinearOrder.of_lt {α : Type u} [LT α]
     (lt_asymm : Asymm (α := α) (· < ·) := by exact inferInstance)
     (not_lt_trans : Trans (α := α) (¬ · < ·) (¬ · < ·) (¬ · < ·) := by exact inferInstance)
-    (lt_tricho : Tricho (α := α) (· < ·) := by exact inferInstance) :
+    (lt_trichotomous : Trichotomous (α := α) (· < ·) := by exact inferInstance) :
     haveI := LE.ofLT α
     IsLinearOrder α :=
   letI := LE.ofLT α
   haveI : IsLinearPreorder α := .of_lt
   { le_antisymm := by
-      simpa [LE.ofLT] using fun a b hab hba => lt_tricho.tricho a b hba hab }
+      simpa [LE.ofLT] using fun a b hab hba => lt_trichotomous.trichotomous a b hba hab }
 
 /--
 This lemma characterizes in terms of `LT α` when a `Min α` instance

src/Init/Data/Order/Lemmas.lean

@@ -28,35 +28,41 @@ public instance (r : α → α → Prop) [Total r] : Refl r where
 public instance (r : α → α → Prop) [Asymm r] : Antisymm r where
   antisymm a b h h' := (Asymm.asymm a b h h').elim
 
-public instance (r : α → α → Prop) [Total r] : Tricho r where
-  tricho a b h h' := by simpa [h, h'] using Total.total (r := r) a b
+public instance (r : α → α → Prop) [Total r] : Trichotomous r where
+  trichotomous a b h h' := by simpa [h, h'] using Total.total (r := r) a b
 
-public theorem Tricho.rel_or_eq_or_swap {r : α → α → Prop} [Tricho r] {a b} :
-    r a b ∨ a = b ∨ r b a := by
-  cases Classical.em (r a b) with | inl hab | inr hab
-  · exact Or.inl hab
-  · cases Classical.em (r b a) with | inl hba | inr hba
-    · exact Or.inr (Or.inr hba)
-    · exact Or.inr (Or.inl (Tricho.tricho _ _ hab hba))
+public theorem Trichotomous.rel_or_eq_or_rel_swap {r : α → α → Prop} [Trichotomous r] {a b} :
+    r a b ∨ a = b ∨ r b a := match Classical.em (r a b) with
+  | .inl hab => .inl hab | .inr hab => match Classical.em (r b a) with
+    | .inl hba => .inr <| .inr hba
+    | .inr hba => .inr <| .inl <| Trichotomous.trichotomous _ _ hab hba
 
-public theorem tricho_of_rel_or_eq_or_swap {r : α → α → Prop}
-    (h : ∀ {a b}, r a b ∨ a = b ∨ r b a) : Tricho r where
-  tricho _ _ hab hba := (h.resolve_left hab).resolve_right hba
+public theorem trichotomous_of_rel_or_eq_or_rel_swap {r : α → α → Prop}
+    (h : ∀ {a b}, r a b ∨ a = b ∨ r b a) : Trichotomous r where
+  trichotomous _ _ hab hba := (h.resolve_left hab).resolve_right hba
+
+public theorem Antisymm.trichotomous_of_antisymm_not {r : α → α → Prop} [i : Antisymm (¬ r · ·)] :
+    Trichotomous r where trichotomous := i.antisymm
+
+public theorem Trichotomous.antisymm_not {r : α → α → Prop} [i : Trichotomous r] :
+    Antisymm (¬ r · ·) where antisymm := i.trichotomous
 
 public theorem Total.of_not_swap {r : α → α → Prop} [Total r] {a b} (h : ¬ r a b) : r b a :=
   (Total.total a b).elim (fun h' => (h h').elim) (·)
 
-public def total_of_of_not_swap {r : α → α → Prop} (h : ∀ {a b}, ¬ r a b → r b a) : Total r where
+public theorem total_of_not_rel_swap_imp_rel {r : α → α → Prop} (h : ∀ {a b}, ¬ r a b → r b a) :
+    Total r where
   total a b := Classical.byCases (p := r a b) Or.inl (fun hab => Or.inr (h hab))
 
-public def total_of_refl_of_tricho (r : α → α → Prop) [Refl r] [Tricho r] : Total r where
-  total a b := (Tricho.rel_or_eq_or_swap (a := a) (b := b) (r := r)).elim Or.inl <|
+public theorem total_of_refl_of_trichotomous (r : α → α → Prop) [Refl r] [Trichotomous r] :
+    Total r where
+  total a b := (Trichotomous.rel_or_eq_or_rel_swap (a := a) (b := b) (r := r)).elim Or.inl <|
     fun h => h.elim (fun h => h ▸ Or.inl (Refl.refl _)) Or.inr
 
-public def asymm_of_irrefl_of_antisymm (r : α → α → Prop) [Irrefl r] [Antisymm r] : Asymm r where
+public theorem asymm_of_irrefl_of_antisymm (r : α → α → Prop) [Irrefl r] [Antisymm r] : Asymm r where
   asymm a b h h' := Irrefl.irrefl _ (Antisymm.antisymm a b h h' ▸ h)
 
-public def Total.asymm_of_total_not {r : α → α → Prop} [i : Total (¬ r · ·)] : Asymm r where
+public theorem Total.asymm_of_total_not {r : α → α → Prop} [i : Total (¬ r · ·)] : Asymm r where
   asymm a b h := by cases i.total a b <;> trivial
 
 public theorem Asymm.total_not {r : α → α → Prop} [i : Asymm r] : Total (¬ r · ·) where
@@ -130,8 +136,8 @@ public theorem not_lt_of_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a
     (h : a ≤ b) : ¬ b < a := imp_not_comm.1 not_le_of_gt h
 
 public instance {α : Type u} {_ : LE α} [LT α] [LawfulOrderLT α]
-    [Tricho (α := α) (· < ·)] : Antisymm (α := α) (· ≤ ·) where
-  antisymm _ _ hab hba := Tricho.tricho _ _ (not_lt_of_ge hba) (not_lt_of_ge hab)
+    [Trichotomous (α := α) (· < ·)] : Antisymm (α := α) (· ≤ ·) where
+  antisymm _ _ hab hba := Trichotomous.trichotomous _ _ (not_lt_of_ge hba) (not_lt_of_ge hab)
 
 public theorem not_gt_of_lt {α : Type u} [LT α] [i : Std.Asymm (α := α) (· < ·)] {a b : α}
     (h : a < b) : ¬ b < a :=
@@ -151,8 +157,8 @@ public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
     intro h h'
     exact h.2.elim h'.1
 
-@[deprecated Asymm.total_not (since := "2025-10-24")]
-public def instIrreflLtOfIsPreorderOfLawfulOrderLT {α : Type u} [LT α] [LE α] [IsPreorder α]
+@[deprecated instIrreflOfAsymm (since := "2025-10-24")]
+public theorem instIrreflLtOfIsPreorderOfLawfulOrderLT {α : Type u} [LT α] [LE α]
     [LawfulOrderLT α] : Std.Irrefl (α := α) (· < ·) := inferInstance
 
 public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) ]
@@ -175,8 +181,8 @@ public theorem not_le {α : Type u} [LT α] [LE α] [Std.Total (α := α) (· 
   exact le_of_not_ge
 
 public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
-    [Total (α := α) (· ≤ ·)] [Antisymm (α := α) (· ≤ ·)] : Tricho (α := α) (· < ·) where
-  tricho a b hab hba := by
+    [Total (α := α) (· ≤ ·)] [Antisymm (α := α) (· ≤ ·)] : Trichotomous (α := α) (· < ·) where
+  trichotomous a b hab hba := by
     simp only [not_lt] at hab hba
     exact Antisymm.antisymm (r := (· ≤ ·)) a b hba hab
 
@@ -188,7 +194,7 @@ public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
     exact le_trans hbc hab
 
 @[deprecated Asymm.total_not (since := "2025-10-24")]
-public def instTotalNotLtOfLawfulOrderLTOfLe {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
+public theorem instTotalNotLtOfLawfulOrderLTOfLe {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
     : Total (α := α) (¬ · < ·) := Asymm.total_not
 
 public theorem lt_of_le_of_lt {α : Type u} [LE α] [LT α]

src/Init/Data/String/Lemmas.lean

@@ -28,7 +28,7 @@ protected theorem ne_of_data_ne {a b : String} (h : a.data ≠ b.data) : a ≠ b
 @[simp] protected theorem le_refl (a : String) : a ≤ a := List.le_refl _
 @[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
 
-attribute [local instance] Char.notLTTrans Char.ltTricho Char.ltAsymm
+attribute [local instance] Char.notLTTrans Char.ltTrichotomous Char.ltAsymm
 
 protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
 protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans