fix: deprecate IsTotal in favour of Std.Total

Mathlib/Algebra/Group/Basic.lean

@@ -1027,41 +1027,49 @@ end CommGroup
 
 section multiplicative
 
-variable [Monoid β] (p r : α → α → Prop) [IsTotal α r] (f : α → α → β)
+variable [Monoid β] (p r : α → α → Prop) [Std.Total r] (f : α → α → β)
 
-@[to_additive additive_of_symmetric_of_isTotal]
-lemma multiplicative_of_symmetric_of_isTotal
+@[to_additive additive_of_symmetric_of_stdTotal]
+lemma multiplicative_of_symmetric_of_stdTotal
     (hsymm : Symmetric p) (hf_swap : ∀ {a b}, p a b → f a b * f b a = 1)
     (hmul : ∀ {a b c}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c)
     {a b c : α} (pab : p a b) (pbc : p b c) (pac : p a c) : f a c = f a b * f b c := by
   have hmul' : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c := by
     intro b c rbc pab pbc pac
-    obtain rab | rba := total_of r a b
+    obtain rab | rba := Std.Total.total (r := r) a b
     · exact hmul rab rbc pab pbc pac
     rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
-    obtain rac | rca := total_of r a c
+    obtain rac | rca := Std.Total.total (r := r) a c
     · rw [hmul rba rac (hsymm pab) pac pbc]
     · rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one]
-  obtain rbc | rcb := total_of r b c
+  obtain rbc | rcb := Std.Total.total (r := r) b c
   · exact hmul' rbc pab pbc pac
   · rw [hmul' rcb pac (hsymm pbc) pab, mul_assoc, hf_swap (hsymm pbc), mul_one]
 
+@[to_additive (attr := deprecated additive_of_symmetric_of_stdTotal (since := "2025-10-24"))
+additive_of_symmetric_of_isTotal]
+alias multiplicative_of_symmetric_of_isTotal := multiplicative_of_symmetric_of_stdTotal
+
 /-- If a binary function from a type equipped with a total relation `r` to a monoid is
   anti-symmetric (i.e. satisfies `f a b * f b a = 1`), in order to show it is multiplicative
   (i.e. satisfies `f a c = f a b * f b c`), we may assume `r a b` and `r b c` are satisfied.
   We allow restricting to a subset specified by a predicate `p`. -/
-@[to_additive additive_of_isTotal /-- If a binary function from a type equipped with a total
+@[to_additive additive_of_stdTotal /-- If a binary function from a type equipped with a total
   relation `r` to an additive monoid is anti-symmetric (i.e. satisfies `f a b + f b a = 0`), in
   order to show it is additive (i.e. satisfies `f a c = f a b + f b c`), we may assume `r a b` and
   `r b c` are satisfied. We allow restricting to a subset specified by a predicate `p`. -/]
-theorem multiplicative_of_isTotal (p : α → Prop) (hswap : ∀ {a b}, p a → p b → f a b * f b a = 1)
+theorem multiplicative_of_stdTotal (p : α → Prop) (hswap : ∀ {a b}, p a → p b → f a b * f b a = 1)
     (hmul : ∀ {a b c}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c) {a b c : α}
     (pa : p a) (pb : p b) (pc : p c) : f a c = f a b * f b c := by
-  apply multiplicative_of_symmetric_of_isTotal (fun a b => p a ∧ p b) r f fun _ _ => And.symm
+  apply multiplicative_of_symmetric_of_stdTotal (fun a b => p a ∧ p b) r f fun _ _ => And.symm
   · simp_rw [and_imp]; exact @hswap
   · exact fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2
   exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]
 
+@[to_additive (attr := deprecated additive_of_stdTotal (since := "2025-10-24"))
+additive_of_isTotal]
+alias multiplicative_of_isTotal := multiplicative_of_stdTotal
+
 end multiplicative
 
 /-- An auxiliary lemma that can be used to prove `⇑(f ^ n) = ⇑f^[n]`. -/

Mathlib/Algebra/Order/Archimedean/Class.lean

@@ -137,7 +137,7 @@ instance : Preorder (MulArchimedeanOrder M) where
     exact ⟨1, by simpa using h⟩
 
 @[to_additive]
-instance : IsTotal (MulArchimedeanOrder M) (· ≤ ·) where
+instance : Std.Total (α := MulArchimedeanOrder M) (· ≤ ·) where
   total a b := by
     obtain hab | hab := le_total |a.val|ₘ |b.val|ₘ
     · exact .inr ⟨1, by simpa using hab⟩

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -470,8 +470,9 @@ instance decidableLT [Preorder α] [DecidableLT α] : DecidableLT (WithZero α)
   | 0, (a : α) => isTrue <| by simp
   | (a : α), (b : α) => decidable_of_iff' _ coe_lt_coe
 
-instance isTotal_le [Preorder α] [IsTotal α (· ≤ ·)] : IsTotal (WithZero α) (· ≤ ·) where
-  total x y := by cases x <;> cases y <;> simp; simpa using IsTotal.total ..
+instance inst_stdTotal_le [Preorder α] [Std.Total (α := α) (· ≤ ·)] :
+    Std.Total (α := WithZero α) (· ≤ ·) where
+  total x y := by cases x <;> cases y <;> simp; simpa using Std.Total.total ..
 
 section LinearOrder
 variable [LinearOrder α] {a b c : α} {x y : WithZero α}

Mathlib/Algebra/Order/Ring/Canonical.lean

@@ -88,20 +88,20 @@ section Sub
 section NonUnitalNonAssocSemiring
 
 variable [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R]
-  [Sub R] [OrderedSub R] [IsTotal R (· ≤ ·)]
+  [Sub R] [OrderedSub R] [Std.Total (α := R) (· ≤ ·)]
 
 namespace AddLECancellable
 
 protected theorem mul_tsub {a b c : R}
     (h : AddLECancellable (a * c)) : a * (b - c) = a * b - a * c := by
-  obtain (hbc | hcb) := total_of (· ≤ ·) b c
+  obtain (hbc | hcb) := Std.Total.total (r := (· ≤ ·)) b c
   · rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)]
   · apply h.eq_tsub_of_add_eq
     rw [← mul_add, tsub_add_cancel_of_le hcb]
 
 protected theorem tsub_mul [MulRightMono R] {a b c : R}
     (h : AddLECancellable (b * c)) : (a - b) * c = a * c - b * c := by
-  obtain (hab | hba) := total_of (· ≤ ·) a b
+  obtain (hab | hba) := Std.Total.total (r := (· ≤ ·)) a b
   · rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_right' hab c)]
   · apply h.eq_tsub_of_add_eq
     rw [← add_mul, tsub_add_cancel_of_le hba]
@@ -122,7 +122,7 @@ end NonUnitalNonAssocSemiring
 section NonAssocSemiring
 
 variable [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R]
-  [Sub R] [OrderedSub R] [IsTotal R (· ≤ ·)]
+  [Sub R] [OrderedSub R] [Std.Total (α := R) (· ≤ ·)]
 
 lemma mul_tsub_one [AddLeftReflectLE R] (a b : R) :
     a * (b - 1) = a * b - a := by rw [mul_tsub, mul_one]
@@ -134,7 +134,7 @@ end NonAssocSemiring
 section CommSemiring
 
 variable [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R]
-  [Sub R] [OrderedSub R] [IsTotal R (· ≤ ·)] [AddLeftReflectLE R]
+  [Sub R] [OrderedSub R] [Std.Total (α := R) (· ≤ ·)] [AddLeftReflectLE R]
 
 /-- The `tsub` version of `mul_self_sub_mul_self`. Notably, this holds for `Nat` and `NNReal`. -/
 theorem mul_self_tsub_mul_self (a b : R) :

Mathlib/Data/Finset/Sort.lean

@@ -26,14 +26,14 @@ section sort
 /-- `sort s` constructs a sorted list from the unordered set `s`.
   (Uses merge sort algorithm.) -/
 def sort (s : Finset α) (r : α → α → Prop := by exact fun a b => a ≤ b)
-    [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : List α :=
+    [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [Std.Total r] : List α :=
   Multiset.sort s.1 r
 
 section
 
 variable (f : α ↪ β) (s : Finset α)
-variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r]
-variable (r' : β → β → Prop) [DecidableRel r'] [IsTrans β r'] [IsAntisymm β r'] [IsTotal β r']
+variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [Std.Total r]
+variable (r' : β → β → Prop) [DecidableRel r'] [IsTrans β r'] [IsAntisymm β r'] [Std.Total r']
 
 @[simp]
 theorem sort_val : Multiset.sort s.val r  = sort s r :=
@@ -95,7 +95,7 @@ end
 section
 
 variable {m : Multiset α} {s : Finset α}
-variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r]
+variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [Std.Total r]
 
 @[simp]
 theorem sort_mk (h : m.Nodup) : sort ⟨m, h⟩ r = m.sort r := rfl

Mathlib/Data/List/Sort.lean

@@ -584,7 +584,7 @@ theorem Sublist.orderedInsert_sublist [IsTrans α r] {as bs} (x) (hs : as <+ bs)
 
 section TotalAndTransitive
 
-variable [IsTotal α r] [IsTrans α r]
+variable [Std.Total r] [IsTrans α r]
 
 theorem Sorted.orderedInsert (a : α) : ∀ l, Sorted r l → Sorted r (orderedInsert r a l)
   | [], _ => sorted_singleton a
@@ -596,7 +596,7 @@ theorem Sorted.orderedInsert (a : α) : ∀ l, Sorted r l → Sorted r (orderedI
       intro b' bm
       rcases (mem_orderedInsert r).mp bm with be | bm
       · subst b'
-        exact (total_of r _ _).resolve_left h'
+        exact (Std.Total.total _ _).resolve_left h'
       · exact rel_of_sorted_cons h _ bm
 
 variable (r)
@@ -631,11 +631,11 @@ theorem pair_sublist_insertionSort {a b : α} {l : List α} (hab : r a b) (h : [
     [a, b] <+ insertionSort r l :=
   sublist_insertionSort (pairwise_pair.mpr hab) h
 
-variable [IsAntisymm α r] [IsTotal α r] [IsTrans α r]
+variable [IsAntisymm α r] [Std.Total r] [IsTrans α r]
 
 /--
 A version of `insertionSort_stable` which only assumes `c <+~ l` (instead of `c <+ l`), but
-additionally requires `IsAntisymm α r`, `IsTotal α r` and `IsTrans α r`.
+additionally requires `IsAntisymm α r`, `Std.Total r` and `IsTrans α r`.
 -/
 theorem sublist_insertionSort' {l c : List α} (hs : c.Sorted r) (hc : c <+~ l) :
     c <+ insertionSort r l := by
@@ -682,13 +682,13 @@ section Correctness
 
 section TotalAndTransitive
 
-variable {r} [IsTotal α r] [IsTrans α r]
+variable {r} [Std.Total r] [IsTrans α r]
 
 theorem Sorted.merge {l l' : List α} (h : Sorted r l) (h' : Sorted r l') :
     Sorted r (merge l l' (r · ·)) := by
   simpa using sorted_merge (le := (r · ·))
     (fun a b c h₁ h₂ => by simpa using _root_.trans (by simpa using h₁) (by simpa using h₂))
-    (fun a b => by simpa using IsTotal.total a b)
+    (fun a b => by simpa using Std.Total.total a b)
     l l' (by simpa using h) (by simpa using h')
 
 variable (r)
@@ -697,7 +697,7 @@ variable (r)
 theorem sorted_mergeSort' (l : List α) : Sorted r (mergeSort l (r · ·)) := by
   simpa using sorted_mergeSort (le := (r · ·))
     (fun _ _ _ => by simpa using trans_of r)
-    (by simpa using total_of r)
+    (by simpa using Std.Total.total)
     l
 
 variable [IsAntisymm α r]

Mathlib/Data/Multiset/Sort.lean

@@ -23,19 +23,19 @@ section sort
 /-- `sort s` constructs a sorted list from the multiset `s`.
   (Uses merge sort algorithm.) -/
 def sort (s : Multiset α) (r : α → α → Prop := by exact fun a b => a ≤ b)
-    [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : List α :=
+    [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [Std.Total r] : List α :=
   Quot.liftOn s (mergeSort · (r · ·)) fun _ _ h =>
     eq_of_perm_of_sorted ((mergeSort_perm _ _).trans <| h.trans (mergeSort_perm _ _).symm)
       (sorted_mergeSort IsTrans.trans
-        (fun a b => by simpa using IsTotal.total a b) _)
+        (fun a b => by simpa using Std.Total.total a b) _)
       (sorted_mergeSort IsTrans.trans
-        (fun a b => by simpa using IsTotal.total a b) _)
+        (fun a b => by simpa using Std.Total.total a b) _)
 
 section
 
 variable (a : α) (f : α → β) (l : List α) (s : Multiset α)
-variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r]
-variable (r' : β → β → Prop) [DecidableRel r'] [IsTrans β r'] [IsAntisymm β r'] [IsTotal β r']
+variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [Std.Total r]
+variable (r' : β → β → Prop) [DecidableRel r'] [IsTrans β r'] [IsAntisymm β r'] [Std.Total r']
 
 @[simp]
 theorem coe_sort : sort l r = mergeSort l (r · ·) :=
@@ -75,7 +75,7 @@ end
 section
 
 variable {a : α} {s : Multiset α}
-variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r]
+variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [Std.Total r]
 
 @[simp]
 theorem mem_sort : a ∈ sort s r ↔ a ∈ s := by rw [← mem_coe, sort_eq]

Mathlib/Data/Nat/PartENat.lean

@@ -379,15 +379,15 @@ theorem pos_iff_one_le {x : PartENat} : 0 < x ↔ 1 ≤ x :=
       rw [← Nat.cast_zero, ← Nat.cast_one, PartENat.coe_lt_coe, PartENat.coe_le_coe]
       rfl
 
-instance isTotal : IsTotal PartENat (· ≤ ·) where
+instance inst_stdTotal_le : Std.Total (α := PartENat) (· ≤ ·) where
   total x y :=
     PartENat.casesOn (P := fun z => z ≤ y ∨ y ≤ z) x (Or.inr le_top)
       (PartENat.casesOn y (fun _ => Or.inl le_top) fun x y =>
         (le_total x y).elim (Or.inr ∘ coe_le_coe.2) (Or.inl ∘ coe_le_coe.2))
 
 noncomputable instance linearOrder : LinearOrder PartENat :=
   { PartENat.partialOrder with
-    le_total := IsTotal.total
+    le_total := Std.Total.total
     toDecidableLE := Classical.decRel _
     max := (· ⊔ ·)
     max_def a b := congr_fun₂ (@sup_eq_maxDefault PartENat _ (_) _) _ _ }

Mathlib/Data/Ordmap/Invariants.lean

@@ -539,7 +539,7 @@ theorem merge_node {ls ll lx lr rs rl rx rr} :
 /-! ### `insert` -/
 
 
-theorem dual_insert [LE α] [IsTotal α (· ≤ ·)] [DecidableLE α] (x : α) :
+theorem dual_insert [LE α] [Std.Total (α := α) (· ≤ ·)] [DecidableLE α] (x : α) :
     ∀ t : Ordnode α, dual (Ordnode.insert x t) = @Ordnode.insert αᵒᵈ _ _ x (dual t)
   | nil => rfl
   | node _ l y r => by

Mathlib/Data/Ordmap/Ordset.lean

@@ -473,7 +473,7 @@ theorem Valid.merge {l r} (hl : Valid l) (hr : Valid r)
     (sep : l.All fun x => r.All fun y => x < y) : Valid (@merge α l r) :=
   (Valid'.merge_aux hl hr sep).1
 
-theorem insertWith.valid_aux [IsTotal α (· ≤ ·)] [DecidableLE α] (f : α → α) (x : α)
+theorem insertWith.valid_aux [Std.Total (α := α) (· ≤ ·)] [DecidableLE α] (f : α → α) (x : α)
     (hf : ∀ y, x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) :
     ∀ {t o₁ o₂},
       Valid' o₁ t o₂ →
@@ -494,15 +494,15 @@ theorem insertWith.valid_aux [IsTotal α (· ≤ ·)] [DecidableLE α] (f : α 
         rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
         exact (e.add_right _).add_right _
       exact Or.inl ⟨_, e, h.3.1⟩
-    · have : y < x := lt_of_le_not_ge ((total_of (· ≤ ·) _ _).resolve_left h_1) h_1
+    · have : y < x := lt_of_le_not_ge ((Std.Total.total _ _).resolve_left h_1) h_1
       rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩
       suffices H : _ by
         refine ⟨h.left.balanceR vr H, ?_⟩
         rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]
         exact (e.add_left _).add_right _
       exact Or.inr ⟨_, e, h.3.1⟩
 
-theorem insertWith.valid [IsTotal α (· ≤ ·)] [DecidableLE α] (f : α → α) (x : α)
+theorem insertWith.valid [Std.Total (α := α) (· ≤ ·)] [DecidableLE α] (f : α → α) (x : α)
     (hf : ∀ y, x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) {t} (h : Valid t) : Valid (insertWith f x t) :=
   (insertWith.valid_aux _ _ hf h ⟨⟩ ⟨⟩).1
 
@@ -512,7 +512,7 @@ theorem insert_eq_insertWith [DecidableLE α] (x : α) :
   | node _ l y r => by
     unfold Ordnode.insert insertWith; cases cmpLE x y <;> simp [insert_eq_insertWith]
 
-theorem insert.valid [IsTotal α (· ≤ ·)] [DecidableLE α] (x : α) {t} (h : Valid t) :
+theorem insert.valid [Std.Total (α := α) (· ≤ ·)] [DecidableLE α] (x : α) {t} (h : Valid t) :
     Valid (Ordnode.insert x t) := by
   rw [insert_eq_insertWith]; exact insertWith.valid _ _ (fun _ _ => ⟨le_rfl, le_rfl⟩) h
 
@@ -522,7 +522,7 @@ theorem insert'_eq_insertWith [DecidableLE α] (x : α) :
   | node _ l y r => by
     unfold insert' insertWith; cases cmpLE x y <;> simp [insert'_eq_insertWith]
 
-theorem insert'.valid [IsTotal α (· ≤ ·)] [DecidableLE α]
+theorem insert'.valid [Std.Total (α := α) (· ≤ ·)] [DecidableLE α]
     (x : α) {t} (h : Valid t) : Valid (insert' x t) := by
   rw [insert'_eq_insertWith]; exact insertWith.valid _ _ (fun _ => id) h
 
@@ -684,16 +684,16 @@ instance Empty.instDecidablePred : DecidablePred (@Empty α _) :=
 
 /-- O(log n). Insert an element into the set, preserving balance and the BST property.
   If an equivalent element is already in the set, this replaces it. -/
-protected def insert [IsTotal α (· ≤ ·)] [DecidableLE α] (x : α) (s : Ordset α) :
+protected def insert [Std.Total (α := α) (· ≤ ·)] [DecidableLE α] (x : α) (s : Ordset α) :
     Ordset α :=
   ⟨Ordnode.insert x s.1, insert.valid _ s.2⟩
 
-instance instInsert [IsTotal α (· ≤ ·)] [DecidableLE α] : Insert α (Ordset α) :=
+instance instInsert [Std.Total (α := α) (· ≤ ·)] [DecidableLE α] : Insert α (Ordset α) :=
   ⟨Ordset.insert⟩
 
 /-- O(log n). Insert an element into the set, preserving balance and the BST property.
   If an equivalent element is already in the set, the set is returned as is. -/
-nonrec def insert' [IsTotal α (· ≤ ·)] [DecidableLE α] (x : α) (s : Ordset α) :
+nonrec def insert' [Std.Total (α := α) (· ≤ ·)] [DecidableLE α] (x : α) (s : Ordset α) :
     Ordset α :=
   ⟨insert' x s.1, insert'.valid _ s.2⟩
 

Mathlib/Data/Prod/Basic.lean

@@ -179,16 +179,17 @@ instance {r : α → α → Prop} {s : β → β → Prop} [IsStrictOrder α r]
     | (_, _), (_, _), .right _ _,     .left  _ _ hr₂ => (irrefl _ hr₂).elim
     | (_, _), (_, _), .right _ hs₁,   .right _ hs₂   => antisymm hs₁ hs₂ ▸ rfl⟩
 
-instance isTotal_left {r : α → α → Prop} {s : β → β → Prop} [IsTotal α r] :
-    IsTotal (α × β) (Prod.Lex r s) :=
-  ⟨fun ⟨a₁, _⟩ ⟨a₂, _⟩ ↦ (IsTotal.total a₁ a₂).imp (Lex.left _ _) (Lex.left _ _)⟩
+instance inst_stdTotal_left {r : α → α → Prop} {s : β → β → Prop} [Std.Total r] :
+    Std.Total (Prod.Lex r s) :=
+  ⟨fun ⟨a₁, _⟩ ⟨a₂, _⟩ ↦ (Std.Total.total a₁ a₂).imp (Lex.left _ _) (Lex.left _ _)⟩
 
-instance isTotal_right {r : α → α → Prop} {s : β → β → Prop} [IsTrichotomous α r] [IsTotal β s] :
-    IsTotal (α × β) (Prod.Lex r s) :=
+instance inst_stdTotal_right {r : α → α → Prop} {s : β → β → Prop} [IsTrichotomous α r]
+    [Std.Total s] :
+    Std.Total (Prod.Lex r s) :=
   ⟨fun ⟨i, a⟩ ⟨j, b⟩ ↦ by
     obtain hij | rfl | hji := trichotomous_of r i j
     · exact Or.inl (.left _ _ hij)
-    · exact (total_of s a b).imp (.right _) (.right _)
+    · exact (Std.Total.total a b).imp (.right _) (.right _)
     · exact Or.inr (.left _ _ hji) ⟩
 
 instance IsTrichotomous [IsTrichotomous α r] [IsTrichotomous β s] :

Mathlib/Data/Prod/Lex.lean

@@ -167,7 +167,7 @@ instance [Ord α] [Ord β] [Std.TransOrd α] [Std.TransOrd β] : Std.TransOrd (
 /-- Dictionary / lexicographic linear order for pairs. -/
 instance instLinearOrder (α β : Type*) [LinearOrder α] [LinearOrder β] : LinearOrder (α ×ₗ β) :=
   { Prod.Lex.instPartialOrder α β with
-    le_total := total_of (Prod.Lex _ _)
+    le_total := Std.Total.total (r := Prod.Lex _ _)
     toDecidableLE := Prod.Lex.decidable _ _
     toDecidableLT := Prod.Lex.decidable _ _
     toDecidableEq := instDecidableEqLex _

Mathlib/Data/Real/Basic.lean

@@ -455,7 +455,7 @@ instance : SemilatticeInf ℝ :=
 instance : SemilatticeSup ℝ :=
   inferInstance
 
-instance leTotal_R : IsTotal ℝ (· ≤ ·) :=
+instance inst_stdTotal_le : Std.Total (α := ℝ) (· ≤ ·) :=
   ⟨by
     intro a b
     induction a using Real.ind_mk

Mathlib/Data/Sigma/Lex.lean

@@ -112,12 +112,12 @@ instance [IsAsymm ι r] [∀ i, IsAntisymm (α i) (s i)] : IsAntisymm _ (Lex r s
     · exact (irrefl _ hji).elim
     · exact congr_arg (Sigma.mk _ ·) <| antisymm hab hba⟩
 
-instance [IsTrichotomous ι r] [∀ i, IsTotal (α i) (s i)] : IsTotal _ (Lex r s) :=
+instance [IsTrichotomous ι r] [∀ i, Std.Total (s i)] : Std.Total (Lex r s) :=
   ⟨by
     rintro ⟨i, a⟩ ⟨j, b⟩
     obtain hij | rfl | hji := trichotomous_of r i j
     · exact Or.inl (Lex.left _ _ hij)
-    · obtain hab | hba := total_of (s i) a b
+    · obtain hab | hba := Std.Total.total (r := s i) a b
       · exact Or.inl (Lex.right _ _ hab)
       · exact Or.inr (Lex.right _ _ hba)
     · exact Or.inr (Lex.left _ _ hji)⟩

Mathlib/Data/Sigma/Order.lean

@@ -164,7 +164,7 @@ instance partialOrder [Preorder ι] [∀ i, PartialOrder (α i)] :
 instance linearOrder [LinearOrder ι] [∀ i, LinearOrder (α i)] :
     LinearOrder (Σₗ i, α i) :=
   { Lex.partialOrder with
-    le_total := total_of ((Lex (· < ·)) fun _ => (· ≤ ·)),
+    le_total := Std.Total.total (r := (Lex (· < ·)) fun _ => (· ≤ ·)),
     toDecidableEq := Sigma.instDecidableEqSigma
     toDecidableLE := Lex.decidable _ _
     toDecidableLT := Lex.decidable _ _ }