refactor(order/rel_classes): ditch is_strict_total_order' (#16069)

Since Lean 3.46, `is_strict_total_order` and `is_strict_total_order'` are exactly the same typeclass. Hence, we remove the latter for the former.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/data/list/lex.lean

@@ -93,7 +93,7 @@ instance is_asymm (r : α → α → Prop)
 end⟩
 
 instance is_strict_total_order (r : α → α → Prop)
-  [is_strict_total_order' α r] : is_strict_total_order' (list α) (lex r) :=
+  [is_strict_total_order α r] : is_strict_total_order (list α) (lex r) :=
 {..is_strict_weak_order_of_is_order_connected}
 
 instance decidable_rel [decidable_eq α] (r : α → α → Prop)
@@ -157,7 +157,7 @@ theorem nil_lt_cons [has_lt α] (a : α) (l : list α) : [] < a :: l :=
 lex.nil
 
 instance [linear_order α] : linear_order (list α) :=
-linear_order_of_STO' (lex (<))
+linear_order_of_STO (lex (<))
 
 --Note: this overrides an instance in core lean
 instance has_le' [linear_order α] : has_le (list α) :=

src/data/pi/lex.lean

@@ -83,7 +83,7 @@ partial_order_of_SO (<)
 /-- `Πₗ i, α i` is a linear order if the original order is well-founded. -/
 noncomputable instance [linear_order ι] [is_well_order ι (<)] [∀ a, linear_order (β a)] :
   linear_order (lex (Π i, β i)) :=
-@linear_order_of_STO' (Πₗ i, β i) (<)
+@linear_order_of_STO (Πₗ i, β i) (<)
   { to_is_trichotomous := is_trichotomous_lex _ _ is_well_founded.wf } (classical.dec_rel _)
 
 lemma lex.le_of_forall_le [linear_order ι] [is_well_order ι (<)] [Π a, linear_order (β a)]

src/order/rel_classes.lean

@@ -145,17 +145,11 @@ See note [reducible non-instances]. -/
       (asymm h)⟩,
     λ ⟨h₁, h₂⟩, h₁.resolve_left (λ e, h₂ $ e ▸ or.inl rfl)⟩ }
 
-/-- This is basically the same as `is_strict_total_order`, but that definition has a redundant
-assumption `is_incomp_trans α lt`. -/
--- TODO: This is now exactly the same as `is_strict_total_order`, remove.
-@[algebra] class is_strict_total_order' (α : Type u) (lt : α → α → Prop)
-  extends is_trichotomous α lt, is_strict_order α lt : Prop.
-
-/-- Construct a linear order from an `is_strict_total_order'` relation.
+/-- Construct a linear order from an `is_strict_total_order` relation.
 
 See note [reducible non-instances]. -/
 @[reducible]
-def linear_order_of_STO' (r) [is_strict_total_order' α r] [Π x y, decidable (¬ r x y)] :
+def linear_order_of_STO (r) [is_strict_total_order α r] [Π x y, decidable (¬ r x y)] :
   linear_order α :=
 { le_total := λ x y,
     match y, trichotomous_of r x y with
@@ -168,8 +162,8 @@ def linear_order_of_STO' (r) [is_strict_total_order' α r] [Π x y, decidable (
       λ h, h.elim (λ h, h ▸ irrefl_of _ _) (asymm_of r)⟩,
   ..partial_order_of_SO r }
 
-theorem is_strict_total_order'.swap (r) [is_strict_total_order' α r] :
-  is_strict_total_order' α (swap r) :=
+theorem is_strict_total_order.swap (r) [is_strict_total_order α r] :
+  is_strict_total_order α (swap r) :=
 {..is_trichotomous.swap r, ..is_strict_order.swap r}
 
 /-! ### Order connection -/
@@ -193,25 +187,15 @@ theorem is_strict_weak_order_of_is_order_connected [is_asymm α r]
   ..@is_asymm.is_irrefl α r _ }
 
 @[priority 100] -- see Note [lower instance priority]
-instance is_order_connected_of_is_strict_total_order'
-  [is_strict_total_order' α r] : is_order_connected α r :=
+instance is_order_connected_of_is_strict_total_order
+  [is_strict_total_order α r] : is_order_connected α r :=
 ⟨λ a b c h, (trichotomous _ _).imp_right (λ o,
   o.elim (λ e, e ▸ h) (λ h', trans h' h))⟩
 
-@[priority 100] -- see Note [lower instance priority]
-instance is_strict_total_order_of_is_strict_total_order'
-  [is_strict_total_order' α r] : is_strict_total_order α r :=
-{ }
-
-@[priority 100] -- see Note [lower instance priority]
-instance is_strict_weak_order_of_is_strict_total_order'
-  [is_strict_total_order' α r] : is_strict_weak_order α r :=
-{ ..is_strict_weak_order_of_is_order_connected }
-
 @[priority 100] -- see Note [lower instance priority]
 instance is_strict_weak_order_of_is_strict_total_order
   [is_strict_total_order α r] : is_strict_weak_order α r :=
-by { haveI : is_strict_total_order' α r := {}, apply_instance }
+{ ..is_strict_weak_order_of_is_order_connected }
 
 /-! ### Well-order -/
 
@@ -281,11 +265,8 @@ theorem well_founded_lt_dual_iff (α : Type*) [has_lt α] : well_founded_lt α
   extends is_trichotomous α r, is_trans α r, is_well_founded α r : Prop
 
 @[priority 100] -- see Note [lower instance priority]
-instance is_well_order.is_strict_total_order' {α} (r : α → α → Prop) [is_well_order α r] :
-  is_strict_total_order' α r := { }
-@[priority 100] -- see Note [lower instance priority]
 instance is_well_order.is_strict_total_order {α} (r : α → α → Prop) [is_well_order α r] :
-  is_strict_total_order α r := by apply_instance
+  is_strict_total_order α r := { }
 @[priority 100] -- see Note [lower instance priority]
 instance is_well_order.is_trichotomous {α} (r : α → α → Prop) [is_well_order α r] :
   is_trichotomous α r := by apply_instance
@@ -352,7 +333,7 @@ end well_founded_gt
 /-- Construct a decidable linear order from a well-founded linear order. -/
 noncomputable def is_well_order.linear_order (r : α → α → Prop) [is_well_order α r] :
   linear_order α :=
-by { letI := λ x y, classical.dec (¬r x y), exact linear_order_of_STO' r }
+by { letI := λ x y, classical.dec (¬r x y), exact linear_order_of_STO r }
 
 /-- Derive a `has_well_founded` instance from a `is_well_order` instance. -/
 def is_well_order.to_has_well_founded [has_lt α] [hwo : is_well_order α (<)] :
@@ -604,8 +585,7 @@ instance [linear_order α] : is_trichotomous α (<) := ⟨lt_trichotomy⟩
 instance [linear_order α] : is_trichotomous α (>) := is_trichotomous.swap _
 instance [linear_order α] : is_trichotomous α (≤) := is_total.is_trichotomous _
 instance [linear_order α] : is_trichotomous α (≥) := is_total.is_trichotomous _
-instance [linear_order α] : is_strict_total_order α (<) := by apply_instance
-instance [linear_order α] : is_strict_total_order' α (<) := {}
+instance [linear_order α] : is_strict_total_order α (<) := {}
 instance [linear_order α] : is_order_connected α (<) := by apply_instance
 instance [linear_order α] : is_incomp_trans α (<) := by apply_instance
 instance [linear_order α] : is_strict_weak_order α (<) := by apply_instance

src/order/rel_iso.lean

@@ -290,8 +290,8 @@ protected theorem is_strict_order : ∀ (f : r ↪r s) [is_strict_order β s], i
 protected theorem is_trichotomous : ∀ (f : r ↪r s) [is_trichotomous β s], is_trichotomous α r
 | ⟨f, o⟩ ⟨H⟩ := ⟨λ a b, (or_congr o (or_congr f.inj'.eq_iff o)).1 (H _ _)⟩
 
-protected theorem is_strict_total_order' :
-  ∀ (f : r ↪r s) [is_strict_total_order' β s], is_strict_total_order' α r
+protected theorem is_strict_total_order :
+  ∀ (f : r ↪r s) [is_strict_total_order β s], is_strict_total_order α r
 | f H := by exactI {..f.is_trichotomous, ..f.is_strict_order}
 
 protected theorem acc (f : r ↪r s) (a : α) : acc s (f a) → acc r a :=
@@ -305,7 +305,7 @@ protected theorem well_founded : ∀ (f : r ↪r s) (h : well_founded s), well_f
 | f ⟨H⟩ := ⟨λ a, f.acc _ (H _)⟩
 
 protected theorem is_well_order : ∀ (f : r ↪r s) [is_well_order β s], is_well_order α r
-| f H := by exactI {wf := f.well_founded H.wf, ..f.is_strict_total_order'}
+| f H := by exactI {wf := f.well_founded H.wf, ..f.is_strict_total_order}
 
 /-- `quotient.out` as a relation embedding between the lift of a relation and the relation. -/
 @[simps] noncomputable def _root_.quotient.out_rel_embedding [s : setoid α] {r : α → α → Prop} (H) :

src/set_theory/cardinal/ordinal.lean

@@ -404,7 +404,7 @@ begin
     quotient.induction_on c $ λ α IH ol, _) h,
   -- consider the minimal well-order `r` on `α` (a type with cardinality `c`).
   rcases ord_eq α with ⟨r, wo, e⟩, resetI,
-  letI := linear_order_of_STO' r,
+  letI := linear_order_of_STO r,
   haveI : is_well_order α (<) := wo,
   -- Define an order `s` on `α × α` by writing `(a, b) < (c, d)` if `max a b < max c d`, or
   -- the max are equal and `a < c`, or the max are equal and `a = c` and `b < d`.

src/topology/metric_space/emetric_paracompact.lean

@@ -46,7 +46,7 @@ begin
   refine ⟨λ ι s ho hcov, _⟩,
   simp only [Union_eq_univ_iff] at hcov,
   -- choose a well founded order on `S`
-  letI : linear_order ι := linear_order_of_STO' well_ordering_rel,
+  letI : linear_order ι := linear_order_of_STO well_ordering_rel,
   have wf : well_founded ((<) : ι → ι → Prop) := @is_well_founded.wf ι well_ordering_rel _,
   -- Let `ind x` be the minimal index `s : S` such that `x ∈ s`.
   set ind : α → ι := λ x, wf.min {i : ι | x ∈ s i} (hcov x),

src/topology/partition_of_unity.lean

@@ -361,7 +361,7 @@ begin
     exact λ i hi, f.support_to_pou_fun_subset i hi },
   have B : mul_support (λ i, 1 - f i x) ⊆ s,
   { rw [hs, mul_support_one_sub], exact λ i, id },
-  letI : linear_order ι := linear_order_of_STO' well_ordering_rel,
+  letI : linear_order ι := linear_order_of_STO well_ordering_rel,
   rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mul_support_subset _ B,
     finset.prod_one_sub_ordered, sub_sub_cancel],
   refine finset.sum_congr rfl (λ i hi, _),