feat: overlapping instances linter

Mathlib.lean

@@ -7094,6 +7094,7 @@ public import Mathlib.Tactic.Linter.Lint
 public import Mathlib.Tactic.Linter.MinImports
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
+public import Mathlib.Tactic.Linter.OverlappingInstances
 public import Mathlib.Tactic.Linter.PPRoundtrip
 public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.Style

Mathlib/Algebra/Algebra/Shrink.lean

@@ -26,7 +26,7 @@ instance [Semiring α] [Algebra R α] : Algebra R (Shrink.{v} α) := (equivShrin
 variable (R α) in
 /-- Shrinking `α` to a smaller universe preserves algebra structure. -/
 @[simps!]
-def algEquiv [Small.{v} α] [Semiring α] [Algebra R α] : Shrink.{v} α ≃ₐ[R] α :=
+def algEquiv [Semiring α] [Algebra R α] : Shrink.{v} α ≃ₐ[R] α :=
   (equivShrink α).symm.algEquiv _
 
 end Shrink

Mathlib/Algebra/Group/Action/Defs.lean

@@ -619,10 +619,10 @@ but here you can use the even stronger class `MulSemiringAction`, which captures
 how the action plays with both multiplication and addition. -/
 @[ext]
 class MulDistribMulAction (M N : Type*) [Monoid M] [Monoid N] extends MulAction M N where
-  /-- Distributivity of `•` across `*` -/
-  smul_mul : ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y
   /-- Multiplying `1` by a scalar gives `1` -/
   smul_one : ∀ r : M, r • (1 : N) = 1
+  /-- Distributivity of `•` across `*` -/
+  smul_mul : ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y
 
 export MulDistribMulAction (smul_one)
 

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -1119,7 +1119,8 @@ namespace Submonoid
 elements of `M`. -/
 @[to_additive (attr := simps!) /-- The additive equivalence between the type of additive units of
 `M` and the additive submonoid whose elements are the additive units of `M`. -/]
-noncomputable def unitsTypeEquivIsUnitSubmonoid [Monoid M] : Mˣ ≃* IsUnit.submonoid M where
+noncomputable def unitsTypeEquivIsUnitSubmonoid {M : Type*} [Monoid M] :
+    Mˣ ≃* IsUnit.submonoid M where
   toFun x := ⟨x, Units.isUnit x⟩
   invFun x := x.prop.unit
   left_inv _ := IsUnit.unit_of_val_units _

Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean

@@ -166,7 +166,7 @@ lemma Abelian.Ext.mapExactFunctor_add (f g : Ext.{w} X Y n) :
   aesop
 
 /-- Upgraded of `CategoryTheory.Abelian.Ext.mapExactFunctor` into an additive homomorphism. -/
-noncomputable def Functor.mapExtAddHom [HasExt.{w} C] [HasExt.{w'} D] (X Y : C) (n : ℕ) :
+noncomputable def Functor.mapExtAddHom (X Y : C) (n : ℕ) :
     Ext.{w} X Y n →+ Ext.{w'} (F.obj X) (F.obj Y) n where
   toFun e := e.mapExactFunctor F
   map_zero' := by simp
@@ -186,7 +186,7 @@ lemma Functor.mapExactFunctor_smul (r : R) (f : Ext.{w} X Y n) :
   aesop
 
 /-- Upgrade of `F.mapExtAddHom` assuming `F` is linear. -/
-noncomputable def Functor.mapExtLinearMap [HasExt.{w} C] [HasExt.{w'} D] (X Y : C) (n : ℕ) :
+noncomputable def Functor.mapExtLinearMap (X Y : C) (n : ℕ) :
     Ext.{w} X Y n →ₗ[R] Ext.{w'} (F.obj X) (F.obj Y) n where
   __ := F.mapExtAddHom X Y n
   map_smul' := by simp

Mathlib/Algebra/Homology/HomologySequence.lean

@@ -44,8 +44,7 @@ variable {C ι : Type*} [Category* C] [HasZeroMorphisms C] {c : ComplexShape ι}
   [K.HasHomology i] [K.HasHomology j] [L.HasHomology i] [L.HasHomology j]
 
 /-- The morphism `K.opcycles i ⟶ K.cycles j` that is induced by `K.d i j`. -/
-noncomputable def opcyclesToCycles [K.HasHomology i] [K.HasHomology j] :
-    K.opcycles i ⟶ K.cycles j :=
+noncomputable def opcyclesToCycles : K.opcycles i ⟶ K.cycles j :=
   K.liftCycles (K.fromOpcycles i j) _ rfl (by simp)
 
 @[reassoc (attr := simp)]

Mathlib/Algebra/Module/Equiv/Defs.lean

@@ -301,6 +301,7 @@ variable [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₄
 variable [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₄₃ σ₃₂ σ₄₂]
 variable (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃)
 
+set_option linter.overlappingInstances false in
 /-- Linear equivalences are transitive. -/
 -- Note: the `RingHomCompTriple σ₃₂ σ₂₁ σ₃₁` is unused, but is convenient to carry around
 -- implicitly for lemmas like `LinearEquiv.self_trans_symm`.

Mathlib/Algebra/Module/Lattice.lean

@@ -66,7 +66,7 @@ Note 2: In the case `R = ℤ` and `A = K` a field, there is also `IsZLattice` wh
 generated condition is replaced by having the discrete topology. -/
 class IsLattice (A : outParam Type*) [CommRing A] [Algebra R A]
     {V : Type*} [AddCommMonoid V] [Module R V] [Module A V] [IsScalarTower R A V]
-    [Algebra R A] [IsScalarTower R A V] (M : Submodule R V) : Prop where
+    [IsScalarTower R A V] (M : Submodule R V) : Prop where
   fg : M.FG
   span_eq_top : Submodule.span A (M : Set V) = ⊤
 

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -273,7 +273,7 @@ example : (smulZeroClass (A := ℕ) (R := R) (M := M)).toSMul = addCommMonoid.to
 
 -- Ensure that smul has good defeq properties
 private local instance {α} [Monoid M] [SMul M α] : SMul Mˣ α where smul m a := (m : M) • a
-example [Monoid A] [SMulZeroClass A R] (a : Units A) (x : R[M]) :
+example [Monoid A] (a : Units A) (x : R[M]) :
     a • x = (a : A) • x := by
   with_reducible_and_instances rfl
 end

Mathlib/Algebra/Order/Antidiag/Prod.lean

@@ -77,6 +77,7 @@ instance [AddMonoid A] : Subsingleton (HasAntidiagonal A) where
 
 -- The goal of this lemma is to allow to rewrite antidiagonal
 -- when the decidability instances obfuscate Lean
+set_option linter.overlappingInstances false in
 lemma hasAntidiagonal_congr (A : Type*) [AddMonoid A]
     [H1 : HasAntidiagonal A] [H2 : HasAntidiagonal A] :
     H1.antidiagonal = H2.antidiagonal := by congr!; subsingleton

Mathlib/Algebra/Order/Star/Basic.lean

@@ -446,7 +446,6 @@ lemma NonUnitalStarRingHom.map_le_map_of_map_star (f : R →⋆ₙ+* S) {x y : R
   all_goals aesop
 
 instance (priority := 100) StarRingHomClass.instOrderHomClass [FunLike F R S]
-    [StarOrderedRing R] [StarOrderedRing S]
     [NonUnitalRingHomClass F R S] [NonUnitalStarRingHomClass F R S] : OrderHomClass F R S where
   map_rel f := (f : R →⋆ₙ+* S).map_le_map_of_map_star
 

Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

@@ -655,7 +655,7 @@ variable [DecidableEq F] [DecidableEq K] [DecidableEq L]
 /-- The addition of two nonsingular points on a Weierstrass curve in affine coordinates.
 
 Given two nonsingular points `P` and `Q` in affine coordinates, use `P + Q` instead of `add P Q`. -/
-def add [DecidableEq F] : W.Point → W.Point → W.Point
+def add : W.Point → W.Point → W.Point
   | 0, P => P
   | P, 0 => P
   | some x₁ y₁ h₁, some x₂ y₂ h₂ =>

Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

@@ -30,7 +30,7 @@ open CategoryTheory Limits TopologicalSpace SheafOfModules Bicategory
 
 namespace AlgebraicGeometry.Scheme
 
-variable {X Y Z T : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
+variable {X Y Z T : Scheme.{u}}
 
 variable (X) in
 /-- The category of sheaves of modules over a scheme. -/
@@ -311,13 +311,12 @@ end Functorial
 
 noncomputable section Restriction
 
-variable [IsOpenImmersion f]
+variable (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g]
 
 /-- Restriction of an `𝒪ₓ`-module along an open immersion.
 This is isomorphic to the pullback functor (see `restrictFunctorIsoPullback`)
 but has better defeqs. -/
-def restrictFunctor :
-    Y.Modules ⥤ X.Modules :=
+def restrictFunctor : Y.Modules ⥤ X.Modules :=
   letI α : X.presheaf ⟶ f.opensFunctor.op ⋙ Y.presheaf := { app U := (f.appIso U.unop).inv }
   SheafOfModules.pushforward (F := f.opensFunctor)
     ⟨Functor.whiskerRight α (forget₂ CommRingCat RingCat)⟩
@@ -390,8 +389,7 @@ lemma restrictFunctorId_inv_app_app :
       M.presheaf.map (eqToHom (show 𝟙 X ''ᵁ U = U by simp)).op := rfl
 
 /-- Restriction along the composition is isomorphic to the composition of restrictions. -/
-def restrictFunctorComp [IsOpenImmersion f] [IsOpenImmersion g] :
-    restrictFunctor (f ≫ g) ≅ restrictFunctor g ⋙ restrictFunctor f :=
+def restrictFunctorComp : restrictFunctor (f ≫ g) ≅ restrictFunctor g ⋙ restrictFunctor f :=
   have : (f.opensFunctor ⋙ g.opensFunctor).IsContinuous
       (Opens.grothendieckTopology X) (Opens.grothendieckTopology Z) :=
     Functor.isContinuous_comp _ _ _ (Opens.grothendieckTopology _) _
@@ -400,11 +398,11 @@ def restrictFunctorComp [IsOpenImmersion f] [IsOpenImmersion g] :
     (SheafOfModules.pushforwardComp _ _).symm
 
 @[simp]
-lemma restrictFunctorComp_hom_app_app [IsOpenImmersion g] (M : Z.Modules) :
+lemma restrictFunctorComp_hom_app_app (M : Z.Modules) :
     ((restrictFunctorComp f g).hom.app M).app U = M.presheaf.map (eqToHom (by simp)).op := rfl
 
 @[simp]
-lemma restrictFunctorComp_inv_app_app [IsOpenImmersion g] (M : Z.Modules) :
+lemma restrictFunctorComp_inv_app_app (M : Z.Modules) :
     ((restrictFunctorComp f g).inv.app M).app U = M.presheaf.map (eqToHom (by simp)).op := rfl
 
 /-- Restriction along equal morphisms are isomorphic. -/
@@ -424,7 +422,7 @@ lemma restrictFunctorCongr_inv_app_app {f g : X ⟶ Y} (hf : f = g) [IsOpenImmer
     ((restrictFunctorCongr hf).inv.app M).app U = M.presheaf.map (eqToHom (by simp [hf])).op := rfl
 
 /-- Restriction along open immersions commutes with taking stalks. -/
-def restrictStalkNatIso (f : X ⟶ Y) [IsOpenImmersion f] (x : X) :
+def restrictStalkNatIso (x : X) :
     restrictFunctor f ⋙ toPresheaf _ ⋙ TopCat.Presheaf.stalkFunctor _ x ≅
     toPresheaf _ ⋙ TopCat.Presheaf.stalkFunctor _ (f x) :=
   haveI := Functor.initial_of_adjunction (f.isOpenEmbedding.adjunctionNhds x)
@@ -433,8 +431,7 @@ def restrictStalkNatIso (f : X ⟶ Y) [IsOpenImmersion f] (x : X) :
       (Functor.Final.colimIso (f.isOpenEmbedding.functorNhds x).op)
 
 @[simp]
-lemma germ_restrictStalkNatIso_hom_app (f : X ⟶ Y) [IsOpenImmersion f]
-    (x : X) (M : Y.Modules) (hxU : x ∈ U) :
+lemma germ_restrictStalkNatIso_hom_app (x : X) (M : Y.Modules) (hxU : x ∈ U) :
     ((restrictFunctor f).obj M).presheaf.germ U _ hxU ≫
       (restrictStalkNatIso f x).hom.app M = M.presheaf.germ _ _ (by simpa) :=
   haveI := Functor.initial_of_adjunction (f.isOpenEmbedding.adjunctionNhds x)
@@ -444,8 +441,7 @@ lemma germ_restrictStalkNatIso_hom_app (f : X ⟶ Y) [IsOpenImmersion f]
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
-lemma germ_restrictStalkNatIso_inv_app (f : X ⟶ Y) [IsOpenImmersion f]
-    (x : X) (M : Y.Modules) (hxU : x ∈ U) :
+lemma germ_restrictStalkNatIso_inv_app (x : X) (M : Y.Modules) (hxU : x ∈ U) :
     M.presheaf.germ _ _ (by simpa) ≫ (restrictStalkNatIso f x).inv.app M =
       ((restrictFunctor f).obj M).presheaf.germ U _ hxU := by
   rw [← germ_restrictStalkNatIso_hom_app f x M hxU, Category.assoc, ← NatTrans.comp_app,

Mathlib/AlgebraicTopology/ModelCategory/IsCofibrant.lean

@@ -52,8 +52,7 @@ lemma isCofibrant_of_cofibration [(cofibrations C).IsStableUnderComposition]
 
 section
 
-variable (X Y : C) [(cofibrations C).IsStableUnderCobaseChange] [HasInitial C]
-  [HasBinaryCoproduct X Y]
+variable (X Y : C) [(cofibrations C).IsStableUnderCobaseChange] [HasBinaryCoproduct X Y]
 
 instance [hY : IsCofibrant Y] :
     Cofibration (coprod.inl : X ⟶ X ⨿ Y) := by
@@ -63,8 +62,7 @@ instance [hY : IsCofibrant Y] :
     ((IsPushout.of_isColimit_binaryCofan_of_isInitial
     (colimit.isColimit (pair X Y)) initialIsInitial).flip) hY
 
-instance [HasInitial C] [HasBinaryCoproduct X Y] [hX : IsCofibrant X] :
-    Cofibration (coprod.inr : Y ⟶ X ⨿ Y) := by
+instance [hX : IsCofibrant X] : Cofibration (coprod.inr : Y ⟶ X ⨿ Y) := by
   rw [isCofibrant_iff] at hX
   rw [cofibration_iff] at hX ⊢
   exact MorphismProperty.of_isPushout
@@ -102,7 +100,7 @@ lemma isFibrant_of_fibration [(fibrations C).IsStableUnderComposition]
 
 section
 
-variable (X Y : C) [(fibrations C).IsStableUnderBaseChange] [HasTerminal C]
+variable (X Y : C) [(fibrations C).IsStableUnderBaseChange]
   [HasBinaryProduct X Y]
 
 instance [hY : IsFibrant Y] :
@@ -113,8 +111,7 @@ instance [hY : IsFibrant Y] :
     (IsPullback.of_isLimit_binaryFan_of_isTerminal
       (limit.isLimit (pair X Y)) terminalIsTerminal).flip hY
 
-instance [HasTerminal C] [HasBinaryProduct X Y] [hX : IsFibrant X] :
-    Fibration (prod.snd : X ⨯ Y ⟶ Y) := by
+instance [hX : IsFibrant X] : Fibration (prod.snd : X ⨯ Y ⟶ Y) := by
   rw [isFibrant_iff] at hX
   rw [fibration_iff] at hX ⊢
   exact MorphismProperty.of_isPullback

Mathlib/Analysis/Distribution/DerivNotation.lean

@@ -340,7 +340,6 @@ section ContinuousLinearMap
 section definition
 
 variable [CommRing R]
-  [FiniteDimensional ℝ E]
   [Module R V₁] [Module R V₂] [Module R V₃]
   [TopologicalSpace V₁] [TopologicalSpace V₂] [TopologicalSpace V₃] [IsTopologicalAddGroup V₃]
   [LineDerivAdd E V₁ V₂] [LineDerivSMul R E V₁ V₂] [ContinuousLineDeriv E V₁ V₂]

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

@@ -39,7 +39,7 @@ and outputs a set of orthogonal vectors which have the same span.
 open Finset Submodule Module
 
 variable (𝕜 : Type*) {E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
-variable {ι : Type*} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι]
+variable {ι : Type*} [LinearOrder ι] [LocallyFiniteOrderBot ι]
 
 attribute [local instance] IsWellOrder.toHasWellFounded
 
@@ -54,6 +54,8 @@ noncomputable def gramSchmidt [WellFoundedLT ι] (f : ι → E) (n : ι) : E :=
 termination_by n
 decreasing_by exact mem_Iio.1 i.2
 
+variable [WellFoundedLT ι]
+
 /-- This lemma uses `∑ i in` instead of `∑ i :`. -/
 theorem gramSchmidt_def (f : ι → E) (n : ι) :
     gramSchmidt 𝕜 f n = f n - ∑ i ∈ Iio n, (𝕜 ∙ gramSchmidt 𝕜 f i).starProjection (f n) := by

Mathlib/Analysis/InnerProductSpace/Harmonic/HarmonicContOnCl.lean

@@ -51,7 +51,7 @@ theorem harmonicContOnCl_const {c : F} : HarmonicContOnCl (fun _ : E ↦ c) s :=
 
 namespace HarmonicContOnCl
 
-theorem continuousOn_ball [NormedSpace ℝ E] {x : E} {r : ℝ} (h : HarmonicContOnCl f (ball x r)) :
+theorem continuousOn_ball {x : E} {r : ℝ} (h : HarmonicContOnCl f (ball x r)) :
     ContinuousOn f (closedBall x r) := by
   rcases eq_or_ne r 0 with (rfl | hr)
   · rw [closedBall_zero]

Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean

@@ -200,8 +200,8 @@ precisely the units. This allows for the application of this isomorphism in broa
 to the quotient of a complex Banach algebra by a maximal ideal. In the case when `A` is actually a
 `NormedDivisionRing`, one may fill in the argument `hA` with the lemma `isUnit_iff_ne_zero`. -/
 @[simps]
-noncomputable def _root_.NormedRing.algEquivComplexOfComplete (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0)
-    [CompleteSpace A] : ℂ ≃ₐ[ℂ] A :=
+noncomputable def _root_.NormedRing.algEquivComplexOfComplete (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) :
+    ℂ ≃ₐ[ℂ] A :=
   let nt : Nontrivial A := ⟨⟨1, 0, hA.mp ⟨⟨1, 1, mul_one _, mul_one _⟩, rfl⟩⟩⟩
   { Algebra.ofId ℂ A with
     toFun := algebraMap ℂ A

Mathlib/Analysis/Normed/Ring/WithAbs.lean

@@ -253,8 +253,7 @@ variable [Semiring T] [Module R T] (v : AbsoluteValue T S)
 variable (R) in
 /-- The canonical `R`-linear isomorphism between `WithAbs v` and `T`, when
 `v : AbsoluteValue T S`. -/
-def linearEquiv [Semiring T] [Module R T] (v : AbsoluteValue T S) :
-    WithAbs v ≃ₗ[R] T := (equiv v).linearEquiv R
+def linearEquiv : WithAbs v ≃ₗ[R] T := (equiv v).linearEquiv R
 
 variable {v}
 

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

@@ -880,7 +880,7 @@ def normedField : NormedField L :=
 
 /-- `L` with the spectral norm is a `NontriviallyNormedField`. -/
 @[implicit_reducible]
-def nontriviallyNormedField [CompleteSpace K] : NontriviallyNormedField L where
+def nontriviallyNormedField : NontriviallyNormedField L where
   __ := spectralNorm.normedField K L
   non_trivial :=
     let ⟨x, hx⟩ := NontriviallyNormedField.non_trivial (α := K)

Mathlib/CategoryTheory/Adhesive/Subobject.lean

@@ -41,7 +41,7 @@ noncomputable def isColimitBinaryCofan (a b : Subobject X) :
       (by ext; simp [pullback.condition])) (by cat_disch)).hom)
     (by intros; rfl) (by intros; rfl) (by intros; rfl)
 
-instance [Adhesive C] {X : C} : HasBinaryCoproducts (Subobject X) where
+instance : HasBinaryCoproducts (Subobject X) where
   has_colimit F := by
     have : HasColimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
       ⟨⟨⟨_, isColimitBinaryCofan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩

Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean

@@ -188,7 +188,7 @@ lemma universal_property {R' : 𝒮} {a' : 𝒳} (g : R' ⟶ R) (f' : R' ⟶ S)
   have : p.IsHomLift (g ≫ f) φ' := (hf' ▸ inferInstance)
   apply IsStronglyCartesian.universal_property' f
 
-instance isCartesian_of_isStronglyCartesian [p.IsStronglyCartesian f φ] : p.IsCartesian f φ where
+instance isCartesian_of_isStronglyCartesian : p.IsCartesian f φ where
   universal_property := fun φ' => universal_property p f φ (𝟙 R) f (by simp) φ'
 
 section

Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean

@@ -177,8 +177,7 @@ lemma universal_property {S' : 𝒮} {b' : 𝒳} (g : S ⟶ S') (f' : R ⟶ S')
   have : p.IsHomLift (f ≫ g) φ' := (hf' ▸ inferInstance)
   apply IsStronglyCocartesian.universal_property' f
 
-instance isCocartesian_of_isStronglyCocartesian [p.IsStronglyCocartesian f φ] :
-    p.IsCocartesian f φ where
+instance isCocartesian_of_isStronglyCocartesian : p.IsCocartesian f φ where
   universal_property := fun φ' => universal_property p f φ (𝟙 S) f (comp_id f).symm φ'
 
 section

Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

@@ -805,7 +805,7 @@ open Limits
 
 variable {C : Type*} [Category* C] [HasZeroMorphisms C] (P : ObjectProperty C)
 
-instance [HasZeroMorphisms C] : HasZeroMorphisms P.FullSubcategory where
+instance : HasZeroMorphisms P.FullSubcategory where
   -- Note: Add zero field explicitly for a better transparency of definitional properties
   zero _ _ := { zero := P.homMk 0 }
   __ := P.fullyFaithfulι.hasZeroMorphisms

Mathlib/CategoryTheory/Localization/Predicate.lean

@@ -232,6 +232,7 @@ the composition with a localization functor `L : C ⥤ D` with respect to
 def functorEquivalence : D ⥤ E ≌ W.FunctorsInverting E :=
   (whiskeringLeftFunctor L W E).asEquivalence
 
+set_option linter.overlappingInstances false in
 /-- The functor `(D ⥤ E) ⥤ (C ⥤ E)` given by the composition with a localization
 functor `L : C ⥤ D` with respect to `W : MorphismProperty C`. -/
 @[nolint unusedArguments]

Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean

@@ -98,6 +98,7 @@ def powZero [BraidedCategory C] {I : C} (t : IsInitial I) [MonoidalClosed C] : I
     rw [← curry_natural_left, curry_eq_iff, ← cancel_epi (mulZero t).inv]
     apply t.hom_ext
 
+set_option linter.overlappingInstances false in
 set_option backward.isDefEq.respectTransparency false in
 -- TODO: Generalise the below to its commuted variants.
 -- TODO: Define a distributive category, so that zero_mul and friends can be derived from this.

Mathlib/CategoryTheory/Monoidal/Functor.lean

@@ -1220,7 +1220,7 @@ instance isMonoidal_refl : (Equivalence.refl (C := C)).IsMonoidal :=
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The inverse of a monoidal category equivalence is also a monoidal category equivalence. -/
-instance isMonoidal_symm [e.IsMonoidal] : e.symm.IsMonoidal where
+instance isMonoidal_symm : e.symm.IsMonoidal where
   leftAdjoint_ε := by
     simp only [toAdjunction]
     dsimp [symm]

Mathlib/CategoryTheory/Monoidal/Grp_.lean

@@ -351,8 +351,7 @@ lemma ext {X : C} (h₁ h₂ : GrpObj X) (H : h₁.toMonObj = h₂.toMonObj) : h
 set_option backward.isDefEq.respectTransparency false in
 /-- A monoid object with invertible homs is a group object. -/
 @[implicit_reducible]
-def ofInvertible (G : C) [CartesianMonoidalCategory C] [MonObj G]
-    (h : ∀ X (f : X ⟶ G), Invertible f) : GrpObj G where
+def ofInvertible (G : C) [MonObj G] (h : ∀ X (f : X ⟶ G), Invertible f) : GrpObj G where
   inv := Yoneda.fullyFaithful.preimage
     ⟨fun X ↦ TypeCat.ofHom (fun f ↦ (h X.unop f).invOf), fun X Y f ↦ by
       ext g

Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

@@ -151,7 +151,7 @@ omit [Preadditive C] [Preadditive D] in
 instance : (Functor.whiskeringRight C D E).Additive where
 
 omit [Preadditive C] [Preadditive D] in
-instance (F : C ⥤ D) [Preadditive E] : ((Functor.whiskeringLeft C D E).obj F).Additive where
+instance (F : C ⥤ D) : ((Functor.whiskeringLeft C D E).obj F).Additive where
 
 omit [Preadditive D] in
 instance {E' : Type*} [Category* E'] [Preadditive E'] (G : C ⥤ D ⥤ E) (F : E ⥤ E')
@@ -161,7 +161,7 @@ instance {E' : Type*} [Category* E'] [Preadditive E'] (G : C ⥤ D ⥤ E) (F : E
 
 set_option backward.isDefEq.respectTransparency false in
 universe w in
-instance [HasCoproducts.{w} C] [Preadditive C] : (sigmaConst.{w} (C := C)).Additive where
+instance [HasCoproducts.{w} C] : (sigmaConst.{w} (C := C)).Additive where
 
 end
 

Mathlib/CategoryTheory/Shift/Adjunction.lean

@@ -248,8 +248,6 @@ lemma mk' (_ : NatTrans.CommShift adj.unit A) :
     refine (compatibilityCounit_of_compatibilityUnit adj _ _ (fun X ↦ ?_) _).symm
     simpa [Functor.commShiftIso_comp_hom_app] using NatTrans.shift_app_comm adj.unit a X⟩
 
-variable [adj.CommShift A]
-
 /-- The identity adjunction is compatible with the trivial `CommShift` structure on the
 identity functor.
 -/