Fix build issues

Author: linesthatinterlace

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.Antisymm (¬ · < · : α → α → Prop)]
+    [i₂ : Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [i₂ : Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)] {xs ys : Array α} :
+    [Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
-    [Std.Antisymm (¬ · < · : β → β → Prop)]
+    [Std.Tricho (· < · : β → β → 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,8 @@ instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
   antisymm _ _ := Char.le_antisymm
 
 -- This instance is useful while setting up instances for `String`.
-def notLTAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where
-  antisymm _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
+def ltTricho : Std.Tricho (· < · : Char → Char → Prop) where
+  tricho _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
 
 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 not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
-    (antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
+theorem lex_tricho [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
+    (tricho : ∀ 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,20 @@ theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel
       · 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 [not_lex_antisymm antisymm h₁ h₂]
+        simp [lex_tricho tricho h₁ h₂]
       · exfalso
         by_cases hba : r b a
         · exact h₁ (Lex.rel hba)
-        · exact eq (antisymm _ _ hab hba)
+        · exact eq (tricho _ _ hab hba)
 
 protected theorem le_antisymm [LT α]
-    [i : Std.Antisymm (¬ · < · : α → α → Prop)]
+    [i : Std.Tricho (· < · : α → α → Prop)]
     {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
   open Classical in
-  not_lex_antisymm i.antisymm h₁ h₂
+  lex_tricho i.tricho h₁ h₂
 
 instance [LT α]
-    [s : Std.Antisymm (¬ · < · : α → α → Prop)] :
+    [s : Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [i₂ : Std.Tricho (· < · : α → α → 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₂.antisymm _ _ h₁ h₃
+      exact i₂.tricho _ _ h₁ h₃
     · if h₃ : a < b then
         exact .inl h₃
       else
         right
-        exact ⟨i₂.antisymm _ _ h₃ h₁, h₂⟩
+        exact ⟨i₂.tricho _ _ 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.Antisymm (¬ · < · : α → α → Prop)]
+    [i₂ : Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [i₂ : Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} :
+    [Std.Tricho (· < · : α → α → 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.Antisymm.antisymm
+  · simpa using Std.Tricho.tricho
 
 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.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → 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.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
-    [Std.Antisymm (¬ · < · : β → β → Prop)]
+    [Std.Tricho (· < · : β → β → 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,8 @@ 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.Antisymm (¬ . < . : Nat → Nat → Prop) where
-  antisymm _ _ h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt 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₁)
 
 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)
-    (not_lt_antisymm : Antisymm (α := α) (¬ · < ·) := by exact inferInstance) :
+    (lt_tricho : Tricho (α := α) (· < ·) := 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 => not_lt_antisymm.antisymm a b hba hab }
+      simpa [LE.ofLT] using fun a b hab hba => lt_tricho.tricho a b hba hab }
 
 /--
 This lemma characterizes in terms of `LT α` when a `Min α` instance

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.notLTAntisymm Char.notLTTotal
+attribute [local instance] Char.notLTTrans Char.ltTricho 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

src/Init/Data/Vector/Lex.lean

@@ -104,7 +104,7 @@ protected theorem lt_of_le_of_lt [LT α] [LE α] [LawfulOrderLT α] [IsLinearOrd
 @[deprecated Vector.lt_of_le_of_lt (since := "2025-08-01")]
 protected theorem lt_of_le_of_lt' [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → Prop)]
     [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
   letI := LE.ofLT α
@@ -118,7 +118,7 @@ protected theorem le_trans [LT α] [LE α] [LawfulOrderLT α] [IsLinearOrder α]
 @[deprecated Vector.le_trans (since := "2025-08-01")]
 protected theorem le_trans' [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → Prop)]
     [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
   letI := LE.ofLT α
@@ -175,7 +175,7 @@ protected theorem le_of_lt [LT α]
 
 protected theorem le_iff_lt_or_eq [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → Prop)]
     {xs ys : Vector α n} : xs ≤ ys ↔ xs < ys ∨ xs = ys := by
   simpa using Array.le_iff_lt_or_eq (xs := xs.toArray) (ys := ys.toArray)
 
@@ -246,7 +246,7 @@ protected theorem lt_iff_exists [LT α] {xs ys : Vector α n} :
 
 protected theorem le_iff_exists [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Antisymm (¬ · < · : α → α → Prop)] {xs ys : Vector α n} :
+    [Std.Tricho (· < · : α → α → Prop)] {xs ys : Vector α n} :
     xs ≤ ys ↔
       (xs = ys) ∨
         (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → xs[j] = ys[j]) ∧ xs[i] < ys[i]) := by
@@ -260,7 +260,7 @@ theorem append_left_lt [LT α] {xs : Vector α n} {ys ys' : Vector α m} (h : ys
 
 theorem append_left_le [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → Prop)]
     {xs : Vector α n} {ys ys' : Vector α m} (h : ys ≤ ys') :
     xs ++ ys ≤ xs ++ ys' := by
   simpa using Array.append_left_le h
@@ -272,9 +272,9 @@ protected theorem map_lt [LT α] [LT β]
 
 protected theorem map_le [LT α] [LT β]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Tricho (· < · : α → α → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
-    [Std.Antisymm (¬ · < · : β → β → Prop)]
+    [Std.Tricho (· < · : β → β → Prop)]
     {xs ys : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : xs ≤ ys) :
     map f xs ≤ map f ys := by
   simpa using Array.map_le w h