chore: remove duplicated namespaces from instances (#10899)

Mathlib/Algebra/Algebra/Opposite.lean

@@ -37,7 +37,7 @@ variable [IsScalarTower R S A]
 
 namespace MulOpposite
 
-instance MulOpposite.instAlgebra : Algebra R Aᵐᵒᵖ where
+instance instAlgebra : Algebra R Aᵐᵒᵖ where
   toRingHom := (algebraMap R A).toOpposite fun x y => Algebra.commutes _ _
   smul_def' c x := unop_injective <| by
     simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul, op_mul,

Mathlib/Analysis/NormedSpace/LinearIsometry.lean

@@ -129,7 +129,7 @@ theorem diam_range [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
   (SemilinearIsometryClass.isometry f).diam_range
 #align semilinear_isometry_class.diam_range SemilinearIsometryClass.diam_range
 
-instance (priority := 100) SemilinearIsometryClass.toContinuousSemilinearMapClass
+instance (priority := 100) toContinuousSemilinearMapClass
     [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] : ContinuousSemilinearMapClass 𝓕 σ₁₂ E E₂ where
   map_continuous := SemilinearIsometryClass.continuous
 
@@ -533,7 +533,7 @@ namespace SemilinearIsometryEquivClass
 variable (𝓕)
 
 -- `σ₂₁` becomes a metavariable, but it's OK since it's an outparam
-instance (priority := 100) SemilinearIsometryEquivClass.toSemilinearIsometryClass [EquivLike 𝓕 E E₂]
+instance (priority := 100) toSemilinearIsometryClass [EquivLike 𝓕 E E₂]
     [s : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂] : SemilinearIsometryClass 𝓕 σ₁₂ E E₂ :=
   { s with }
 

Mathlib/CategoryTheory/Category/Preorder.lean

@@ -51,7 +51,7 @@ instance (priority := 100) smallCategory (α : Type u) [Preorder α] : SmallCate
 #align preorder.small_category Preorder.smallCategory
 
 -- porting note: added to ease the port of `CategoryTheory.Subobject.Basic`
-instance Preorder.subsingleton_hom {α : Type u} [Preorder α] (U V : α) :
+instance subsingleton_hom {α : Type u} [Preorder α] (U V : α) :
   Subsingleton (U ⟶ V) := ⟨fun _ _ => ULift.ext _ _ (Subsingleton.elim _ _ )⟩
 
 end Preorder

Mathlib/CategoryTheory/Monad/Kleisli.lean

@@ -44,7 +44,7 @@ instance [Inhabited C] (T : Monad C) : Inhabited (Kleisli T) :=
 
 /-- The Kleisli category on a monad `T`.
     cf Definition 5.2.9 in [Riehl][riehl2017]. -/
-instance Kleisli.category : Category (Kleisli T) where
+instance category : Category (Kleisli T) where
   Hom := fun X Y : C => X ⟶ (T : C ⥤ C).obj Y
   id X := T.η.app X
   comp {X} {Y} {Z} f g := f ≫ (T : C ⥤ C).map g ≫ T.μ.app Z
@@ -55,7 +55,7 @@ instance Kleisli.category : Category (Kleisli T) where
   assoc f g h := by
     simp only [Functor.map_comp, Category.assoc, Monad.assoc]
     erw [T.μ.naturality_assoc]
-#align category_theory.kleisli.kleisli.category CategoryTheory.Kleisli.Kleisli.category
+#align category_theory.kleisli.kleisli.category CategoryTheory.Kleisli.category
 
 namespace Adjunction
 
@@ -122,7 +122,7 @@ instance [Inhabited C] (U : Comonad C) : Inhabited (Cokleisli U) :=
   ⟨(default : C)⟩
 
 /-- The co-Kleisli category on a comonad `U`.-/
-instance Cokleisli.category : Category (Cokleisli U) where
+instance category : Category (Cokleisli U) where
   Hom := fun X Y : C => (U : C ⥤ C).obj X ⟶ Y
   id X := U.ε.app X
   comp {X} {Y} {Z} f g := U.δ.app X ≫ (U : C ⥤ C).map f ≫ g
@@ -134,7 +134,7 @@ instance Cokleisli.category : Category (Cokleisli U) where
     -- Porting note: something was broken here and was easier just to redo from scratch
     simp only [Functor.map_comp, ← Category.assoc, eq_whisker]
     simp only [Category.assoc, U.δ.naturality, Functor.comp_map, U.coassoc_assoc]
-#align category_theory.cokleisli.cokleisli.category CategoryTheory.Cokleisli.Cokleisli.category
+#align category_theory.cokleisli.cokleisli.category CategoryTheory.Cokleisli.category
 
 namespace Adjunction
 

Mathlib/Control/LawfulFix.lean

@@ -282,13 +282,13 @@ theorem uncurry_curry_continuous :
 
 end Curry
 
-instance Pi.lawfulFix' [LawfulFix <| (x : Sigma β) → γ x.1 x.2] :
+instance lawfulFix' [LawfulFix <| (x : Sigma β) → γ x.1 x.2] :
     LawfulFix ((x y : _) → γ x y) where
   fix_eq {_f} hc := by
     dsimp [fix]
     conv =>
       lhs
       erw [LawfulFix.fix_eq (uncurry_curry_continuous hc)]
-#align pi.pi.lawful_fix' Pi.Pi.lawfulFix'
+#align pi.pi.lawful_fix' Pi.lawfulFix'
 
 end Pi

Mathlib/Data/Complex/Basic.lean

@@ -416,7 +416,7 @@ instance addCommGroup : AddCommGroup ℂ :=
     add_left_neg := by intros; ext <;> simp }
 
 
-instance Complex.addGroupWithOne : AddGroupWithOne ℂ :=
+instance addGroupWithOne : AddGroupWithOne ℂ :=
   { Complex.addCommGroup with
     natCast := fun n => ⟨n, 0⟩
     natCast_zero := by
@@ -436,7 +436,7 @@ instance Complex.addGroupWithOne : AddGroupWithOne ℂ :=
 
 -- Porting note: proof needed modifications and rewritten fields
 instance commRing : CommRing ℂ :=
-  { Complex.addGroupWithOne with
+  { addGroupWithOne with
     mul := (· * ·)
     npow := @npowRec _ ⟨(1 : ℂ)⟩ ⟨(· * ·)⟩
     add_comm := by intros; ext <;> simp [add_comm]

Mathlib/Logic/Function/FromTypes.lean

@@ -78,7 +78,7 @@ theorem const_succ {n} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ) :
 theorem const_succ_apply {n} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ)
     (x : p 0) : const p t x = const (vecTail p) t := rfl
 
-instance FromTypes.inhabited {n} {p : Fin n → Type u} {τ} [Inhabited τ] :
+instance inhabited {n} {p : Fin n → Type u} {τ} [Inhabited τ] :
     Inhabited (FromTypes p τ) := ⟨const p default⟩
 
 end FromTypes

Mathlib/Logic/Function/OfArity.lean

@@ -60,9 +60,9 @@ theorem const_succ_apply (α : Type u) {β : Type u} (b : β) (n : ℕ) (x : α)
     const α b n.succ x = const _ b n := FromTypes.const_succ_apply _ b x
 #align arity.const_succ_apply Function.OfArity.const_succ_apply
 
-instance OfArity.inhabited {α β n} [Inhabited β] : Inhabited (OfArity α β n) :=
+instance inhabited {α β n} [Inhabited β] : Inhabited (OfArity α β n) :=
   inferInstanceAs (Inhabited (FromTypes (fun _ => α) β))
-#align arity.arity.inhabited Function.OfArity.OfArity.inhabited
+#align arity.arity.inhabited Function.OfArity.inhabited
 
 end OfArity
 

Mathlib/MeasureTheory/OuterMeasure/Basic.lean

@@ -365,10 +365,10 @@ instance instPartialOrder : PartialOrder (OuterMeasure α) where
   le_antisymm a b hab hba := ext fun s => le_antisymm (hab s) (hba s)
 #align measure_theory.outer_measure.outer_measure.partial_order MeasureTheory.OuterMeasure.instPartialOrder
 
-instance OuterMeasure.orderBot : OrderBot (OuterMeasure α) :=
+instance orderBot : OrderBot (OuterMeasure α) :=
   { bot := 0,
     bot_le := fun a s => by simp only [coe_zero, Pi.zero_apply, coe_bot, zero_le] }
-#align measure_theory.outer_measure.outer_measure.order_bot MeasureTheory.OuterMeasure.OuterMeasure.orderBot
+#align measure_theory.outer_measure.outer_measure.order_bot MeasureTheory.OuterMeasure.orderBot
 
 theorem univ_eq_zero_iff (m : OuterMeasure α) : m univ = 0 ↔ m = 0 :=
   ⟨fun h => bot_unique fun s => (m.mono' <| subset_univ s).trans_eq h, fun h => h.symm ▸ rfl⟩

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

@@ -98,17 +98,15 @@ namespace ContinuousMonoidHom
 variable {A B C D E}
 
 @[to_additive]
-instance ContinuousMonoidHom.funLike :
-    FunLike (ContinuousMonoidHom A B) A B where
+instance funLike : FunLike (ContinuousMonoidHom A B) A B where
   coe f := f.toFun
   coe_injective' f g h := by
     obtain ⟨⟨⟨ _ , _ ⟩, _⟩, _⟩ := f
     obtain ⟨⟨⟨ _ , _ ⟩, _⟩, _⟩ := g
     congr
 
 @[to_additive]
-instance ContinuousMonoidHom.ContinuousMonoidHomClass :
-    ContinuousMonoidHomClass (ContinuousMonoidHom A B) A B where
+instance ContinuousMonoidHomClass : ContinuousMonoidHomClass (ContinuousMonoidHom A B) A B where
   map_mul f := f.map_mul'
   map_one f := f.map_one'
   map_continuous f := f.continuous_toFun