perf: use declaration range internals in unused instances in type linters

[thorimur]

---

[github-actions]

PR summary 2d59066e04

Import changes exceeding 2%

%	File
+33.33%	Mathlib.Tactic.Linter.UnusedInstancesInType

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter.UnusedInstancesInType	3	4	+1 (+33.33%)

Import changes for all files

Files

Import difference

325 files Mathlib.Algebra.BigOperators.Group.List.Defs Mathlib.Algebra.Expr Mathlib.Algebra.Group.Commutator Mathlib.Algebra.Group.Defs Mathlib.Algebra.Group.Int.Defs Mathlib.Algebra.Group.Invertible.Defs Mathlib.Algebra.Group.MinimalAxioms Mathlib.Algebra.Group.Nat.Defs Mathlib.Algebra.Group.PUnit Mathlib.Algebra.GroupWithZero.Defs Mathlib.Algebra.GroupWithZero.Nat Mathlib.Algebra.GroupWithZero.Regular Mathlib.Algebra.HierarchyDesign Mathlib.Algebra.Notation.Defs Mathlib.Algebra.Notation.Lemmas Mathlib.Algebra.Notation.Pi.Defs Mathlib.Algebra.Notation Mathlib.Algebra.Order.Field.Defs Mathlib.Algebra.PEmptyInstances Mathlib.Algebra.Regular.Defs Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note Mathlib.CategoryTheory.Category.Init Mathlib.CategoryTheory.ConcreteCategory.Bundled Mathlib.Combinatorics.Matroid.Init Mathlib.Combinatorics.SimpleGraph.Init Mathlib.Control.Applicative Mathlib.Control.Basic Mathlib.Control.Combinators Mathlib.Control.Functor Mathlib.Control.Lawful Mathlib.Control.Traversable.Basic Mathlib.Control.Traversable.Lemmas Mathlib.Control.ULift Mathlib.Data.Array.Defs Mathlib.Data.Array.Extract Mathlib.Data.Bool.AllAny Mathlib.Data.Bracket Mathlib.Data.ENat.Defs Mathlib.Data.Finset.Attr Mathlib.Data.Int.Cast.Pi Mathlib.Data.Int.Init Mathlib.Data.Int.Notation Mathlib.Data.List.Defs Mathlib.Data.List.GetD Mathlib.Data.List.Indexes Mathlib.Data.List.Lookmap Mathlib.Data.List.Monad Mathlib.Data.List.SplitOn Mathlib.Data.Nat.BinaryRec Mathlib.Data.Nat.Bits Mathlib.Data.Nat.MaxPowDiv Mathlib.Data.Nat.Notation Mathlib.Data.Nat.NthRoot.Defs Mathlib.Data.Nat.Size Mathlib.Data.Num.Basic Mathlib.Data.Option.Defs Mathlib.Data.Option.NAry Mathlib.Data.Ordering.Basic Mathlib.Data.PNat.Notation Mathlib.Data.Prod.PProd Mathlib.Data.Rat.Init Mathlib.Data.SProd Mathlib.Data.Set.CoeSort Mathlib.Data.Set.Defs Mathlib.Data.Stream.Defs Mathlib.Data.String.Defs Mathlib.Data.String.Lemmas Mathlib.Data.Sym.Sym2.Init Mathlib.Data.Tree.Basic Mathlib.Data.Tree.Get Mathlib.Data.Tree.RBMap Mathlib.Data.Tree.Traversable Mathlib.Data.TwoPointing Mathlib.Deprecated.Aliases Mathlib.GroupTheory.EckmannHilton Mathlib.Init Mathlib.Lean.CoreM Mathlib.Lean.Elab.Tactic.Basic Mathlib.Lean.Elab.Term Mathlib.Lean.EnvExtension Mathlib.Lean.Exception Mathlib.Lean.Expr.ExtraRecognizers Mathlib.Lean.Expr.Rat Mathlib.Lean.Expr.ReplaceRec Mathlib.Lean.Expr Mathlib.Lean.FoldEnvironment Mathlib.Lean.GoalsLocation Mathlib.Lean.Json Mathlib.Lean.LocalContext Mathlib.Lean.MessageData.ForExprs Mathlib.Lean.MessageData.Trace Mathlib.Lean.Meta.Basic Mathlib.Lean.Meta.CongrTheorems Mathlib.Lean.Meta.DiscrTree Mathlib.Lean.Meta.KAbstractPositions Mathlib.Lean.Meta.RefinedDiscrTree.Basic Mathlib.Lean.Meta.RefinedDiscrTree.Encode Mathlib.Lean.Meta.RefinedDiscrTree.Initialize Mathlib.Lean.Meta.RefinedDiscrTree.Lookup Mathlib.Lean.Meta.RefinedDiscrTree Mathlib.Lean.Meta.Simp Mathlib.Lean.Meta.Tactic.Rewrite Mathlib.Lean.Meta Mathlib.Lean.Name Mathlib.Lean.PrettyPrinter.Delaborator Mathlib.Lean.Thunk Mathlib.Logic.Basic Mathlib.Logic.ExistsUnique Mathlib.Logic.Function.Coequalizer Mathlib.Logic.Function.CompTypeclasses Mathlib.Logic.Function.Defs Mathlib.Logic.Function.ULift Mathlib.Logic.IsEmpty.Defs Mathlib.Logic.Lemmas Mathlib.Logic.Nonempty Mathlib.Logic.Nontrivial.Defs Mathlib.Logic.OpClass Mathlib.Logic.Relator Mathlib.Order.Bounds.Defs Mathlib.Order.Notation Mathlib.Order.TypeTags Mathlib.Tactic.AdaptationNote Mathlib.Tactic.ApplyAt Mathlib.Tactic.ApplyCongr Mathlib.Tactic.ApplyWith Mathlib.Tactic.ArithMult.Init Mathlib.Tactic.ArithMult Mathlib.Tactic.Attr.Core Mathlib.Tactic.Attr.Register Mathlib.Tactic.Basic Mathlib.Tactic.Bound.Attribute Mathlib.Tactic.Bound.Init Mathlib.Tactic.ByCases Mathlib.Tactic.ByContra Mathlib.Tactic.CasesM Mathlib.Tactic.Cases Mathlib.Tactic.CategoryTheory.CategoryStar Mathlib.Tactic.CategoryTheory.Coherence.Datatypes Mathlib.Tactic.CategoryTheory.Coherence.Normalize Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence Mathlib.Tactic.Change Mathlib.Tactic.Check Mathlib.Tactic.Clean Mathlib.Tactic.ClearExcept Mathlib.Tactic.ClearExclamation Mathlib.Tactic.Clear_ Mathlib.Tactic.Coe Mathlib.Tactic.CongrExclamation Mathlib.Tactic.CongrM Mathlib.Tactic.Constructor Mathlib.Tactic.Continuity.Init Mathlib.Tactic.Continuity Mathlib.Tactic.ContinuousFunctionalCalculus Mathlib.Tactic.Contrapose Mathlib.Tactic.Conv Mathlib.Tactic.Convert Mathlib.Tactic.Core Mathlib.Tactic.DSimpPercent Mathlib.Tactic.DefEqAbuse Mathlib.Tactic.DefEqTransformations Mathlib.Tactic.DepRewrite Mathlib.Tactic.DeriveTraversable Mathlib.Tactic.Eqns Mathlib.Tactic.ErwQuestion Mathlib.Tactic.Eval Mathlib.Tactic.ExistsI Mathlib.Tactic.Explode.Datatypes Mathlib.Tactic.Explode.Pretty Mathlib.Tactic.Explode Mathlib.Tactic.Ext Mathlib.Tactic.ExtendDoc Mathlib.Tactic.FBinop Mathlib.Tactic.FailIfNoProgress Mathlib.Tactic.FastInstance Mathlib.Tactic.FieldSimp.Attr Mathlib.Tactic.FindSyntax Mathlib.Tactic.Find Mathlib.Tactic.Finiteness.Attr Mathlib.Tactic.FunProp.Attr Mathlib.Tactic.FunProp.Core Mathlib.Tactic.FunProp.Decl Mathlib.Tactic.FunProp.Elab Mathlib.Tactic.FunProp.FunctionData Mathlib.Tactic.FunProp.Mor Mathlib.Tactic.FunProp.Theorems Mathlib.Tactic.FunProp.ToBatteries Mathlib.Tactic.FunProp.Types Mathlib.Tactic.FunProp Mathlib.Tactic.GCongr.ForwardAttr Mathlib.Tactic.GeneralizeProofs Mathlib.Tactic.Generalize Mathlib.Tactic.GuardGoalNums Mathlib.Tactic.GuardHypNums Mathlib.Tactic.HaveI Mathlib.Tactic.Have Mathlib.Tactic.HigherOrder Mathlib.Tactic.Hint Mathlib.Tactic.ITauto Mathlib.Tactic.InferParam Mathlib.Tactic.Inhabit Mathlib.Tactic.IrreducibleDef Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm Mathlib.Tactic.Linter.CommandStart Mathlib.Tactic.Linter.DeprecatedModule Mathlib.Tactic.Linter.FindDeprecations Mathlib.Tactic.Linter.HaveLetLinter Mathlib.Tactic.Linter.PPRoundtrip Mathlib.Tactic.Linter.TextBased.UnicodeLinter Mathlib.Tactic.Linter.TextBased Mathlib.Tactic.Linter.UnusedInstancesInType Mathlib.Tactic.Linter.UpstreamableDecl Mathlib.Tactic.Linter.ValidatePRTitle Mathlib.Tactic.Linter Mathlib.Tactic.Measurability.Init Mathlib.Tactic.Measurability Mathlib.Tactic.Monotonicity.Attr Mathlib.Tactic.Monotonicity.Basic Mathlib.Tactic.NthRewrite Mathlib.Tactic.Observe Mathlib.Tactic.OfNat Mathlib.Tactic.Order.CollectFacts Mathlib.Tactic.Order.Graph.Basic Mathlib.Tactic.Order.Graph.Tarjan Mathlib.Tactic.Order.Preprocessing Mathlib.Tactic.Order.ToInt Mathlib.Tactic.Order Mathlib.Tactic.PPWithUniv Mathlib.Tactic.Polyrith Mathlib.Tactic.Propose Mathlib.Tactic.Push.Attr Mathlib.Tactic.Push Mathlib.Tactic.RSuffices Mathlib.Tactic.Recall Mathlib.Tactic.Recover Mathlib.Tactic.ReduceModChar.Ext Mathlib.Tactic.Relation.Rfl Mathlib.Tactic.Relation.Symm Mathlib.Tactic.RenameBVar Mathlib.Tactic.Rename Mathlib.Tactic.Replace Mathlib.Tactic.RewriteSearch Mathlib.Tactic.Sat.FromLRAT Mathlib.Tactic.Says Mathlib.Tactic.ScopedNS Mathlib.Tactic.SetLike Mathlib.Tactic.Set Mathlib.Tactic.SimpIntro Mathlib.Tactic.SimpRw Mathlib.Tactic.Simproc.Divisors Mathlib.Tactic.Simproc.ExistsAndEq Mathlib.Tactic.Simps.Basic Mathlib.Tactic.Simps.NotationClass Mathlib.Tactic.SplitIfs Mathlib.Tactic.Spread Mathlib.Tactic.StacksAttribute Mathlib.Tactic.Subsingleton Mathlib.Tactic.Substs Mathlib.Tactic.SuccessIfFailWithMsg Mathlib.Tactic.SudoSetOption Mathlib.Tactic.SuppressCompilation Mathlib.Tactic.SwapVar Mathlib.Tactic.TFAE Mathlib.Tactic.Tauto Mathlib.Tactic.TermCongr Mathlib.Tactic.ToAdditive Mathlib.Tactic.ToDual Mathlib.Tactic.ToExpr Mathlib.Tactic.ToFun Mathlib.Tactic.ToLevel Mathlib.Tactic.Trace Mathlib.Tactic.Translate.Attributes Mathlib.Tactic.Translate.Core Mathlib.Tactic.Translate.GuessName Mathlib.Tactic.Translate.Reorder Mathlib.Tactic.Translate.TagUnfoldBoundary Mathlib.Tactic.Translate.ToAdditive Mathlib.Tactic.Translate.ToDual Mathlib.Tactic.Translate.UnfoldBoundary Mathlib.Tactic.TryThis Mathlib.Tactic.TypeCheck Mathlib.Tactic.UnsetOption Mathlib.Tactic.Use Mathlib.Tactic.Variable Mathlib.Tactic.WLOG Mathlib.Tactic.Widget.Calc Mathlib.Tactic.Widget.CongrM Mathlib.Tactic.Widget.Conv Mathlib.Tactic.Widget.GCongr Mathlib.Tactic.Widget.InteractiveUnfold Mathlib.Tactic.Widget.LibraryRewrite Mathlib.Tactic.Widget.SelectInsertParamsClass Mathlib.Tactic.Widget.SelectPanelUtils Mathlib.Tactic.WithoutCDot Mathlib.Testing.Plausible.Testable Mathlib.Topology.Sheaves.Init Mathlib.Util.AddRelatedDecl Mathlib.Util.AssertNoSorry Mathlib.Util.AtLocation Mathlib.Util.AtomM.Recurse Mathlib.Util.AtomM Mathlib.Util.CompileInductive Mathlib.Util.CountHeartbeats Mathlib.Util.Delaborators Mathlib.Util.DischargerAsTactic Mathlib.Util.ElabWithoutMVars Mathlib.Util.Export Mathlib.Util.FormatTable Mathlib.Util.GetAllModules Mathlib.Util.LongNames Mathlib.Util.MemoFix Mathlib.Util.Notation3 Mathlib.Util.PPOptions Mathlib.Util.Qq Mathlib.Util.Simp Mathlib.Util.SleepHeartbeats Mathlib.Util.Superscript Mathlib.Util.SynthesizeUsing Mathlib.Util.Tactic Mathlib.Util.TermReduce Mathlib.Util.TransImports Mathlib.Util.WhatsNew Mathlib.Util.WithWeakNamespace

1

---

Declarations diff

+ fooUnfinished

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[thorimur]

!bench

[leanprover-radar]

Benchmark results for cb0f38e against 2d59066 are in. No significant results found. @thorimur

• ✅ build//instructions: -266.0G (-0.15%)

Small changes (2✅, 1🟥)

• 🟥 build/module/Batteries.Data.Bool//instructions: +18.3M (+1.73%)
• ✅ build/module/Mathlib.CategoryTheory.Limits.Lattice//instructions: -426.3M (-3.72%)
• ✅ build/profile/interpretation//wall-clock: -2m 54s (-1.75%)