fix(Algebra): some instance names (#6125)

Mathlib/Algebra/AddTorsor.lean

@@ -280,7 +280,7 @@ namespace Prod
 
 variable {G : Type _} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P']
 
-instance : AddTorsor (G × G') (P × P') where
+instance instAddTorsor : AddTorsor (G × G') (P × P') where
   vadd v p := (v.1 +ᵥ p.1, v.2 +ᵥ p.2)
   zero_vadd _ := Prod.ext (zero_vadd _ _) (zero_vadd _ _)
   add_vadd _ _ _ := Prod.ext (add_vadd _ _ _) (add_vadd _ _ _)

Mathlib/Algebra/Associated.lean

@@ -804,7 +804,7 @@ section CommMonoid
 
 variable [CommMonoid α]
 
-instance : Mul (Associates α) :=
+instance instMul : Mul (Associates α) :=
   ⟨fun a' b' =>
     (Quotient.liftOn₂ a' b' fun a b => ⟦a * b⟧) fun a₁ a₂ b₁ b₂ ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ =>
       Quotient.sound <| ⟨c₁ * c₂, by
@@ -816,7 +816,7 @@ theorem mk_mul_mk {x y : α} : Associates.mk x * Associates.mk y = Associates.mk
   rfl
 #align associates.mk_mul_mk Associates.mk_mul_mk
 
-instance : CommMonoid (Associates α) where
+instance instCommMonoid : CommMonoid (Associates α) where
   one := 1
   mul := (· * ·)
   mul_one a' := Quotient.inductionOn a' <| fun a => show ⟦a * 1⟧ = ⟦a⟧ by simp
@@ -827,7 +827,7 @@ instance : CommMonoid (Associates α) where
   mul_comm a' b' :=
     Quotient.inductionOn₂ a' b' <| fun a b => show ⟦a * b⟧ = ⟦b * a⟧ by rw [mul_comm]
 
-instance : Preorder (Associates α) where
+instance instPreorder : Preorder (Associates α) where
   le := Dvd.dvd
   le_refl := dvd_refl
   le_trans a b c := dvd_trans
@@ -913,7 +913,7 @@ theorem le_mul_right {a b : Associates α} : a ≤ a * b :=
 theorem le_mul_left {a b : Associates α} : a ≤ b * a := by rw [mul_comm]; exact le_mul_right
 #align associates.le_mul_left Associates.le_mul_left
 
-instance : OrderBot (Associates α) where
+instance instOrderBot : OrderBot (Associates α) where
   bot := 1
   bot_le _ := one_le
 
@@ -982,7 +982,7 @@ section CommMonoidWithZero
 
 variable [CommMonoidWithZero α]
 
-instance : CommMonoidWithZero (Associates α) where
+instance instCommMonoidWithZero : CommMonoidWithZero (Associates α) where
     zero_mul := by
       rintro ⟨a⟩
       show Associates.mk (0 * a) = Associates.mk 0
@@ -992,11 +992,11 @@ instance : CommMonoidWithZero (Associates α) where
       show Associates.mk (a * 0) = Associates.mk 0
       rw [mul_zero]
 
-instance : OrderTop (Associates α) where
+instance instOrderTop : OrderTop (Associates α) where
   top := 0
   le_top a := ⟨0, (mul_zero a).symm⟩
 
-instance : BoundedOrder (Associates α) where
+instance instBoundedOrder : BoundedOrder (Associates α) where
 
 instance [DecidableRel ((· ∣ ·) : α → α → Prop)] :
     DecidableRel ((· ∣ ·) : Associates α → Associates α → Prop) := fun a b =>
@@ -1083,15 +1083,15 @@ section CancelCommMonoidWithZero
 
 variable [CancelCommMonoidWithZero α]
 
-instance : PartialOrder (Associates α) where
+instance instPartialOrder : PartialOrder (Associates α) where
     le_antisymm := fun a' b' =>
       Quotient.inductionOn₂ a' b' fun _ _ hab hba =>
         Quot.sound <| associated_of_dvd_dvd (dvd_of_mk_le_mk hab) (dvd_of_mk_le_mk hba)
 
-instance : OrderedCommMonoid (Associates α) where
+instance instOrderedCommMonoid : OrderedCommMonoid (Associates α) where
     mul_le_mul_left := fun a _ ⟨d, hd⟩ c => hd.symm ▸ mul_assoc c a d ▸ le_mul_right
 
-instance : CancelCommMonoidWithZero (Associates α) :=
+instance instCancelCommMonoidWithZero : CancelCommMonoidWithZero (Associates α) :=
 { (by infer_instance : CommMonoidWithZero (Associates α)) with
   mul_left_cancel_of_ne_zero := by
     rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h

Mathlib/RingTheory/UniqueFactorizationDomain.lean

@@ -1556,7 +1556,7 @@ noncomputable instance : Inf (Associates α) :=
   ⟨fun a b => (a.factors ⊓ b.factors).prod⟩
 
 noncomputable instance : Lattice (Associates α) :=
-  { Associates.instPartialOrderAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero with
+  { Associates.instPartialOrder with
     sup := (· ⊔ ·)
     inf := (· ⊓ ·)
     sup_le := fun _ _ c hac hbc =>