diff --git a/Mathlib.lean b/Mathlib.lean
index 14ee8ec6788e43..4b96ae3e05a261 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -7239,6 +7239,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
diff --git a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean
index 6d16674327f61a..5c8c249872fc8f 100644
--- a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean
+++ b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean
@@ -376,6 +376,7 @@ protected lemma nontrivial {F : J ⥤ CommRingCat.{v}} [IsFilteredOrEmpty J]
     (Types.FilteredColimit.isColimit_eq_iff' (isColimitOfPreserves (forget _) hc) _ _).mp h
   exact zero_ne_one (((F.map f).hom.map_zero.symm.trans e).trans (F.map f).hom.map_one)
 
+set_option linter.overlappingInstances false in
 omit [IsFiltered J] in
 instance {F : J ⥤ CommRingCat.{v}} [IsFilteredOrEmpty J]
     [HasColimit F] [∀ i, Nontrivial (F.obj i)] : Nontrivial ↑(Limits.colimit F) :=
diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 5c33f2bbbe1238..bab0b703504194 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -833,8 +833,8 @@ end NonUnitalStarRing
 namespace Algebra
 
 variable [CommSemiring R]
-variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
-variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
+variable [∀ i, Semiring (G i)] [∀ i, Algebra R (G i)]
+variable [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 variable [Nonempty ι]
 
 variable (G f) in
diff --git a/Mathlib/Algebra/Homology/HomotopyFiber.lean b/Mathlib/Algebra/Homology/HomotopyFiber.lean
index e5efe421ca2e24..bcb49936da5332 100644
--- a/Mathlib/Algebra/Homology/HomotopyFiber.lean
+++ b/Mathlib/Algebra/Homology/HomotopyFiber.lean
@@ -42,7 +42,7 @@ class HasHomotopyFiber (φ : F ⟶ G) : Prop where
 instance [HasBinaryBiproducts C] : HasHomotopyFiber φ where
   hasBinaryBiproduct _ _ _ := inferInstance
 
-variable [HasHomotopyFiber φ] [DecidableRel c.Rel]
+variable [HasHomotopyFiber φ]
 
 instance : HasHomotopyCofiber ((opFunctor C c).map φ.op) where
   hasBinaryBiproduct i j hij := by
diff --git a/Mathlib/Algebra/Module/DedekindDomain.lean b/Mathlib/Algebra/Module/DedekindDomain.lean
index 8185c795c70e12..fc699e5eb4a0f5 100644
--- a/Mathlib/Algebra/Module/DedekindDomain.lean
+++ b/Mathlib/Algebra/Module/DedekindDomain.lean
@@ -22,14 +22,12 @@ public section
 
 universe u v
 
-variable {R : Type u} [CommRing R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module R M]
+variable {R : Type u} [CommRing R] [IsDedekindDomain R] {M : Type v} [AddCommGroup M] [Module R M]
 
 open scoped DirectSum
 
 namespace Submodule
 
-variable [IsDedekindDomain R]
-
 open UniqueFactorizationMonoid
 
 /-- Over a Dedekind domain, an `I`-torsion module is the internal direct sum of its `p i ^ e i`-
diff --git a/Mathlib/Algebra/Module/Equiv/Defs.lean b/Mathlib/Algebra/Module/Equiv/Defs.lean
index d99677823a8bf6..5d4616cf15966c 100644
--- a/Mathlib/Algebra/Module/Equiv/Defs.lean
+++ b/Mathlib/Algebra/Module/Equiv/Defs.lean
@@ -296,6 +296,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`.
diff --git a/Mathlib/Algebra/Module/GradedModule.lean b/Mathlib/Algebra/Module/GradedModule.lean
index 019d32ab4861e9..b5cd34d70ed2ac 100644
--- a/Mathlib/Algebra/Module/GradedModule.lean
+++ b/Mathlib/Algebra/Module/GradedModule.lean
@@ -191,20 +191,21 @@ end SetLike
 namespace GradedModule
 
 variable [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A]
-  [AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSMul 𝓐 𝓜]
+  [AddSubmonoidClass σ M] [SetLike.GradedSMul 𝓐 𝓜]
+  [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐]
 
 /-- The smul multiplication of `A` on `⨁ i, 𝓜 i` from `(⨁ i, 𝓐 i) →+ (⨁ i, 𝓜 i) →+ ⨁ i, 𝓜 i`
 turns `⨁ i, 𝓜 i` into an `A`-module
 -/
 @[implicit_reducible]
-def isModule [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] : Module A (⨁ i, 𝓜 i) :=
+def isModule : Module A (⨁ i, 𝓜 i) :=
   { Module.compHom _ (DirectSum.decomposeRingEquiv 𝓐 : A ≃+* ⨁ i, 𝓐 i).toRingHom with
     smul := fun a b => DirectSum.decompose 𝓐 a • b }
 
 /-- `⨁ i, 𝓜 i` and `M` are isomorphic as `A`-modules.
 "The internal version" and "the external version" are isomorphism as `A`-modules.
 -/
-def linearEquiv [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] [DirectSum.Decomposition 𝓜] :
+def linearEquiv [DirectSum.Decomposition 𝓜] :
     @LinearEquiv A A _ _ (RingHom.id A) (RingHom.id A) _ _ M (⨁ i, 𝓜 i) _
     _ _ (by letI := isModule 𝓐 𝓜; infer_instance) := by
   letI h := isModule 𝓐 𝓜
diff --git a/Mathlib/Algebra/Order/Antidiag/Prod.lean b/Mathlib/Algebra/Order/Antidiag/Prod.lean
index 9217a07c264188..e53c0810966ba6 100644
--- a/Mathlib/Algebra/Order/Antidiag/Prod.lean
+++ b/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
diff --git a/Mathlib/Algebra/Order/Invertible.lean b/Mathlib/Algebra/Order/Invertible.lean
index ccdf4d4e138f23..983786f2539f8e 100644
--- a/Mathlib/Algebra/Order/Invertible.lean
+++ b/Mathlib/Algebra/Order/Invertible.lean
@@ -41,6 +41,5 @@ theorem invOf_le_one [Invertible a] (h : 1 ≤ a) : ⅟a ≤ 1 :=
 theorem invOf_lt_one [Invertible a] (h : 1 < a) : ⅟a < 1 :=
   mul_invOf_self a ▸ lt_mul_of_one_lt_left (invOf_pos.2 <| one_pos.trans h) h
 
-theorem pos_invOf_of_invertible_cast [Nontrivial R] (n : ℕ)
-    [Invertible (n : R)] : 0 < ⅟(n : R) :=
+theorem pos_invOf_of_invertible_cast (n : ℕ) [Invertible (n : R)] : 0 < ⅟(n : R) :=
   invOf_pos.2 <| Nat.cast_pos.2 <| pos_of_invertible_cast (R := R) n
diff --git a/Mathlib/Algebra/Polynomial/Div.lean b/Mathlib/Algebra/Polynomial/Div.lean
index 47a937313aff9c..38002ad6857ee4 100644
--- a/Mathlib/Algebra/Polynomial/Div.lean
+++ b/Mathlib/Algebra/Polynomial/Div.lean
@@ -789,7 +789,7 @@ lemma _root_.Irreducible.isRoot_eq_bot_of_natDegree_ne_one
     (hi : Irreducible p) (hdeg : p.natDegree ≠ 1) : p.IsRoot = ⊥ :=
   le_bot_iff.mp fun _ ↦ hi.not_isRoot_of_natDegree_ne_one hdeg
 
-lemma _root_.Irreducible.subsingleton_isRoot [IsLeftCancelMulZero R]
+lemma _root_.Irreducible.subsingleton_isRoot
     (hi : Irreducible p) : { x | p.IsRoot x }.Subsingleton :=
   fun _ hx ↦ (subsingleton_isRoot_of_natDegree_eq_one <| natDegree_eq_of_degree_eq_some <|
     degree_eq_one_of_irreducible_of_root hi hx) hx
diff --git a/Mathlib/Algebra/Star/StarRingHom.lean b/Mathlib/Algebra/Star/StarRingHom.lean
index 3a978d56dbf996..a3b62713103402 100644
--- a/Mathlib/Algebra/Star/StarRingHom.lean
+++ b/Mathlib/Algebra/Star/StarRingHom.lean
@@ -260,27 +260,26 @@ namespace StarRingEquivClass
 -- See note [lower instance priority]
 instance (priority := 50) {F A B : Type*} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B]
     [EquivLike F A B] [hF : StarRingEquivClass F A B] :
-    StarHomClass F A B :=
-  { hF with }
+    StarHomClass F A B where
+  __ := hF
 
 -- See note [lower instance priority]
 instance (priority := 100) {F A B : Type*} [NonUnitalNonAssocSemiring A] [Star A]
-    [NonUnitalNonAssocSemiring B] [Star B] [EquivLike F A B] [RingEquivClass F A B]
-    [StarRingEquivClass F A B] : NonUnitalStarRingHomClass F A B :=
-  { }
+    [NonUnitalNonAssocSemiring B] [Star B] [EquivLike F A B] [StarRingEquivClass F A B] :
+    NonUnitalStarRingHomClass F A B where
 
 /-- Turn an element of a type `F` satisfying `StarRingEquivClass F A B` into an actual
 `StarRingEquiv`. This is declared as the default coercion from `F` to `A ≃⋆+* B`. -/
 @[coe]
 def toStarRingEquiv {F A B : Type*} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B]
-    [EquivLike F A B] [RingEquivClass F A B] [StarRingEquivClass F A B] (f : F) : A ≃⋆+* B :=
+    [EquivLike F A B] [StarRingEquivClass F A B] (f : F) : A ≃⋆+* B :=
   { (RingEquivClass.toRingEquiv f : A ≃+* B) with
     map_star' := map_star f }
 
 /-- Any type satisfying `StarRingEquivClass` can be cast into `StarRingEquiv` via
 `StarRingEquivClass.toStarRingEquiv`. -/
 instance instCoeHead {F A B : Type*} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B]
-    [EquivLike F A B] [RingEquivClass F A B] [StarRingEquivClass F A B] : CoeHead F (A ≃⋆+* B) :=
+    [EquivLike F A B] [StarRingEquivClass F A B] : CoeHead F (A ≃⋆+* B) :=
   ⟨toStarRingEquiv⟩
 
 end StarRingEquivClass
diff --git a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean
index 35ad0d20dc6c20..03df3365bc1290 100644
--- a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean
@@ -169,8 +169,6 @@ theorem sqrt_toReal_spectralRadius_self_mul_star_eq_norm (a : A) :
 
 end CStarAlgebra
 
-variable [StarModule ℂ A]
-
 /-- Any element of the spectrum of a selfadjoint is real. -/
 theorem IsSelfAdjoint.mem_spectrum_eq_re {a : A} (ha : IsSelfAdjoint a) {z : ℂ}
     (hz : z ∈ spectrum ℂ a) : z = z.re := by
diff --git a/Mathlib/Analysis/Convex/StdSimplex.lean b/Mathlib/Analysis/Convex/StdSimplex.lean
index d66293dae57801..6d15a5177c2763 100644
--- a/Mathlib/Analysis/Convex/StdSimplex.lean
+++ b/Mathlib/Analysis/Convex/StdSimplex.lean
@@ -86,6 +86,8 @@ theorem ite_eq_mem_stdSimplex (i : ι) : (if i = · then (1 : 𝕜) else 0) ∈
 
 variable [IsOrderedRing 𝕜]
 
+set_option linter.overlappingInstances false
+
 #adaptation_note /-- nightly-2024-03-11
 we need a type annotation on the segment in the following two lemmas. -/
 
diff --git a/Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean b/Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
index a822d8e1b75e34..619b123068af91 100644
--- a/Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
+++ b/Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
@@ -30,7 +30,7 @@ section AddGroup
 variable [AddGroup G]
 
 section Semifield
-variable [Fintype G] [Semifield R] [IsDomain R] [CharZero R] {ψ : AddChar G R}
+variable [Fintype G] [Semifield R] [CharZero R] {ψ : AddChar G R}
 
 lemma expect_eq_ite (ψ : AddChar G R) : 𝔼 a, ψ a = if ψ = 0 then 1 else 0 := by
   simp [Fintype.expect_eq_sum_div_card, sum_eq_ite, ite_div]
diff --git a/Mathlib/Analysis/Normed/Field/Krasner.lean b/Mathlib/Analysis/Normed/Field/Krasner.lean
index 8966dac2e328b4..2054044e2888d8 100644
--- a/Mathlib/Analysis/Normed/Field/Krasner.lean
+++ b/Mathlib/Analysis/Normed/Field/Krasner.lean
@@ -67,7 +67,7 @@ theorem krasner [Field K] [Algebra K L]
   IsKrasner.krasner' hx sp hy h
 
 variable [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K]
-    [NormedAlgebra K L] [Algebra.IsAlgebraic K L]
+    [NormedAlgebra K L]
 
 /-- Krasner's lemma assuming `Normal K L`. -/
 theorem of_completeSpace_of_normal [Normal K L] : IsKrasner K L where
@@ -114,7 +114,7 @@ If `K` is a complete nontrivially normed field and `L` is an algebraic extension
 such that the norm of `L` extends the norm on `K`, then `IsKrasner K L` holds.
 This corresponds to the classical Krasner's lemma.
 -/
-instance of_completeSpace : IsKrasner K L where
+instance of_completeSpace [Algebra.IsAlgebraic K L] : IsKrasner K L where
   krasner' {x} {y} xsep sp yint kr := by
     -- Reduce to the case `L = algebraic closure of K` to apply the previous lemma.
     let C := AlgebraicClosure K
diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean
index b5b34a11866a91..b9c6cf68f86e3b 100644
--- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean
+++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean
@@ -52,6 +52,8 @@ lemma conjSqrt_le_conjSqrt {c a b : A} (h : a ≤ b) : conjSqrt c a ≤ conjSqrt
 
 variable [IsSemitopologicalRing A] [T2Space A]
 
+set_option linter.overlappingInstances false
+
 @[grind =]
 lemma isStrictlyPositive_conjSqrt_iff (c a : A) (hc : IsStrictlyPositive c := by cfc_tac) :
     IsStrictlyPositive (conjSqrt c a) ↔ IsStrictlyPositive a := by
diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean
index 8403145edf7f25..3e35c746f7fcfe 100644
--- a/Mathlib/Analysis/SpecificLimits/Normed.lean
+++ b/Mathlib/Analysis/SpecificLimits/Normed.lean
@@ -952,6 +952,7 @@ lemma tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder
   · rw [← tendsto_zero_iff_norm_tendsto_zero]
     exact tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hmul.norm.isBoundedUnder_le hf₁
 
+set_option linter.overlappingInstances false in
 -- The use case in mind for this is when `K = ℝ`, and `R = ℝ` or `ℂ`
 lemma tendsto_smul_comp_nat_floor_of_tendsto_nsmul [NormSMulClass ℤ K] [LinearOrder K]
     [IsStrictOrderedRing K] [FloorSemiring K] [HasSolidNorm K] {g : ℕ → R} {t : R}
diff --git a/Mathlib/CategoryTheory/Localization/Predicate.lean b/Mathlib/CategoryTheory/Localization/Predicate.lean
index c0a5e2f8ffc2a1..ca88ecb7e2851b 100644
--- a/Mathlib/CategoryTheory/Localization/Predicate.lean
+++ b/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]
diff --git a/Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean
index 5fdd055d657958..02f96505e73e9e 100644
--- a/Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean
+++ b/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.
diff --git a/Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean b/Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
index 996438605450d0..803ff254e3ee77 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
@@ -56,6 +56,7 @@ def Over.mapCongr [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf :
     Over.map Q hf ≅ Over.map (f := g) Q (by cat_disch) :=
   NatIso.ofComponents (fun Y ↦ Over.isoMk (Iso.refl _))
 
+set_option linter.overlappingInstances false in
 /-- `Over.map` preserves identities. -/
 @[simps!]
 def Over.mapId [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := 𝟙 X)
@@ -225,6 +226,7 @@ def Under.mapCongr [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf :
     Under.map Q hf ≅ Under.map (f := g) Q (by cat_disch) :=
   NatIso.ofComponents (fun Y ↦ Under.isoMk (Iso.refl _))
 
+set_option linter.overlappingInstances false in
 /-- `Under.map` preserves identities. -/
 @[simps!]
 def Under.mapId [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := 𝟙 X)
diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean
index 9c8d3d42ec0c5b..38dca9bf636293 100644
--- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean
+++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean
@@ -303,8 +303,7 @@ example : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Full
 example : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful := by
   infer_instance
 
-instance [A.IsVerdierLeftLocalizing B] [Preadditive D₁] [Preadditive D₂]
-    [L₁.Additive] [L₂.Additive] :
+instance [Preadditive D₁] [Preadditive D₂] [L₁.Additive] [L₂.Additive] :
     ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive := by
   let F := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
   rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW]
@@ -316,7 +315,7 @@ instance [A.IsVerdierLeftLocalizing B] [Preadditive D₁] [Preadditive D₂]
 then the induced functor between the localizations with respect to `(B.inverseImage A.ι).trW`
 and `B.trW` is fully faithful. -/
 @[no_expose]
-noncomputable def IsVerdierLeftLocalizing.fullyFaithful [A.IsVerdierLeftLocalizing B]
+noncomputable def IsVerdierLeftLocalizing.fullyFaithful
     {L₁ : A.FullSubcategory ⥤ D₁} {L₂ : C ⥤ D₂} {F : D₁ ⥤ D₂}
     [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW]
     (e : L₁ ⋙ F ≅ A.ι ⋙ L₂) :
diff --git a/Mathlib/Control/Applicative.lean b/Mathlib/Control/Applicative.lean
index ff499c0eaf8c33..e2441e2eeb7c3d 100644
--- a/Mathlib/Control/Applicative.lean
+++ b/Mathlib/Control/Applicative.lean
@@ -40,6 +40,7 @@ theorem Applicative.map_seq_map (f : α → β → γ) (g : σ → β) (x : F α
 theorem Applicative.pure_seq_eq_map' (f : α → β) : ((pure f : F (α → β)) <*> ·) = (f <$> ·) := by
   simp [functor_norm]
 
+set_option linter.overlappingInstances false in
 theorem Applicative.ext {F} :
     ∀ {A1 : Applicative F} {A2 : Applicative F} [@LawfulApplicative F A1] [@LawfulApplicative F A2],
       (∀ {α : Type u} (x : α), @Pure.pure _ A1.toPure _ x = @Pure.pure _ A2.toPure _ x) →
diff --git a/Mathlib/Control/Functor.lean b/Mathlib/Control/Functor.lean
index 37046a426e48de..f428d9e905aa0c 100644
--- a/Mathlib/Control/Functor.lean
+++ b/Mathlib/Control/Functor.lean
@@ -43,6 +43,7 @@ theorem Functor.map_comp_map (f : α → β) (g : β → γ) :
     ((g <$> ·) ∘ (f <$> ·) : F α → F γ) = ((g ∘ f) <$> ·) :=
   funext fun _ => (comp_map _ _ _).symm
 
+set_option linter.overlappingInstances false in
 theorem Functor.ext {F} :
     ∀ {F1 : Functor F} {F2 : Functor F} [@LawfulFunctor F F1] [@LawfulFunctor F F2],
     (∀ (α β) (f : α → β) (x : F α), @Functor.map _ F1 _ _ f x = @Functor.map _ F2 _ _ f x) →
diff --git a/Mathlib/FieldTheory/Normal/Defs.lean b/Mathlib/FieldTheory/Normal/Defs.lean
index ba83063b21b15c..89baf0c28c983a 100644
--- a/Mathlib/FieldTheory/Normal/Defs.lean
+++ b/Mathlib/FieldTheory/Normal/Defs.lean
@@ -90,9 +90,10 @@ theorem AlgEquiv.transfer_normal (f : E ≃ₐ[F] E') : Normal F E ↔ Normal F
   ⟨fun _ ↦ Normal.of_algEquiv f, fun _ ↦ Normal.of_algEquiv f.symm⟩
 
 theorem Normal.of_equiv_equiv {M N : Type*} [Field N] [Field M] [Algebra M N]
-    [Algebra.IsAlgebraic F E] [h : Normal F E] {f : F ≃+* M} {g : E ≃+* N}
+    [h : Normal F E] {f : F ≃+* M} {g : E ≃+* N}
     (hcomp : (algebraMap M N).comp f = (g : E →+* N).comp (algebraMap F E)) :
     Normal M N := by
+  have := h
   rw [normal_iff] at h ⊢
   intro x
   rw [← g.apply_symm_apply x]
diff --git a/Mathlib/GroupTheory/OreLocalization/Basic.lean b/Mathlib/GroupTheory/OreLocalization/Basic.lean
index f6867fd3b5a6db..3510c03ad063e9 100644
--- a/Mathlib/GroupTheory/OreLocalization/Basic.lean
+++ b/Mathlib/GroupTheory/OreLocalization/Basic.lean
@@ -548,6 +548,7 @@ protected def hsmul (c : R) :
     rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
       ← oreDiv_smul_oreDiv, ← OreLocalization.expand])
 
+set_option linter.overlappingInstances false in
 /- Warning: This gives a diamond on `SMul R[S⁻¹] M[S⁻¹][S⁻¹]`, but we will almost never localize
 at the same monoid twice. -/
 /- Although the definition does not require `IsScalarTower R M X`,
diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean
index d0760e71b0bf60..dab3e5140a5402 100644
--- a/Mathlib/Init.lean
+++ b/Mathlib/Init.lean
@@ -16,6 +16,7 @@ public import Mathlib.Tactic.Linter.Header
 public import Mathlib.Tactic.Linter.FlexibleLinter
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
+public import Mathlib.Tactic.Linter.OverlappingInstances
 public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.TacticDocumentation
 -- The following import contains the environment extension for the unused tactic linter.
diff --git a/Mathlib/Lean/Elab/InfoTree.lean b/Mathlib/Lean/Elab/InfoTree.lean
index a7350bfff60158..9755b678eea600 100644
--- a/Mathlib/Lean/Elab/InfoTree.lean
+++ b/Mathlib/Lean/Elab/InfoTree.lean
@@ -99,6 +99,17 @@ def onHighestNode? {α} (t : InfoTree) (ctx? : Option ContextInfo)
     (f : ContextInfo → Info → PersistentArray InfoTree → α) : Option α :=
   t.findSome? (ctx? := ctx?) fun ctx i ch => some (f ctx i ch)
 
+/--
+Returns the context and `info` on the outermost `.node info _` which has
+context, having merged and updated contexts appropriately.
+
+If `ctx?` is `some ctx`, `ctx` is used as an initial context. A `ctx?` of `none` should **only** be
+used when operating on the first node of the entire infotree. Otherwise, it is likely that no
+context will be found.
+-/
+def getHighestInfo? (t : InfoTree) (ctx? : Option ContextInfo) : Option (ContextInfo × Info) :=
+  t.onHighestNode? ctx? fun ctx i _ => (ctx, i)
+
 /--
 Get the `parentDecl`s of every elaborated body.
 
@@ -119,6 +130,22 @@ def getDeclsByBody (t : InfoTree) : List Name :=
       else decls
     | _ => decls
 
+/-- Gets the first child info of each `Lean.Elab.BodyInfo`, which should be the only child, and
+should be a `TermInfo`, `PartialTermInfo`, or `TacticInfo`. `getDeclBodyInfos` does not validate
+either of these conditions. -/
+def getDeclBodyInfos (t : InfoTree) : List (Syntax × ContextInfo × Info) :=
+  t.foldInfoTree (init := []) fun ctx t acc =>
+    match t with
+    | .node (.ofCustomInfo i) body => Id.run do
+      if i.value.typeName == ``Lean.Elab.Term.BodyInfo then
+        if h : 0 < body.size then
+          -- See through `.context`s instead of just matching on `.node`:
+          let result? := body[0].getHighestInfo? ctx
+          if let some result := result? then
+            return (i.stx, result) :: acc
+      return acc
+    | _ => acc
+
 /--
 Get the declarations elaborated in the infotree `t` which are theorems according to the
 environment. This includes e.g. `instance`s of `Prop` classes in addition to declarations declared
@@ -127,4 +154,21 @@ using the keyword `theorem` directly.
 def getTheorems (t : InfoTree) (env : Environment) : List ConstantVal :=
   t.getDeclsByBody.filterMap env.findTheoremConstVal?
 
-end Lean.Elab.InfoTree
+end InfoTree
+
+namespace Info
+
+/-- Gets the local context, and the expected type of the `Info`.
+Handles `TacticInfo`s (looking at the first goal), `TermInfo`s, and `PartialTermInfo`s.
+Does not get the metavariable context; assumes that the caller has accumulated an ambient
+`ContextInfo` at this point which is sufficient. -/
+def getLCtx? : Info → Option (LocalContext × Option Expr)
+  | .ofTacticInfo i => do
+    let g ← i.goalsBefore.head?
+    let decl ← i.mctxBefore.findDecl? g
+    some (decl.lctx, decl.type)
+  | .ofTermInfo i
+  | .ofPartialTermInfo i => some (i.lctx, i.expectedType?)
+  | _ => none
+
+end Lean.Elab.Info
diff --git a/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean b/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
index d7e51e5a7f0298..7372076997fa65 100644
--- a/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
@@ -194,8 +194,8 @@ theorem iIsOrtho.not_isOrtho_basis_self_of_nondegenerate {n : Type w} [Nontrivia
 
 /-- Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate
 iff the basis has no elements which are self-orthogonal. -/
-theorem iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {n : Type w} [Nontrivial R]
-    [IsDomain R] (B : BilinForm R M) (v : Basis n R M) (hO : B.iIsOrtho v) :
+theorem iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {n : Type w} [IsDomain R]
+    (B : BilinForm R M) (v : Basis n R M) (hO : B.iIsOrtho v) :
     B.Nondegenerate ↔ ∀ i, ¬B.IsOrtho (v i) (v i) :=
   ⟨hO.not_isOrtho_basis_self_of_nondegenerate, hO.nondegenerate_of_not_isOrtho_basis_self _⟩
 
diff --git a/Mathlib/LinearAlgebra/Eigenspace/Matrix.lean b/Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
index 4fe412fc1d32c1..595b618e461c91 100644
--- a/Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
+++ b/Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
@@ -41,6 +41,8 @@ lemma hasEigenvector_toLin'_diagonal (d : n → R) (i : n) :
     HasEigenvector (toLin' (diagonal d)) (d i) (Pi.basisFun R n i) :=
   hasEigenvector_toLin_diagonal _ _ (Pi.basisFun R n)
 
+set_option linter.overlappingInstances false
+
 /-- Eigenvalues of a diagonal linear operator are the diagonal entries. -/
 lemma hasEigenvalue_toLin_diagonal_iff (d : n → R) {μ : R} [IsDomain R] [IsTorsionFree R M]
     (b : Basis n R M) : HasEigenvalue (toLin b b (diagonal d)) μ ↔ ∃ i, d i = μ := by
diff --git a/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean b/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
index c0811e35ec06e8..e557a7f8d6b6e1 100644
--- a/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
+++ b/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
@@ -110,6 +110,7 @@ lemma not_isG2_iff_isNotG2 :
   · specialize h i j
     lia
 
+set_option linter.overlappingInstances false in
 lemma IsG2.pairingIn_mem_zero_one_three [P.IsG2]
     (i j : ι) (h : P.root i ≠ P.root j) (h' : P.root i ≠ -P.root j) :
     P.pairingIn ℤ i j ∈ ({-3, -1, 0, 1, 3} : Set ℤ) := by
diff --git a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean
index 5b6e32a7a88c6c..f5504e6ef84b64 100644
--- a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean
+++ b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean
@@ -111,6 +111,7 @@ section chainBotCoeff_mul_chainTopCoeff
 
 variable {b : P.Base} {i j k l m : ι}
 
+set_option linter.overlappingInstances false in
 private lemma chainBotCoeff_mul_chainTopCoeff.aux_0 [P.IsNotG2]
     (hik_mem : P.root k + P.root i ∈ range P.root) :
     P.pairingIn ℤ k i = 0 ∨ (P.pairingIn ℤ k i < 0 ∧ P.chainBotCoeff i k = 0) := by
diff --git a/Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean b/Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean
index c69b973e4e8ff9..f22bdb572a56e1 100644
--- a/Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean
+++ b/Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean
@@ -1007,7 +1007,7 @@ lemma nondegenerate_restrict_iff_disjoint_ker (hs : ∀ x, 0 ≤ B x x) (hB : B.
   have key : x ∈ W ⊓ LinearMap.ker B := ⟨hx, h⟩
   simpa [hW.eq_bot] using key
 
-variable [IsDomain R] [IsTorsionFree R M]
+variable [IsTorsionFree R M]
 
 /-- Strict **Cauchy-Schwarz** is equivalent to linear independence for positive definite forms. -/
 lemma apply_mul_apply_lt_iff_linearIndependent (hp : ∀ x, x ≠ 0 → 0 < B x x) (x y : M) :
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index 74c7b6811593ef..482715df4ee0f9 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -1079,6 +1079,7 @@ theorem beq_ext {α : Type*} (inst1 : BEq α) (inst2 : BEq α)
   funext x y
   exact h x y
 
+set_option linter.overlappingInstances false in
 theorem lawful_beq_subsingleton {α : Type*} (inst1 : BEq α) (inst2 : BEq α)
     [@LawfulBEq α inst1] [@LawfulBEq α inst2] :
     inst1 = inst2 := by
diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
index cf3c08b2e72958..02e96a6e6284dd 100644
--- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
+++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
@@ -445,6 +445,7 @@ theorem condExpL1CLM_of_aestronglyMeasurable' (f : α →₁[μ] F') (hfm : AESt
 
 end CondExpL1CLM
 
+set_option linter.overlappingInstances false in
 /-- Conditional expectation of a function, in L1. Its value is 0 if the function is not
 integrable. The function-valued `condExp` should be used instead in most cases. -/
 def condExpL1 (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)]
diff --git a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
index 133510ba04c807..f4c3ac89204cbb 100644
--- a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
+++ b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
@@ -885,8 +885,7 @@ Given two left-invariant measures which are finite
 on compacts and regular, they coincide up to a multiplicative constant. -/
 @[to_additive isAddLeftInvariant_eq_smul_of_regular]
 lemma isMulLeftInvariant_eq_smul_of_regular [LocallyCompactSpace G]
-    (μ' μ : Measure G) [IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ']
-    [Regular μ] [Regular μ'] :
+    (μ' μ : Measure G) [IsHaarMeasure μ] [IsMulLeftInvariant μ'] [Regular μ] [Regular μ'] :
     μ' = haarScalarFactor μ' μ • μ := by
   have A : ∀ U, IsOpen U → μ' U = (haarScalarFactor μ' μ • μ) U := by
     intro U hU
diff --git a/Mathlib/NumberTheory/ClassNumber/Finite.lean b/Mathlib/NumberTheory/ClassNumber/Finite.lean
index e4acead5a61378..9ececd2e0e3e3c 100644
--- a/Mathlib/NumberTheory/ClassNumber/Finite.lean
+++ b/Mathlib/NumberTheory/ClassNumber/Finite.lean
@@ -265,6 +265,8 @@ theorem ne_bot_of_prod_finsetApprox_mem (J : Ideal S)
     (h : algebraMap _ _ (∏ m ∈ finsetApprox bS adm, m) ∈ J) : J ≠ ⊥ :=
   (Submodule.ne_bot_iff _).mpr ⟨_, h, prod_finsetApprox_ne_zero _ _⟩
 
+set_option linter.overlappingInstances false
+
 /-- Each class in the class group contains an ideal `J`
 such that `M := Π m ∈ finsetApprox` is in `J`. -/
 theorem exists_mk0_eq_mk0 [IsDedekindDomain S] [Algebra.IsAlgebraic R S] (I : (Ideal S)⁰) :
diff --git a/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean b/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
index 16feaf41197085..d1a5dafc52a651 100644
--- a/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
+++ b/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
@@ -148,7 +148,7 @@ end NumberField.Embeddings
 
 section Place
 
-variable {K : Type*} [Field K] {A : Type*} [NormedDivisionRing A] [Nontrivial A] (φ : K →+* A)
+variable {K : Type*} [Field K] {A : Type*} [NormedDivisionRing A] (φ : K →+* A)
 
 /-- An embedding into a normed division ring defines a place of `K` -/
 def NumberField.place : AbsoluteValue K ℝ :=
diff --git a/Mathlib/NumberTheory/RamificationInertia/Galois.lean b/Mathlib/NumberTheory/RamificationInertia/Galois.lean
index 29bb40aa13df0c..c1c03b98160bcd 100644
--- a/Mathlib/NumberTheory/RamificationInertia/Galois.lean
+++ b/Mathlib/NumberTheory/RamificationInertia/Galois.lean
@@ -198,6 +198,8 @@ theorem inertiaDegIn_mul_inertiaDegIn [p.IsMaximal] [P.IsMaximal] :
   rw [inertiaDegIn_eq_inertiaDeg p P G, inertiaDegIn_eq_inertiaDeg p Q GAC,
     inertiaDegIn_eq_inertiaDeg P Q GBC, inertiaDeg_algebra_tower p P Q]
 
+set_option linter.overlappingInstances false
+
 variable {p} in
 include G GAC GBC in
 theorem ramificationIdxIn_mul_ramificationIdxIn [IsDedekindDomain B] [IsDedekindDomain C]
diff --git a/Mathlib/RingTheory/ChainOfDivisors.lean b/Mathlib/RingTheory/ChainOfDivisors.lean
index f23e8be6ecacba..2567220b66644d 100644
--- a/Mathlib/RingTheory/ChainOfDivisors.lean
+++ b/Mathlib/RingTheory/ChainOfDivisors.lean
@@ -244,6 +244,8 @@ variable [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M]
 
 open DivisorChain
 
+set_option linter.overlappingInstances false
+
 theorem pow_image_of_prime_by_factor_orderIso_dvd
     {m p : Associates M} {n : Associates N} (hn : n ≠ 0) (hp : p ∈ normalizedFactors m)
     (d : Set.Iic m ≃o Set.Iic n) {s : ℕ} (hs' : p ^ s ≤ m) :
@@ -376,6 +378,8 @@ def mkFactorOrderIsoOfFactorDvdEquiv [IsCancelMulZero N]
 
 variable [UniqueFactorizationMonoid M] [UniqueFactorizationMonoid N]
 
+set_option linter.overlappingInstances false
+
 theorem mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors {m p : M} {n : N} (hm : m ≠ 0)
     (hn : n ≠ 0) (hp : p ∈ normalizedFactors m) {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }}
     (hd : ∀ l l', (d l : N) ∣ d l' ↔ (l : M) ∣ (l' : M)) :
diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean
index ecf2702d81d56c..53c4d81062fa4d 100644
--- a/Mathlib/RingTheory/ClassGroup.lean
+++ b/Mathlib/RingTheory/ClassGroup.lean
@@ -222,6 +222,8 @@ theorem ClassGroup.mk_canonicalEquiv (K' : Type*) [Field K'] [Algebra R K'] [IsF
       ← Units.map_comp, ← RingEquiv.coe_monoidHom_trans,
       FractionalIdeal.canonicalEquiv_trans_canonicalEquiv]
 
+set_option linter.overlappingInstances false
+
 /-- Send a nonzero integral ideal to an invertible fractional ideal. -/
 def FractionalIdeal.mk0 [IsDedekindDomain R] :
     (Ideal R)⁰ →* (FractionalIdeal R⁰ K)ˣ where
diff --git a/Mathlib/RingTheory/DedekindDomain/Different.lean b/Mathlib/RingTheory/DedekindDomain/Different.lean
index f8423b5d363d6e..e0189143a01d15 100644
--- a/Mathlib/RingTheory/DedekindDomain/Different.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Different.lean
@@ -560,6 +560,8 @@ lemma differentialIdeal_le_iff {I : Ideal B} (hI : I ≠ ⊥) :
 
 variable (A K B L)
 
+set_option linter.overlappingInstances false
+
 open FractionalIdeal in
 /-- Transitivity of the different ideal. -/
 theorem differentIdeal_eq_differentIdeal_mul_differentIdeal (C : Type*) [IsDomain B] [CommRing C]
@@ -683,6 +685,8 @@ variable (L)
 variable [IsFractionRing B L] [IsDedekindDomain A] [IsDedekindDomain B]
   [IsTorsionFree A B] [Module.Finite A B]
 
+set_option linter.overlappingInstances false
+
 include K L in
 lemma pow_sub_one_dvd_differentIdeal_aux
     {p : Ideal A} [p.IsMaximal] (P : Ideal B) {e : ℕ} (he : e ≠ 0) (hp : p ≠ ⊥)
diff --git a/Mathlib/RingTheory/DedekindDomain/Dvr.lean b/Mathlib/RingTheory/DedekindDomain/Dvr.lean
index 84bfe92c8fa629..148e5ee14fe445 100644
--- a/Mathlib/RingTheory/DedekindDomain/Dvr.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Dvr.lean
@@ -75,6 +75,8 @@ theorem Ring.DimensionLEOne.localization {R : Type*} (Rₘ : Type*) [CommRing R]
   refine h.not_lt_lt ⊥ (p.under R) (P.under R) ⟨?_, hpP'⟩
   exact IsLocalization.bot_lt_under_prime _ _ hM _ hp0⟩
 
+set_option linter.overlappingInstances false
+
 /-- The localization of a Dedekind domain is a Dedekind domain. -/
 theorem IsLocalization.isDedekindDomain [IsDedekindDomain A] {M : Submonoid A} (hM : M ≤ A⁰)
     (Aₘ : Type*) [CommRing Aₘ] [IsDomain Aₘ] [Algebra A Aₘ] [IsLocalization M Aₘ] :
diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
index 0131c48e6a37f9..d401bea183103f 100644
--- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
@@ -1186,6 +1186,7 @@ alias _root_.mem_primesOverFinset_iff := mem_primesOverFinset_iff
 
 end IsDedekindDomain
 
+set_option linter.overlappingInstances false in
 variable {R} (A) in
 theorem IsLocalRing.primesOverFinset_eq [IsLocalRing A] [IsDedekindDomain A]
     [Algebra R A] [FaithfulSMul R A] [Module.Finite R A] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :
diff --git a/Mathlib/RingTheory/DedekindDomain/Instances.lean b/Mathlib/RingTheory/DedekindDomain/Instances.lean
index 86f51ed0f6f8fe..982a7cf3602f09 100644
--- a/Mathlib/RingTheory/DedekindDomain/Instances.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Instances.lean
@@ -144,10 +144,12 @@ instance : IsScalarTower Rₚ Sₚ L := by
     RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
     ← IsScalarTower.algebraMap_eq]
 
+set_option linter.overlappingInstances false in
 instance [IsDedekindDomain S] : IsDedekindDomain Sₚ :=
   isDedekindDomain S
     (algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ P.primeCompl_le_nonZeroDivisors) _
 
+set_option linter.overlappingInstances false in
 instance [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [hP : NeZero P] :
     IsPrincipalIdealRing Sₚ :=
   IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P (fun h ↦ hP.1 h)
diff --git a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
index 37151e22f7df1e..7e8ffa3eefa9d3 100644
--- a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
+++ b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
@@ -208,6 +208,8 @@ theorem integralClosure.isNoetherianRing [IsIntegrallyClosed A] [IsNoetherianRin
 
 variable (A K) [IsDomain C]
 
+set_option linter.overlappingInstances false
+
 /-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain,
 the integral closure `C` of `A` in `L` is a Dedekind domain.
 
diff --git a/Mathlib/RingTheory/DedekindDomain/LinearDisjoint.lean b/Mathlib/RingTheory/DedekindDomain/LinearDisjoint.lean
index b6d0791e01c094..d504e598dc6aab 100644
--- a/Mathlib/RingTheory/DedekindDomain/LinearDisjoint.lean
+++ b/Mathlib/RingTheory/DedekindDomain/LinearDisjoint.lean
@@ -76,6 +76,8 @@ variable [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDo
     [IsFractionRing B L] [IsFractionRing R₁ F₁] [IsFractionRing R₂ F₂] [IsIntegrallyClosed A]
     [IsIntegralClosure B R₁ L] [IsTorsionFree R₁ B] [IsTorsionFree R₂ B]
 
+set_option linter.overlappingInstances false
+
 namespace IsDedekindDomain
 
 theorem differentIdeal_dvd_map_differentIdeal [Algebra.IsIntegral R₂ B]
diff --git a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
index ccf0649bb93f6f..f1a75c850f1310 100644
--- a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
+++ b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
@@ -92,8 +92,8 @@ theorem exists_maximalIdeal_pow_eq_of_principal [IsNoetherianRing R] [IsLocalRin
   · rw [hx, Ideal.span_singleton_pow, Ideal.span_le, Set.singleton_subset_iff]
     exact Nat.find_spec this
 
-theorem maximalIdeal_isPrincipal_of_isDedekindDomain [IsLocalRing R] [IsDomain R]
-    [IsDedekindDomain R] : (maximalIdeal R).IsPrincipal := by
+theorem maximalIdeal_isPrincipal_of_isDedekindDomain [IsLocalRing R] [IsDedekindDomain R] :
+    (maximalIdeal R).IsPrincipal := by
   classical
   by_cases ne_bot : maximalIdeal R = ⊥
   · rw [ne_bot]; infer_instance
diff --git a/Mathlib/RingTheory/FractionalIdeal/Extended.lean b/Mathlib/RingTheory/FractionalIdeal/Extended.lean
index ccea9938b35ee0..ee07c0d90eb66e 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Extended.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Extended.lean
@@ -244,6 +244,8 @@ theorem extendedHom_le_one_iff [IsIntegrallyClosed A] [IsIntegrallyClosed B] :
 
 section IsDedekindDomain
 
+set_option linter.overlappingInstances false
+
 variable [IsDedekindDomain A] [IsDedekindDomain B]
 
 theorem one_le_extendedHom_iff (hI : I ≠ 0) : 1 ≤ extendedHom L B I ↔ 1 ≤ I := by
diff --git a/Mathlib/RingTheory/HahnSeries/Lex.lean b/Mathlib/RingTheory/HahnSeries/Lex.lean
index 842ad48b5145fd..d7ed4861f1fcb7 100644
--- a/Mathlib/RingTheory/HahnSeries/Lex.lean
+++ b/Mathlib/RingTheory/HahnSeries/Lex.lean
@@ -389,7 +389,7 @@ instance [IsOrderedRing R] [NoZeroDivisors R] : IsOrderedRing (Lex R⟦Γ⟧) wh
     · rwa [leadingCoeff_nonneg_iff]
     · simpa
 
-instance [IsDomain R] [IsStrictOrderedRing R] : IsStrictOrderedRing (Lex R⟦Γ⟧) where
+instance [IsStrictOrderedRing R] : IsStrictOrderedRing (Lex R⟦Γ⟧) where
 
 end OrderedRing
 
diff --git a/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean b/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
index 0b107f99397c57..a8f308649071e7 100644
--- a/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
+++ b/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
@@ -198,7 +198,7 @@ theorem cardQuot_mul [IsDedekindDomain S] [Module.Free ℤ S] (I J : Ideal S) :
           (hIJ (Ideal.dvd_iff_le.mpr le_sup_left) (Ideal.dvd_iff_le.mpr le_sup_right)))
 
 /-- The absolute norm of the ideal `I : Ideal R` is the cardinality of the quotient `R ⧸ I`. -/
-noncomputable def Ideal.absNorm [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] :
+noncomputable def Ideal.absNorm [IsDedekindDomain S] [Module.Free ℤ S] :
     Ideal S →*₀ ℕ where
   toFun := Submodule.cardQuot
   map_mul' I J := by rw [cardQuot_mul]
@@ -209,7 +209,7 @@ noncomputable def Ideal.absNorm [Nontrivial S] [IsDedekindDomain S] [Module.Free
 
 namespace Ideal
 
-variable [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S]
+variable [IsDedekindDomain S] [Module.Free ℤ S]
 
 theorem absNorm_apply (I : Ideal S) : absNorm I = cardQuot I := rfl
 
diff --git a/Mathlib/RingTheory/Ideal/Norm/RelNorm.lean b/Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
index e7004eed7607e4..74b68815f1914c 100644
--- a/Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
+++ b/Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
@@ -192,6 +192,8 @@ theorem spanNorm_le_comap (I : Ideal S) : spanNorm R I ≤ comap (algebraMap R S
   | add _ _ _ _ hx hy => exact Submodule.add_mem _ hx hy
   | smul _ _ _ hx => exact Submodule.smul_mem _ _ hx
 
+set_option linter.overlappingInstances false
+
 /-- Multiplicativity of `Ideal.spanNorm`. simp-normal form is `map_mul (Ideal.relNorm R)`. -/
 theorem spanNorm_mul [IsDedekindDomain R] [IsDedekindDomain S] (I J : Ideal S) :
     spanNorm R (I * J) = spanNorm R I * spanNorm R J := by
diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean
index 6e26c40fe75874..f3c37bcdb40462 100644
--- a/Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean
+++ b/Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean
@@ -35,7 +35,7 @@ instance [Algebra.IsSeparable (A ⧸ p) (B ⧸ q)] :
   ext x
   simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]
 
-instance [p.IsMaximal] [q.IsMaximal] [Algebra.IsSeparable p.ResidueField q.ResidueField] :
+instance [Algebra.IsSeparable p.ResidueField q.ResidueField] :
     Algebra.IsSeparable (A ⧸ p) (B ⧸ q) := by
   refine Algebra.IsSeparable.of_equiv_equiv
     (.symm <| .ofBijective _ p.bijective_algebraMap_quotient_residueField)
diff --git a/Mathlib/RingTheory/NormalClosure.lean b/Mathlib/RingTheory/NormalClosure.lean
index e412603b1c5bab..03624140bf835a 100644
--- a/Mathlib/RingTheory/NormalClosure.lean
+++ b/Mathlib/RingTheory/NormalClosure.lean
@@ -126,6 +126,8 @@ instance : IsGalois K (FractionRing T) := by
 
 variable [IsDedekindDomain S]
 
+set_option linter.overlappingInstances false
+
 instance : Module.Finite S T :=
   IsIntegralClosure.finite S L E T
 
diff --git a/Mathlib/RingTheory/Valuation/RankOne.lean b/Mathlib/RingTheory/Valuation/RankOne.lean
index dcf66cb8d5c942..1316d30f2bb7e2 100644
--- a/Mathlib/RingTheory/Valuation/RankOne.lean
+++ b/Mathlib/RingTheory/Valuation/RankOne.lean
@@ -131,7 +131,7 @@ instance : IsNontrivial v where
 
 section Restrict
 
-instance isNontrivial_restrict [v.IsNontrivial] : (v.restrict).IsNontrivial where
+instance isNontrivial_restrict : (v.restrict).IsNontrivial where
   exists_val_nontrivial := by
     obtain ⟨x, ⟨hx0, hx1⟩⟩ := IsNontrivial.exists_val_nontrivial (v := v)
     exact ⟨x, by simp [hx0], by grind [restrict_eq_one_iff]⟩
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index f127f12741db40..bf34ec4f9fd6bb 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -178,6 +178,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
diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean
index c3e7f66e5c96bf..39d6bd05085bbe 100644
--- a/Mathlib/Tactic/Linter/DirectoryDependency.lean
+++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean
@@ -224,6 +224,8 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[
   -- For more fine-grained exceptions of the next two imports, one needs to rename that file.
   (`Mathlib.Tactic.Linter, `ImportGraph),
   (`Mathlib.Tactic.Linter, `Mathlib.Tactic.MinImports),
+  (`Mathlib.Tactic.Linter.OverlappingInstances, `Mathlib.Lean.ContextInfo),
+  (`Mathlib.Tactic.Linter.OverlappingInstances, `Mathlib.Lean.Elab.Tactic.Meta),
   (`Mathlib.Tactic.Linter.TextBased, `Mathlib.Data.Nat.Notation),
   (`Mathlib.Tactic.Linter.UnusedInstancesInType, `Mathlib.Lean.Expr.Basic),
   (`Mathlib.Tactic.Linter.UnusedInstancesInType, `Mathlib.Lean.Environment),
diff --git a/Mathlib/Tactic/Linter/OverlappingInstances.lean b/Mathlib/Tactic/Linter/OverlappingInstances.lean
new file mode 100644
index 00000000000000..4bfd16a8ee01df
--- /dev/null
+++ b/Mathlib/Tactic/Linter/OverlappingInstances.lean
@@ -0,0 +1,236 @@
+/-
+Copyright (c) 2026 Jovan Gerbscheid. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jovan Gerbscheid, Thomas R. Murrills
+-/
+module
+
+public meta import Lean.Elab.Command
+public meta import Mathlib.Lean.ContextInfo
+public meta import Batteries.Lean.Position
+public meta import Mathlib.Tactic.Linter.UnusedInstancesInType
+
+/-!
+# A linter for declarations with local instances that overlap
+
+If the same data can be obtained from two different instances, we risk having
+non-defeq versions of that data. This situation is known as an "instance diamond".
+This linter warns against instance diamonds in local contexts.
+
+This is a syntax linter. It is run on partially and fully elaborated declarations.
+
+To find diamonds, we compute the parent classes of each local instance.
+For classes that aren't structures, this is just the class itself.
+If any of these parent classes is duplicated, we throw a warning.
+
+This linter also warns on redundant proposition classes, i.e. those that can be synthesized from
+the other instances in the local context. (Note: we do *not* warn on proposition classes that
+merely overlap.) Even though redundant proposition classes cause no meaningful issue, they are
+still undesirable.
+
+A common case where this linter may fire is if the same type class assumption is given in both a
+`variable` statement and a declaration. This kind of variable shadowing does not actually produce
+declarations with duplicate type class assumptions, but it is still not desirable.
+
+
+## TODO
+
+Support declarations without bodies (`structure`s/`class`es/`inductive`s etc.)
+
+-/
+
+open Lean Meta Elab Command
+
+meta section
+
+namespace Mathlib.Linter.OverlappingInstances
+
+/-- Clear the instances from the given application.
+This is used to deal with classes that have instance parameters.
+For example, if you have a local instance of `ContinuousAdd α` and `IsTopologicalAddGroup α`,
+then the two `ContinuousAdd α` instances may have slightly different `[Add α]` arguments. -/
+def eraseInstances (e : Expr) : MetaM Expr := do
+  e.withApp fun f args ↦ do
+  let finfo ← getFunInfo f
+  let mut args := args
+  for param in finfo.paramInfo, i in *...args.size do
+    if param.binderInfo.isInstImplicit then
+      args := args.set! i default
+  return mkAppN f args
+
+/-- Compute the parent classes of `cls`, excluding parent classes that have a parent themselves.
+The reason to exclude such classes is that if there is a duplication in such a class,
+then there will necessarily also be a duplication in its parent.
+If `cls` carries data, then only consider parents that carry data.
+If `cls` is a non-structure class, this simply returns `#[cls]`.
+
+The resulting expressions contain bound variables that correspond to the parameters of `cls`.
+The universe levels and bound variables need to be instantiated to get concrete data projections. -/
+partial def getAbstractProjections (cls : Name) : CoreM (Array Expr) := do
+  let cinfo ← getConstInfo cls
+  MetaM.run' <| forallTelescope cinfo.type fun xs type ↦ do
+    withLocalDeclD `self (mkAppN (.const cls (cinfo.levelParams.map .param)) xs) fun inst ↦ do
+      go cls inst #[] xs type.isProp |>.run' {}
+where
+  go (cls : Name) (inst : Expr) (acc : Array Expr) (xs : Array Expr) (isProp : Bool) :
+      StateRefT NameSet MetaM (Array Expr) := do
+    let type ← whnf (← inferType inst)
+    let mut acc := acc
+    let mut anyParent := false
+    if let some info := getStructureInfo? (← getEnv) cls then
+      let .const _ us := type.getAppFn | panic! s!"`{inst} is not an instance"
+      for info in info.parentInfo do
+        let parent := info.structName
+        if (← get).contains parent then continue
+        modify (·.insert parent)
+        unless ← isInstance info.projFn do continue
+        let isProp' := (← getConstInfo parent).type.getForallBody.isProp
+        let proj := Expr.app (mkAppN (.const info.projFn us) type.getAppArgs) inst
+        acc ← go parent proj acc xs isProp'
+        -- When projecting from a data-carrying class to a `Prop` class,
+        -- we record the data-carrying class. This helps with determining which overlaps have data.
+        unless !isProp && isProp' do
+          anyParent := true
+    if !anyParent then
+      acc := acc.push (← eraseInstances (type.abstract xs))
+    return acc
+
+/-- A cache for the result of `getAbstractDataProjections`. -/
+initialize classProjectionsCache : IO.Ref (NameMap (Array Expr)) ← IO.mkRef {}
+
+/-- Return the result of `getAbstractDataProjections`, using a global cache.
+To ensure soundness, the cache is only used for imported declarations. -/
+def getAbstractProjectionsCached (cls : Name) : CoreM (Array Expr) := do
+  if (← getEnv).isImportedConst cls then
+    if let some result := (← classProjectionsCache.get).find? cls then
+      return result
+    let result ← getAbstractProjections cls
+    classProjectionsCache.modify (·.insert cls result)
+    return result
+  else
+    getAbstractProjections cls
+
+/-- Find classes for which multiple different instances can be synthesized in the local context.
+The result maps classes to the (at least 2) local instances that generate them. -/
+partial def findOverlappingInstances : MetaM (ExprMap (Array FVarId)) := do
+  -- Maps a class to the collection of local instances that overlap on it.
+  -- This only includes overlaps of at least 2 local instances.
+  let mut overlaps : ExprMap (Array FVarId) := {}
+  -- Maps a class to the first local instance that produces an instance of it.
+  let mut encountered : ExprMap FVarId := {}
+  for decl in ← getLCtx do
+    if decl.binderInfo.isInstImplicit then
+      let type ← instantiateMVars decl.type
+      let projClasses ← forallTelescopeReducing (whnfType := true) type fun xs type ↦ do
+        type.withApp fun f args ↦ do
+        let .const cls us := f |
+          return #[] -- This can happen when using `set_option checkBinderAnnotations false`
+        let levelParams := (← getConstInfo cls).levelParams
+        let projs ← getAbstractProjectionsCached cls
+        projs.mapM fun proj ↦
+          mkForallFVars xs <| (proj.instantiateLevelParams levelParams us).instantiateRev args
+      for projCls in projClasses do
+        if let some fvarId' := encountered[projCls]? then
+          overlaps := overlaps.alter projCls (·.getD #[fvarId'] |>.push decl.fvarId)
+        else
+          encountered := encountered.insert projCls decl.fvarId
+  return overlaps
+
+/-- Lints against overlaps between instances in the local contexts of declarations. -/
+register_option linter.overlappingInstances : Bool := {
+  defValue := true
+  descr := "enable the overlapping instances linter."
+}
+
+/-- Report a warning message if there are any overlapping instances in the local context.
+For `Prop` instances, only report local instances that are redundant. -/
+def runLinter (ctx : ContextInfo) (lctx : LocalContext) (expectedType? : Option Expr) :
+    IO (Option MessageData) := do
+  ctx.runMetaM lctx do
+  -- Add the hypotheses of the expected type to the local context, as it may have more instances.
+  expectedType?.elim id (forallTelescope · fun _ _ => ·) do
+  let overlaps ← findOverlappingInstances
+  if overlaps.isEmpty then
+    return none
+  -- Sort the suggestions in a (somewhat) deterministic way.
+  let overlaps := overlaps.toArray.qsort (·.1.lt ·.1)
+  let sortedOverlaps : Std.HashMap (Array FVarId) (Array Expr) :=
+    overlaps.foldl (init := {}) fun s (overlap, fvars) ↦ s.alter fvars (·.getD #[] |>.push overlap)
+  let sortedOverlaps := sortedOverlaps.toArray.qsort (Array.lex ·.2 ·.2 Expr.lt)
+  let mut msgs := #[]
+  let mut needsDiamondMsg := false
+  for (fvars, overlaps) in sortedOverlaps do
+    let fvarTypes ← fvars.mapM (do instantiateMVars <| ← ·.getType)
+    -- If the overlapping instances are the same, use a simple message.
+    if fvarTypes.all (· == fvarTypes[0]!) then
+      msgs := msgs.push <|
+        m!"There are {fvarTypes.size} `{.sbracket fvarTypes[0]!}` instances; one is sufficient."
+    else
+      let propOverlap ← overlaps.allM isProp
+      unless propOverlap do
+        needsDiamondMsg := true
+      -- Ignore `Prop` overlaps when data conflicts are present.
+      let overlaps ← if propOverlap then pure overlaps else overlaps.filterM (notM <| isProp ·)
+      let localInsts := (← getLCtx).decls.toList.reduceOption
+      -- Otherwise, figure out which instances can be synthesized from the other instances
+      let mut redundant := #[]
+      for fvar in fvars, type in fvarTypes do
+        let localInsts := localInsts.filter (·.fvarId != fvar)
+        if (← withLocalInstances localInsts (trySynthInstance type)) matches .some _ then
+          redundant := redundant.push type
+      -- For `Prop` overlaps, only warn if there is an instance that can be removed.
+      if propOverlap && redundant.isEmpty then
+        continue
+      let fvarTypes := .andList <| fvarTypes.toList.map (m!"`{.sbracket ·}`")
+      let overlaps := .andList <| overlaps.toList.map (m!"`{.sbracket ·}`")
+      let mut msg :=
+        m!"{fvarTypes} {if propOverlap then "each imply" else
+          "can be used to infer conflicting versions of"} {overlaps}."
+      unless redundant.isEmpty do
+        let redundant' := .andList <| redundant.toList.map (m!"`{.sbracket ·}`")
+        msg := m!"{msg}\n💡️ Of these, {redundant'} may be removed."
+      msgs := msgs.push msg
+  if msgs.isEmpty then
+    return none
+  let inDecl ← if let some decl := ctx.parentDecl? then
+    pure m!" in `{← addMessageContextPartial (.ofConstName decl)}`" else pure ""
+  let mut msg := m!"Overlapping instance parameters{inDecl}:\n"
+  for overlapMsg in msgs do
+    msg := msg ++ m!"\n⚠️ {overlapMsg}"
+  if needsDiamondMsg then
+    msg := msg ++ m!"\n\n\
+      When a data-carrying type class has multiple potential instances coming from different \
+      instance parameters, then these potential instances are incompatible. This is an example of \
+      an \"instance diamond\", which leads to unexpected unification failures.\
+      \n\n\
+      Delete or combine some of your instance parameters to avoid this."
+  addMessageContextFull msg
+
+initialize registerTraceClass `overlappingInstances
+
+open Linter in
+/--
+Lints against data-carrying overlaps between instances in the local contexts of declarations.
+-/
+def overlappingInstances : Linter where
+  run := UnusedInstancesInType.withSetBoolOptionIn fun cmd => do
+    unless getLinterValue linter.overlappingInstances (← getLinterOptions) do
+      return
+    -- Note: we don't break on errors; we want to lint even on partial declarations
+    profileitM Exception "overlappingInstancesLinter" (← getOptions) do
+    for t in ← getInfoTrees do
+      for (ref, ctx, info) in t.getDeclBodyInfos do
+        let some (lctx, expectedType?) := info.getLCtx? | pure ()
+        withTraceNode `overlappingInstances
+          (fun _ ↦ return m!"linting `{.ofConstName <| ctx.parentDecl?.getD .anonymous}`") do
+        let some msg ← runLinter ctx lctx expectedType? | pure ()
+        /- Log the warning from the declaration's selection range (usually the declaration name,
+        or `instance`) to the body if possible. This underlines the hypotheses and type,
+        and makes the warning visible in the infoview when the cursor is within the body. -/
+        let declRange? ← ctx.parentDecl?.bindM findDeclarationSyntaxRange?
+        let ref := declRange?.elim ref (mkNullNode #[.ofRange ·, ref])
+        logLint linter.overlappingInstances ref msg
+
+initialize addLinter overlappingInstances
+
+end Mathlib.Linter.OverlappingInstances
diff --git a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean
index 2f260cdd2459de..72e03512cdafc3 100644
--- a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean
+++ b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean
@@ -285,7 +285,7 @@ def isDecidableVariant (type : Expr) : Bool :=
 
 /-- `withSetOptionIn` currently breaks infotree searches, so we simply set `Bool` options
 until this is fixed in [lean4#11313](https://github.com/leanprover/lean4/pull/11313). -/
-partial def withSetBoolOptionIn (x : CommandElab) : CommandElab
+public partial def withSetBoolOptionIn (x : CommandElab) : CommandElab
   | `(command| set_option $opt:ident $val in $cmd:command) => do
     match val.raw with
     | Syntax.atom _ "true"  =>
diff --git a/Mathlib/Tactic/NormNum/Ineq.lean b/Mathlib/Tactic/NormNum/Ineq.lean
index 99571399a7cec0..74518ce20e9761 100644
--- a/Mathlib/Tactic/NormNum/Ineq.lean
+++ b/Mathlib/Tactic/NormNum/Ineq.lean
@@ -89,7 +89,7 @@ theorem isNNRat_le_true [Semiring α] [LinearOrder α] [IsStrictOrderedRing α]
     simp only [Nat.mul_eq, Nat.cast_mul, mul_invOf_cancel_right'] at h
     rwa [Nat.commute_cast] at h
 
-theorem isNNRat_lt_true [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α] :
+theorem isNNRat_lt_true [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] :
     {a b : α} → {na nb : ℕ} → {da db : ℕ} →
     IsNNRat a na da → IsNNRat b nb db → decide (na * db < nb * da) → a < b
   | _, _, _, _, da, db, ⟨_, rfl⟩, ⟨_, rfl⟩, h => by
@@ -101,7 +101,7 @@ theorem isNNRat_lt_true [Semiring α] [LinearOrder α] [IsStrictOrderedRing α]
     simp? at h says simp only [Nat.cast_mul, mul_invOf_cancel_right'] at h
     rwa [Nat.commute_cast] at h
 
-theorem isNNRat_le_false [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α]
+theorem isNNRat_le_false [Semiring α] [LinearOrder α] [IsStrictOrderedRing α]
     {a b : α} {na nb : ℕ} {da db : ℕ}
     (ha : IsNNRat a na da) (hb : IsNNRat b nb db) (h : decide (nb * da < na * db)) : ¬a ≤ b :=
   not_le_of_gt (isNNRat_lt_true hb ha h)
@@ -125,7 +125,7 @@ theorem isRat_le_true [Ring α] [LinearOrder α] [IsStrictOrderedRing α] :
       mul_invOf_cancel_right'] at h
     rwa [Int.commute_cast] at h
 
-theorem isRat_lt_true [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α] :
+theorem isRat_lt_true [Ring α] [LinearOrder α] [IsStrictOrderedRing α] :
     {a b : α} → {na nb : ℤ} → {da db : ℕ} →
     IsRat a na da → IsRat b nb db → decide (na * db < nb * da) → a < b
   | _, _, _, _, da, db, ⟨_, rfl⟩, ⟨_, rfl⟩, h => by
@@ -137,7 +137,7 @@ theorem isRat_lt_true [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontr
     simp? at h says simp only [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h
     rwa [Int.commute_cast] at h
 
-theorem isRat_le_false [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α]
+theorem isRat_le_false [Ring α] [LinearOrder α] [IsStrictOrderedRing α]
     {a b : α} {na nb : ℤ} {da db : ℕ}
     (ha : IsRat a na da) (hb : IsRat b nb db) (h : decide (nb * da < na * db)) : ¬a ≤ b :=
   not_le_of_gt (isRat_lt_true hb ha h)
diff --git a/Mathlib/Topology/Algebra/MulAction.lean b/Mathlib/Topology/Algebra/MulAction.lean
index 5dde5946dbe3fd..09789bd4d954c9 100644
--- a/Mathlib/Topology/Algebra/MulAction.lean
+++ b/Mathlib/Topology/Algebra/MulAction.lean
@@ -330,6 +330,7 @@ theorem continuousSMul_iInf {ts' : ι → TopologicalSpace X}
     (h : ∀ i, @ContinuousSMul M X _ _ (ts' i)) : @ContinuousSMul M X _ _ (⨅ i, ts' i) :=
   continuousSMul_sInf <| Set.forall_mem_range.mpr h
 
+set_option linter.overlappingInstances false in
 @[to_additive]
 theorem continuousSMul_inf {t₁ t₂ : TopologicalSpace X} [@ContinuousSMul M X _ _ t₁]
     [@ContinuousSMul M X _ _ t₂] : @ContinuousSMul M X _ _ (t₁ ⊓ t₂) := by
diff --git a/Mathlib/Topology/Algebra/Nonarchimedean/Completion.lean b/Mathlib/Topology/Algebra/Nonarchimedean/Completion.lean
index d84352703a98a9..e1461995043d87 100644
--- a/Mathlib/Topology/Algebra/Nonarchimedean/Completion.lean
+++ b/Mathlib/Topology/Algebra/Nonarchimedean/Completion.lean
@@ -64,7 +64,6 @@ instance {G : Type*} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G]
     exact closure_minimal (Set.image_subset_iff.mpr hCW) C_closed
 
 /-- The completion of a nonarchimedean ring is a nonarchimedean ring. -/
-instance {R : Type*} [Ring R] [UniformSpace R] [IsTopologicalRing R] [IsUniformAddGroup R]
-    [NonarchimedeanRing R] :
+instance {R : Type*} [Ring R] [UniformSpace R] [IsUniformAddGroup R] [NonarchimedeanRing R] :
     NonarchimedeanRing (Completion R) where
   is_nonarchimedean := NonarchimedeanAddGroup.is_nonarchimedean
diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/Mathlib/Topology/Connected/PathConnected.lean
index 46e8b52415fa8e..4f062ef7f1aec4 100644
--- a/Mathlib/Topology/Connected/PathConnected.lean
+++ b/Mathlib/Topology/Connected/PathConnected.lean
@@ -565,7 +565,7 @@ variable [PathConnectedSpace X]
 def somePath (x y : X) : Path x y :=
   Nonempty.some (joined x y)
 
-instance [PathConnectedSpace X] : Subsingleton (ZerothHomotopy X) :=
+instance : Subsingleton (ZerothHomotopy X) :=
   (pathConnectedSpace_iff_zerothHomotopy.1 inferInstance).2
 
 end PathConnectedSpace
diff --git a/MathlibTest/OverlappingInstances.lean b/MathlibTest/OverlappingInstances.lean
new file mode 100644
index 00000000000000..5e9019262dbb55
--- /dev/null
+++ b/MathlibTest/OverlappingInstances.lean
@@ -0,0 +1,391 @@
+module
+
+import Mathlib.Tactic.Linter.OverlappingInstances
+import Mathlib.Init
+
+public section
+
+class SubBar (α : Type) where
+  a' : α
+
+class Bar (α : Type) extends SubBar α where
+  a : α
+
+class Baz (α : Type) where
+  b : α
+
+class Baq (α : Type) where
+  b : α
+
+class FooBarBaz (α) extends Bar α, Baz α
+
+class FooBarBaz' (α) extends Bar α, Baz α
+
+class FooBarBaq (α) extends Bar α, Baq α
+
+/--
+error: unsolved goals
+inst✝¹ inst✝ : Add Nat
+⊢ [Add Nat] → [Add Nat] → Bool
+---
+warning: Overlapping instance parameters in `foo`:
+
+⚠️ There are 4 `[Add Nat]` instances; one is sufficient.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+def foo [Add Nat] [Add Nat] : [Add Nat] → [Add Nat] → Bool := by
+  skip
+
+/--
+@ +3:21...+4:12
+warning: Overlapping instance parameters in `foo₁`:
+
+⚠️ `[FooBarBaz Nat]` and `[FooBarBaq Nat]` can be used to infer conflicting versions of `[SubBar Nat]`.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs (positions := true) in
+set_option linter.overlappingInstances true in
+/-- A docstring! -/
+@[expose] public def foo₁ [FooBarBaz Nat] [FooBarBaq Nat] : Bool := by
+  exact true
+
+/--
+warning: Overlapping instance parameters in `foo₂`:
+
+⚠️ There are 2 `[FooBarBaz Nat]` instances; one is sufficient.
+⚠️ `[FooBarBaz
+   Nat]`, `[FooBarBaz Nat]`, and `[FooBarBaq Nat]` can be used to infer conflicting versions of `[SubBar Nat]`.
+💡️ Of these, `[FooBarBaz Nat]` and `[FooBarBaz Nat]` may be removed.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+def foo₂ [FooBarBaz Nat] [FooBarBaz Nat] [FooBarBaq Nat] : Bool := true
+
+/--
+warning: Overlapping instance parameters in `foo₃`:
+
+⚠️ There are 2 `[FooBarBaz Nat]` instances; one is sufficient.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+def foo₃ [FooBarBaz Nat] [FooBarBaz Nat] : Bool := true
+
+/--
+warning: Overlapping instance parameters in `foo₄`:
+
+⚠️ There are 2 `[FooBarBaz Nat]` instances; one is sufficient.
+⚠️ `[FooBarBaz Nat]`, `[FooBarBaz Nat]`, and `[Bar Nat]` can be used to infer conflicting versions of `[SubBar Nat]`.
+💡️ Of these, `[FooBarBaz Nat]`, `[FooBarBaz Nat]`, and `[Bar Nat]` may be removed.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+theorem foo₄ [FooBarBaz Nat] [FooBarBaz Nat] [Bar Nat] : True := trivial
+
+/--
+warning: Overlapping instance parameters in `foo₅`:
+
+⚠️ `[FooBarBaz Nat]` and `[FooBarBaz' Nat]` can be used to infer conflicting versions of `[Baz Nat]` and `[SubBar Nat]`.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+lemma foo₅ [FooBarBaz Nat] [FooBarBaz' Nat] : True := trivial
+
+/--
+warning: Overlapping instance parameters in `foo₆`:
+
+⚠️ `[FooBarBaz Nat]` and `[FooBarBaz' Nat]` can be used to infer conflicting versions of `[Baz Nat]`.
+⚠️ `[FooBarBaz
+   Nat]`, `[FooBarBaz' Nat]`, and `[FooBarBaq Nat]` can be used to infer conflicting versions of `[SubBar Nat]`.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+lemma foo₆ [FooBarBaz Nat] [FooBarBaz' Nat] [FooBarBaq Nat] : True := trivial
+
+namespace Foo
+
+/-! Test unresolving name (`foo`, not `Foo.foo` or `_private...foo`) -/
+
+/--
+warning: Overlapping instance parameters in `foo`:
+
+⚠️ There are 2 `[Add Nat]` instances; one is sufficient.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+private def foo [Add Nat] [Add Nat] : Bool := true
+
+end Foo
+
+namespace prop
+
+class IsFoo : Prop
+
+class IsBar : Prop extends IsFoo
+
+class IsBaz : Prop extends IsBar
+
+/--
+warning: Overlapping instance parameters in `_example`:
+
+⚠️ `[IsBar]` and `[IsBaz]` each imply `[IsFoo]`.
+💡️ Of these, `[IsBar]` may be removed.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+example [IsBar] [IsBaz] : True := trivial
+
+class Bar : Type extends IsFoo
+class Baz : Type extends IsFoo
+class Baz1 : Type extends Baz
+class Baz2 : Type extends Baz
+
+/--
+warning: Overlapping instance parameters in `_example`:
+
+⚠️ `[IsFoo]` and `[Bar]` each imply `[IsFoo]`.
+💡️ Of these, `[IsFoo]` may be removed.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+example [IsFoo] [Bar] : True := trivial
+
+example [IsBar] [Bar] : True := trivial
+
+example [Bar] [Baz] : True := trivial
+
+/--
+warning: Overlapping instance parameters in `_example`:
+
+⚠️ There are 2 `[Baz]` instances; one is sufficient.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+example [Baz] [Baz] : True := trivial
+
+/--
+warning: Overlapping instance parameters in `_example`:
+
+⚠️ `[Baz]` and `[Baz1]` can be used to infer conflicting versions of `[Baz]`.
+💡️ Of these, `[Baz]` may be removed.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+example [Baz] [Baz1] : True := trivial
+
+/--
+warning: Overlapping instance parameters in `_example`:
+
+⚠️ `[Baz1]` and `[Baz2]` can be used to infer conflicting versions of `[Baz]`.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+example [Baz1] [Baz2] : True := trivial
+
+end prop
+
+section duplicates
+
+/-! Make sure we warn on duplicate inductive classes and duplicate `Prop` classes. -/
+
+class inductive IndFoo where
+| mk₁ (n : Nat) | mk₂ (b : Bool)
+
+/--
+warning: Overlapping instance parameters in `indFoo`:
+
+⚠️ There are 2 `[IndFoo]` instances; one is sufficient.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+def indFoo [IndFoo] [IndFoo] : Bool := true
+
+class inductive IndFooProp : Prop where
+| mk₁ (n : Nat) | mk₂ (b : Bool)
+
+/--
+warning: Overlapping instance parameters in `indFooProp`:
+
+⚠️ There are 2 `[IndFooProp]` instances; one is sufficient.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+def indFooProp [IndFooProp] [IndFooProp] : Bool := true
+
+end duplicates
+
+section instantiateMVars
+
+variable {α : Type*} [Repr α]
+
+/--
+warning: Overlapping instance parameters in `needsInstantiateMVars`:
+
+⚠️ There are 2 `[Repr α]` instances; one is sufficient.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+def needsInstantiateMVars [Repr α] : Bool := true
+
+end instantiateMVars
+
+section setOptionIn
+
+set_option linter.overlappingInstances false in
+def fooNothing [Add Nat] [Add Nat] : [Add Nat] → [Add Nat] → Bool := true
+
+set_option linter.overlappingInstances false
+
+/--
+warning: Overlapping instance parameters in `fooSomething`:
+
+⚠️ There are 4 `[Add Nat]` instances; one is sufficient.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+set_option linter.overlappingInstances true in
+def fooSomething [Add Nat] [Add Nat] : [Add Nat] → [Add Nat] → Bool := true
+
+end setOptionIn
+
+namespace universes
+
+/-! Test a projection that goes from `Type*` to `Sort*`. -/
+
+class A (α : Sort u) where
+
+class B (α : Type u) extends A α
+
+/--
+warning: Overlapping instance parameters in `_example`:
+
+⚠️ `[B α]` and `[A α]` can be used to infer conflicting versions of `[A α]`.
+💡️ Of these, `[A α]` may be removed.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+example (α : Type 4) [B α] [A α] : True := trivial
+
+end universes
+
+namespace parameters
+
+/-! Test a projection that changes the instance parameters. (This needs `eraseInstances`) -/
+
+class A (α : Type*) where
+class A' (α : Type*) extends A α where
+
+class B (α β : Type*) [A α] where
+class B' (α β : Type*) [A' α] extends B α β where
+
+instance {α} : A α where
+
+/--
+warning: Overlapping instance parameters in `_example`:
+
+⚠️ `[B α β]` and `[B' α β]` can be used to infer conflicting versions of `[B α β]`.
+💡️ Of these, `[B α β]` may be removed.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+example {α β} [B α β] [A' α] [B' α β] : True := trivial
+
+end parameters
+
+/-! Test a `where` clause. -/
+
+/--
+warning: Overlapping instance parameters in `List.lt'.go`:
+
+⚠️ There are 2 `[DecidableEq α]` instances; one is sufficient.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+def List.lt' {α} [DecidableEq α] (a b : List α) : Bool :=
+  go a b
+where
+  go [DecidableEq α] (_ _ : List α) : Bool := false
+
+-- Sadly, the linter does not work when the declaration doesn't have a body:
+
+class FooClass (α : Type) [Add α] [Add α] where
+
+/-! Test classes that extend a non-class -/
+
+structure NotAClass where
+class IsAClass1 extends NotAClass
+class IsAClass1' extends NotAClass
+class IsAClass2 extends IsAClass1
+
+example [IsAClass1] [IsAClass1'] : True := trivial
+
+/--
+warning: Overlapping instance parameters in `_example`:
+
+⚠️ `[IsAClass1]` and `[IsAClass2]` can be used to infer conflicting versions of `[IsAClass1]`.
+💡️ Of these, `[IsAClass1]` may be removed.
+
+When a data-carrying type class has multiple potential instances coming from different instance parameters, then these potential instances are incompatible. This is an example of an "instance diamond", which leads to unexpected unification failures.
+
+Delete or combine some of your instance parameters to avoid this.
+
+Note: This linter can be disabled with `set_option linter.overlappingInstances false`
+-/
+#guard_msgs in
+example [IsAClass1] [IsAClass2] : True := trivial
diff --git a/MathlibTest/Subsingleton.lean b/MathlibTest/Subsingleton.lean
index 6b5fd394eacca6..f139fe25b410b0 100644
--- a/MathlibTest/Subsingleton.lean
+++ b/MathlibTest/Subsingleton.lean
@@ -56,6 +56,7 @@ end AvoidSurprise
 /-!
 Handles `BEq` instances if there are `LawfulBEq` instances for each.
 -/
+set_option linter.overlappingInstances false in
 example (α : Type) (inst1 inst2 : BEq α) [@LawfulBEq α inst1] [@LawfulBEq α inst2] :
     inst1 = inst2 := by
   subsingleton
diff --git a/MathlibTest/Tactic/NormNum/Basic.lean b/MathlibTest/Tactic/NormNum/Basic.lean
index 9dcfce2cf50b70..e7ec5ae0f5bdc6 100644
--- a/MathlibTest/Tactic/NormNum/Basic.lean
+++ b/MathlibTest/Tactic/NormNum/Basic.lean
@@ -333,7 +333,7 @@ end LinearOrderedRing
 
 section Rat
 
-variable [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α]
+variable [Field α] [LinearOrder α] [IsStrictOrderedRing α]
 
 -- Normalize to True
 example : (1 : ℚ) ≤ 1 := by norm_num1
diff --git a/MathlibTest/Variable.lean b/MathlibTest/Variable.lean
index 3c921952a845aa..de4174b1179fc9 100644
--- a/MathlibTest/Variable.lean
+++ b/MathlibTest/Variable.lean
@@ -194,6 +194,8 @@ info: Try this:
 -/
 #guard_msgs in
 variable? [VectorSpace k V] [Algebra k V]
+
+set_option linter.overlappingInstances false
 example : Field k := inferInstance
 example : AddCommGroup V := inferInstance
 example : Module k V := inferInstance
diff --git a/MathlibTest/WhitespaceLinter.lean b/MathlibTest/WhitespaceLinter.lean
index d80cbd5576ee0a..664907eedb41e0 100644
--- a/MathlibTest/WhitespaceLinter.lean
+++ b/MathlibTest/WhitespaceLinter.lean
@@ -315,6 +315,7 @@ omit  [h : Add Nat]  [Add Nat]
 -- Include statements are not linted.
 include     h
 
+set_option linter.overlappingInstances false in
 /--
 warning: extra space in the source
 
diff --git a/MathlibTest/congr.lean b/MathlibTest/congr.lean
index 6059cfc331d35a..37a8d68ede7332 100644
--- a/MathlibTest/congr.lean
+++ b/MathlibTest/congr.lean
@@ -326,10 +326,12 @@ example {α} [AddCommMonoid α] [PartialOrder α] {a b c d e f g : α} :
 Lawful BEq instances are "subsingletons".
 -/
 
+set_option linter.overlappingInstances false in
 example (inst1 : BEq α) [LawfulBEq α] (inst2 : BEq α) [LawfulBEq α] (xs : List α) (x : α) :
     @List.erase _ inst1 xs x = @List.erase _ inst2 xs x := by
   congr!
 
+set_option linter.overlappingInstances false in
 /--
 error: unsolved goals
 case h.e'_2