[Merged by Bors] - feat: overlapping instances linter

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

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) :=

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

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

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`-

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`.

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 𝓐 𝓜

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/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

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

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

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

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. -/
 

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]

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

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

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}

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/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)

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₂) :

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) →

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) →

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]

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`,

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.

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

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 _⟩
 

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

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