chore(Order): add missing inst prefix to instance names (#11238)

This is not exhaustive; it largely does not rename instances that relate to algebra, and only focuses on the "core" order files.

Mathlib/Algebra/Order/Kleene.lean

@@ -288,7 +288,7 @@ end KleeneAlgebra
 namespace Prod
 
 instance instIdemSemiring [IdemSemiring α] [IdemSemiring β] : IdemSemiring (α × β) :=
-  { Prod.instSemiring, Prod.semilatticeSup _ _, Prod.orderBot _ _ with
+  { Prod.instSemiring, Prod.instSemilatticeSup _ _, Prod.instOrderBot _ _ with
     add_eq_sup := fun _ _ ↦ ext (add_eq_sup _ _) (add_eq_sup _ _) }
 
 instance [IdemCommSemiring α] [IdemCommSemiring β] : IdemCommSemiring (α × β) :=
@@ -324,7 +324,7 @@ end Prod
 namespace Pi
 
 instance instIdemSemiring [∀ i, IdemSemiring (π i)] : IdemSemiring (∀ i, π i) :=
-  { Pi.semiring, Pi.semilatticeSup, Pi.orderBot with
+  { Pi.semiring, Pi.instSemilatticeSup, Pi.instOrderBot with
     add_eq_sup := fun _ _ ↦ funext fun _ ↦ add_eq_sup _ _ }
 
 instance [∀ i, IdemCommSemiring (π i)] : IdemCommSemiring (∀ i, π i) :=

Mathlib/Algebra/Order/Nonneg/Ring.lean

@@ -336,7 +336,7 @@ instance canonicallyOrderedCommSemiring [OrderedCommRing α] [NoZeroDivisors α]
 
 instance canonicallyLinearOrderedAddCommMonoid [LinearOrderedRing α] :
     CanonicallyLinearOrderedAddCommMonoid { x : α // 0 ≤ x } :=
-  { Subtype.linearOrder _, Nonneg.canonicallyOrderedAddCommMonoid with }
+  { Subtype.instLinearOrder _, Nonneg.canonicallyOrderedAddCommMonoid with }
 #align nonneg.canonically_linear_ordered_add_monoid Nonneg.canonicallyLinearOrderedAddCommMonoid
 
 section LinearOrder

Mathlib/Algebra/Order/Pi.lean

@@ -51,7 +51,7 @@ instance existsMulOfLe {ι : Type*} {α : ι → Type*} [∀ i, LE (α i)] [∀
 a canonically ordered additive monoid."]
 instance {ι : Type*} {Z : ι → Type*} [∀ i, CanonicallyOrderedCommMonoid (Z i)] :
     CanonicallyOrderedCommMonoid (∀ i, Z i) where
-  __ := Pi.orderBot
+  __ := Pi.instOrderBot
   __ := Pi.orderedCommMonoid
   __ := Pi.existsMulOfLe
   le_self_mul _ _ := fun _ => le_self_mul

Mathlib/Algebra/Order/Positive/Ring.lean

@@ -146,7 +146,7 @@ instance orderedCommMonoid [StrictOrderedCommSemiring R] [Nontrivial R] :
 ordered cancellative commutative monoid. -/
 instance linearOrderedCancelCommMonoid [LinearOrderedCommSemiring R] :
     LinearOrderedCancelCommMonoid { x : R // 0 < x } :=
-  { Subtype.linearOrder _, Positive.orderedCommMonoid with
+  { Subtype.instLinearOrder _, Positive.orderedCommMonoid with
     le_of_mul_le_mul_left := fun a _ _ h => Subtype.coe_le_coe.1 <| (mul_le_mul_left a.2).1 h }
 #align positive.subtype.linear_ordered_cancel_comm_monoid Positive.linearOrderedCancelCommMonoid
 

Mathlib/Algebra/PUnitInstances.lean

@@ -114,19 +114,19 @@ theorem norm_unit_eq {x : PUnit} : normUnit x = 1 :=
 
 instance canonicallyOrderedAddCommMonoid : CanonicallyOrderedAddCommMonoid PUnit := by
   refine'
-    { PUnit.commRing, PUnit.completeBooleanAlgebra with
+    { PUnit.commRing, PUnit.instCompleteBooleanAlgebra with
       exists_add_of_le := fun {_ _} _ => ⟨unit, Subsingleton.elim _ _⟩.. } <;>
     intros <;>
     trivial
 
 instance linearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid PUnit where
   __ := PUnit.canonicallyOrderedAddCommMonoid
-  __ := PUnit.linearOrder
+  __ := PUnit.instLinearOrder
   le_of_add_le_add_left _ _ _ _ := trivial
   add_le_add_left := by intros; rfl
 
 instance : LinearOrderedAddCommMonoidWithTop PUnit :=
-  { PUnit.completeBooleanAlgebra, PUnit.linearOrderedCancelAddCommMonoid with
+  { PUnit.instCompleteBooleanAlgebra, PUnit.linearOrderedCancelAddCommMonoid with
     top_add' := fun _ => rfl }
 
 @[to_additive]

Mathlib/Analysis/Normed/Order/Lattice.lean

@@ -107,8 +107,9 @@ theorem dual_solid (a b : α) (h : b ⊓ -b ≤ a ⊓ -a) : ‖a‖ ≤ ‖b‖
 /-- Let `α` be a normed lattice ordered group, then the order dual is also a
 normed lattice ordered group.
 -/
-instance (priority := 100) OrderDual.normedLatticeAddCommGroup : NormedLatticeAddCommGroup αᵒᵈ :=
-  { OrderDual.orderedAddCommGroup, OrderDual.normedAddCommGroup, OrderDual.lattice α with
+instance (priority := 100) OrderDual.instNormedLatticeAddCommGroup :
+    NormedLatticeAddCommGroup αᵒᵈ :=
+  { OrderDual.orderedAddCommGroup, OrderDual.normedAddCommGroup, OrderDual.instLattice α with
     solid := dual_solid (α := α) }
 
 theorem norm_abs_eq_norm (a : α) : ‖|a|‖ = ‖a‖ :=

Mathlib/Data/Nat/Order/Lemmas.lean

@@ -36,7 +36,7 @@ instance Subtype.orderBot (s : Set ℕ) [DecidablePred (· ∈ s)] [h : Nonempty
 #align nat.subtype.order_bot Nat.Subtype.orderBot
 
 instance Subtype.semilatticeSup (s : Set ℕ) : SemilatticeSup s :=
-  { Subtype.linearOrder s, LinearOrder.toLattice with }
+  { Subtype.instLinearOrder s, LinearOrder.toLattice with }
 #align nat.subtype.semilattice_sup Nat.Subtype.semilatticeSup
 
 theorem Subtype.coe_bot {s : Set ℕ} [DecidablePred (· ∈ s)] [h : Nonempty s] :

Mathlib/Data/Setoid/Basic.lean

@@ -460,6 +460,5 @@ theorem Quot.subsingleton_iff (r : α → α → Prop) : Subsingleton (Quot r) 
   refine' (surjective_quot_mk _).forall.trans (forall_congr' fun a => _)
   refine' (surjective_quot_mk _).forall.trans (forall_congr' fun b => _)
   rw [Quot.eq]
-  simp only [forall_const, le_Prop_eq, OrderTop.toTop, Pi.orderTop, Pi.top_apply,
-             Prop.top_eq_true, true_implies]
+  simp only [forall_const, le_Prop_eq, Pi.top_apply, Prop.top_eq_true, true_implies]
 #align quot.subsingleton_iff Quot.subsingleton_iff

Mathlib/Order/Basic.lean

@@ -1247,7 +1247,7 @@ instance decidableLT [Preorder α] [h : @DecidableRel α (· < ·)] {p : α →
 /-- A subtype of a linear order is a linear order. We explicitly give the proofs of decidable
 equality and decidable order in order to ensure the decidability instances are all definitionally
 equal. -/
-instance linearOrder [LinearOrder α] (p : α → Prop) : LinearOrder (Subtype p) :=
+instance instLinearOrder [LinearOrder α] (p : α → Prop) : LinearOrder (Subtype p) :=
   @LinearOrder.lift (Subtype p) _ _ ⟨fun x y ↦ ⟨max x y, max_rec' _ x.2 y.2⟩⟩
     ⟨fun x y ↦ ⟨min x y, min_rec' _ x.2 y.2⟩⟩ (fun (a : Subtype p) ↦ (a : α))
     Subtype.coe_injective (fun _ _ ↦ rfl) fun _ _ ↦
@@ -1432,7 +1432,7 @@ namespace PUnit
 
 variable (a b : PUnit.{u + 1})
 
-instance linearOrder : LinearOrder PUnit where
+instance instLinearOrder : LinearOrder PUnit where
   le  := fun _ _ ↦ True
   lt  := fun _ _ ↦ False
   max := fun _ _ ↦ unit

Mathlib/Order/BooleanAlgebra.lean

@@ -727,9 +727,9 @@ theorem compl_le_iff_compl_le : xᶜ ≤ y ↔ yᶜ ≤ x :=
 theorem sdiff_compl : x \ yᶜ = x ⊓ y := by rw [sdiff_eq, compl_compl]
 #align sdiff_compl sdiff_compl
 
-instance OrderDual.booleanAlgebra (α) [BooleanAlgebra α] : BooleanAlgebra αᵒᵈ where
-  __ := OrderDual.distribLattice α
-  __ := OrderDual.boundedOrder α
+instance OrderDual.instBooleanAlgebra (α) [BooleanAlgebra α] : BooleanAlgebra αᵒᵈ where
+  __ := OrderDual.instDistribLattice α
+  __ := OrderDual.instBoundedOrder α
   compl a := toDual (ofDual aᶜ)
   sdiff a b := toDual (ofDual b ⇨ ofDual a); himp := fun a b => toDual (ofDual b \ ofDual a)
   inf_compl_le_bot a := (@codisjoint_hnot_right _ _ (ofDual a)).top_le
@@ -789,38 +789,38 @@ lemma himp_ne_right : x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤ := himp_eq_left.
 
 end BooleanAlgebra
 
-instance Prop.booleanAlgebra : BooleanAlgebra Prop where
-  __ := Prop.heytingAlgebra
+instance Prop.instBooleanAlgebra : BooleanAlgebra Prop where
+  __ := Prop.instHeytingAlgebra
   __ := GeneralizedHeytingAlgebra.toDistribLattice
   compl := Not
   himp_eq p q := propext imp_iff_or_not
   inf_compl_le_bot p H := H.2 H.1
   top_le_sup_compl p _ := Classical.em p
-#align Prop.boolean_algebra Prop.booleanAlgebra
+#align Prop.boolean_algebra Prop.instBooleanAlgebra
 
-instance Prod.booleanAlgebra (α β) [BooleanAlgebra α] [BooleanAlgebra β] :
+instance Prod.instBooleanAlgebra (α β) [BooleanAlgebra α] [BooleanAlgebra β] :
     BooleanAlgebra (α × β) where
-  __ := Prod.heytingAlgebra
-  __ := Prod.distribLattice α β
+  __ := Prod.instHeytingAlgebra
+  __ := Prod.instDistribLattice α β
   himp_eq x y := by ext <;> simp [himp_eq]
   sdiff_eq x y := by ext <;> simp [sdiff_eq]
   inf_compl_le_bot x := by constructor <;> simp
   top_le_sup_compl x := by constructor <;> simp
 
-instance Pi.booleanAlgebra {ι : Type u} {α : ι → Type v} [∀ i, BooleanAlgebra (α i)] :
+instance Pi.instBooleanAlgebra {ι : Type u} {α : ι → Type v} [∀ i, BooleanAlgebra (α i)] :
     BooleanAlgebra (∀ i, α i) where
   __ := Pi.sdiff
-  __ := Pi.heytingAlgebra
-  __ := @Pi.distribLattice ι α _
+  __ := Pi.instHeytingAlgebra
+  __ := @Pi.instDistribLattice ι α _
   sdiff_eq _ _ := funext fun _ => sdiff_eq
   himp_eq _ _ := funext fun _ => himp_eq
   inf_compl_le_bot _ _ := BooleanAlgebra.inf_compl_le_bot _
   top_le_sup_compl _ _ := BooleanAlgebra.top_le_sup_compl _
-#align pi.boolean_algebra Pi.booleanAlgebra
+#align pi.boolean_algebra Pi.instBooleanAlgebra
 
 instance Bool.instBooleanAlgebra : BooleanAlgebra Bool where
   __ := Bool.linearOrder
-  __ := Bool.boundedOrder
+  __ := Bool.instBoundedOrder
   __ := Bool.instDistribLattice
   compl := not
   inf_compl_le_bot a := a.and_not_self.le
@@ -879,7 +879,7 @@ protected def Function.Injective.booleanAlgebra [Sup α] [Inf α] [Top α] [Bot
 
 end lift
 
-instance PUnit.booleanAlgebra : BooleanAlgebra PUnit := by
+instance PUnit.instBooleanAlgebra : BooleanAlgebra PUnit := by
   refine'
-  { PUnit.biheytingAlgebra with
+  { PUnit.instBiheytingAlgebra with
     .. } <;> (intros; trivial)

Mathlib/Order/BoundedOrder.lean

@@ -235,17 +235,17 @@ namespace OrderDual
 
 variable (α)
 
-instance top [Bot α] : Top αᵒᵈ :=
+instance instTop [Bot α] : Top αᵒᵈ :=
   ⟨(⊥ : α)⟩
 
-instance bot [Top α] : Bot αᵒᵈ :=
+instance instBot [Top α] : Bot αᵒᵈ :=
   ⟨(⊤ : α)⟩
 
-instance orderTop [LE α] [OrderBot α] : OrderTop αᵒᵈ where
+instance instOrderTop [LE α] [OrderBot α] : OrderTop αᵒᵈ where
   __ := inferInstanceAs (Top αᵒᵈ)
   le_top := @bot_le α _ _
 
-instance orderBot [LE α] [OrderTop α] : OrderBot αᵒᵈ where
+instance instOrderBot [LE α] [OrderTop α] : OrderBot αᵒᵈ where
   __ := inferInstanceAs (Bot αᵒᵈ)
   bot_le := @le_top α _ _
 
@@ -475,7 +475,7 @@ end SemilatticeInfBot
 class BoundedOrder (α : Type u) [LE α] extends OrderTop α, OrderBot α
 #align bounded_order BoundedOrder
 
-instance OrderDual.boundedOrder (α : Type u) [LE α] [BoundedOrder α] : BoundedOrder αᵒᵈ where
+instance OrderDual.instBoundedOrder (α : Type u) [LE α] [BoundedOrder α] : BoundedOrder αᵒᵈ where
   __ := inferInstanceAs (OrderTop αᵒᵈ)
   __ := inferInstanceAs (OrderBot αᵒᵈ)
 
@@ -618,13 +618,14 @@ theorem top_def [∀ i, Top (α' i)] : (⊤ : ∀ i, α' i) = fun _ => ⊤ :=
   rfl
 #align pi.top_def Pi.top_def
 
-instance orderTop [∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i) where
+instance instOrderTop [∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i) where
   le_top _ := fun _ => le_top
 
-instance orderBot [∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i) where
+instance instOrderBot [∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i) where
   bot_le _ := fun _ => bot_le
 
-instance boundedOrder [∀ i, LE (α' i)] [∀ i, BoundedOrder (α' i)] : BoundedOrder (∀ i, α' i) where
+instance instBoundedOrder [∀ i, LE (α' i)] [∀ i, BoundedOrder (α' i)] :
+    BoundedOrder (∀ i, α' i) where
   __ := inferInstanceAs (OrderTop (∀ i, α' i))
   __ := inferInstanceAs (OrderBot (∀ i, α' i))
 
@@ -777,26 +778,27 @@ namespace Prod
 
 variable (α β)
 
-instance top [Top α] [Top β] : Top (α × β) :=
+instance instTop [Top α] [Top β] : Top (α × β) :=
   ⟨⟨⊤, ⊤⟩⟩
 
-instance bot [Bot α] [Bot β] : Bot (α × β) :=
+instance instBot [Bot α] [Bot β] : Bot (α × β) :=
   ⟨⟨⊥, ⊥⟩⟩
 
 theorem fst_top [Top α] [Top β] : (⊤ : α × β).fst = ⊤ := rfl
 theorem snd_top [Top α] [Top β] : (⊤ : α × β).snd = ⊤ := rfl
 theorem fst_bot [Bot α] [Bot β] : (⊥ : α × β).fst = ⊥ := rfl
 theorem snd_bot [Bot α] [Bot β] : (⊥ : α × β).snd = ⊥ := rfl
 
-instance orderTop [LE α] [LE β] [OrderTop α] [OrderTop β] : OrderTop (α × β) where
+instance instOrderTop [LE α] [LE β] [OrderTop α] [OrderTop β] : OrderTop (α × β) where
   __ := inferInstanceAs (Top (α × β))
   le_top _ := ⟨le_top, le_top⟩
 
-instance orderBot [LE α] [LE β] [OrderBot α] [OrderBot β] : OrderBot (α × β) where
+instance instOrderBot [LE α] [LE β] [OrderBot α] [OrderBot β] : OrderBot (α × β) where
   __ := inferInstanceAs (Bot (α × β))
   bot_le _ := ⟨bot_le, bot_le⟩
 
-instance boundedOrder [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] : BoundedOrder (α × β) where
+instance instBoundedOrder [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] :
+    BoundedOrder (α × β) where
   __ := inferInstanceAs (OrderTop (α × β))
   __ := inferInstanceAs (OrderBot (α × β))
 
@@ -899,7 +901,7 @@ section Bool
 
 open Bool
 
-instance Bool.boundedOrder : BoundedOrder Bool where
+instance Bool.instBoundedOrder : BoundedOrder Bool where
   top := true
   le_top := Bool.le_true
   bot := false