chore: move import of Simproc.ExistsAndEq

[JovanGerb]

This PR moves the import of Simproc.ExistsAndEq to the more appropriate Mathlib.Tactic.Common. This reduces the longest pole.

---

[github-actions]

PR summary a2306eca72

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Basic	58	54	-4 (-6.90%)

Import changes for all files

Files	Import difference
267 files Mathlib.Algebra.AddTorsor.Defs Mathlib.Algebra.BigOperators.Group.List.Defs Mathlib.Algebra.CharZero.Defs Mathlib.Algebra.Field.Defs Mathlib.Algebra.Field.MinimalAxioms Mathlib.Algebra.Free Mathlib.Algebra.Group.Action.Basic Mathlib.Algebra.Group.Action.Defs Mathlib.Algebra.Group.Action.Faithful Mathlib.Algebra.Group.Action.Hom Mathlib.Algebra.Group.Action.Opposite Mathlib.Algebra.Group.Action.Option Mathlib.Algebra.Group.Action.Pretransitive Mathlib.Algebra.Group.Action.Prod Mathlib.Algebra.Group.Action.Sigma Mathlib.Algebra.Group.Action.Sum Mathlib.Algebra.Group.Action.TypeTags Mathlib.Algebra.Group.Action.Units Mathlib.Algebra.Group.Basic Mathlib.Algebra.Group.Commutator Mathlib.Algebra.Group.Commute.Basic Mathlib.Algebra.Group.Commute.Defs Mathlib.Algebra.Group.Commute.Hom Mathlib.Algebra.Group.Commute.Units Mathlib.Algebra.Group.Defs Mathlib.Algebra.Group.Embedding Mathlib.Algebra.Group.Equiv.Basic Mathlib.Algebra.Group.Equiv.Defs Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Equiv.TypeTags Mathlib.Algebra.Group.Ext Mathlib.Algebra.Group.Hom.Basic Mathlib.Algebra.Group.Hom.CompTypeclasses Mathlib.Algebra.Group.Hom.Defs Mathlib.Algebra.Group.Hom.End Mathlib.Algebra.Group.Hom.Instances Mathlib.Algebra.Group.Idempotent Mathlib.Algebra.Group.InjSurj Mathlib.Algebra.Group.Int.Defs Mathlib.Algebra.Group.Int.TypeTags Mathlib.Algebra.Group.Int.Units Mathlib.Algebra.Group.Invertible.Basic Mathlib.Algebra.Group.Invertible.Defs Mathlib.Algebra.Group.Irreducible.Defs Mathlib.Algebra.Group.MinimalAxioms Mathlib.Algebra.Group.ModEq Mathlib.Algebra.Group.Nat.Defs Mathlib.Algebra.Group.Nat.Hom Mathlib.Algebra.Group.Nat.TypeTags Mathlib.Algebra.Group.Nat.Units Mathlib.Algebra.Group.Opposite Mathlib.Algebra.Group.PUnit Mathlib.Algebra.Group.Pi.Basic Mathlib.Algebra.Group.Pi.Units Mathlib.Algebra.Group.Prod Mathlib.Algebra.Group.Semiconj.Basic Mathlib.Algebra.Group.Semiconj.Defs Mathlib.Algebra.Group.Semiconj.Units Mathlib.Algebra.Group.Torsion Mathlib.Algebra.Group.TypeTags.Basic Mathlib.Algebra.Group.TypeTags.Hom Mathlib.Algebra.Group.ULift Mathlib.Algebra.Group.Units.Basic Mathlib.Algebra.Group.Units.Defs Mathlib.Algebra.Group.Units.Equiv Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.Group.Units.Opposite Mathlib.Algebra.GroupWithZero.Action.Defs Mathlib.Algebra.GroupWithZero.Action.End Mathlib.Algebra.GroupWithZero.Action.Faithful Mathlib.Algebra.GroupWithZero.Action.Hom Mathlib.Algebra.GroupWithZero.Action.Opposite Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.Basic Mathlib.Algebra.GroupWithZero.Commute Mathlib.Algebra.GroupWithZero.Defs Mathlib.Algebra.GroupWithZero.Equiv Mathlib.Algebra.GroupWithZero.Hom Mathlib.Algebra.GroupWithZero.Idempotent Mathlib.Algebra.GroupWithZero.InjSurj Mathlib.Algebra.GroupWithZero.Invertible Mathlib.Algebra.GroupWithZero.Nat Mathlib.Algebra.GroupWithZero.NeZero Mathlib.Algebra.GroupWithZero.Opposite Mathlib.Algebra.GroupWithZero.Pi Mathlib.Algebra.GroupWithZero.Regular Mathlib.Algebra.GroupWithZero.Semiconj Mathlib.Algebra.GroupWithZero.ULift Mathlib.Algebra.GroupWithZero.Units.Basic Mathlib.Algebra.GroupWithZero.Units.Equiv Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.HierarchyDesign Mathlib.Algebra.Homology.ComplexShape Mathlib.Algebra.Homology.Embedding.Basic Mathlib.Algebra.Homology.HasNoLoop Mathlib.Algebra.Module.Defs Mathlib.Algebra.Module.MinimalAxioms Mathlib.Algebra.Module.Prod Mathlib.Algebra.NeZero Mathlib.Algebra.Notation.Defs Mathlib.Algebra.Notation.Lemmas Mathlib.Algebra.Notation.Pi.Basic Mathlib.Algebra.Notation.Pi.Defs Mathlib.Algebra.Notation.Prod Mathlib.Algebra.Notation Mathlib.Algebra.Opposites Mathlib.Algebra.Order.Field.Defs Mathlib.Algebra.PEmptyInstances Mathlib.Algebra.Regular.Basic Mathlib.Algebra.Regular.Defs Mathlib.Algebra.Regular.Opposite Mathlib.Algebra.Regular.Pi Mathlib.Algebra.Regular.Prod Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Regular.ULift Mathlib.Algebra.Ring.Action.Rat Mathlib.Algebra.Ring.Defs Mathlib.Algebra.Ring.Ext Mathlib.Algebra.Ring.GrindInstances Mathlib.Algebra.Ring.Hom.InjSurj Mathlib.Algebra.Ring.InjSurj Mathlib.Algebra.Ring.Int.Defs Mathlib.Algebra.Ring.Invertible Mathlib.Algebra.Ring.MinimalAxioms Mathlib.Algebra.Ring.Nat Mathlib.Algebra.Ring.PUnit Mathlib.Algebra.Ring.Regular Mathlib.Algebra.Ring.Semiconj Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note Mathlib.Combinatorics.Quiver.Basic Mathlib.Combinatorics.Quiver.Cast Mathlib.Combinatorics.Quiver.Path Mathlib.Combinatorics.Quiver.Prefunctor Mathlib.Combinatorics.Quiver.Push Mathlib.Combinatorics.Quiver.SingleObj Mathlib.Combinatorics.Quiver.Symmetric Mathlib.Control.Applicative Mathlib.Control.EquivFunctor Mathlib.Control.Lawful Mathlib.Control.Monad.Basic Mathlib.Control.Monad.Cont Mathlib.Control.Monad.Writer Mathlib.Control.Traversable.Equiv Mathlib.Control.Traversable.Lemmas Mathlib.Data.Bool.Basic Mathlib.Data.Char Mathlib.Data.Countable.Defs Mathlib.Data.Erased Mathlib.Data.Finite.Defs Mathlib.Data.FunLike.Basic Mathlib.Data.FunLike.Embedding Mathlib.Data.FunLike.Equiv Mathlib.Data.Int.Basic Mathlib.Data.Int.Cast.Basic Mathlib.Data.Int.Cast.Defs Mathlib.Data.Int.Cast.Field Mathlib.Data.Int.Cast.Prod Mathlib.Data.Int.NatAbs Mathlib.Data.Int.Order.Basic Mathlib.Data.List.Flatten Mathlib.Data.List.GetD Mathlib.Data.List.Pairwise Mathlib.Data.Matrix.DMatrix Mathlib.Data.Nat.Basic Mathlib.Data.Nat.Bits Mathlib.Data.Nat.Cast.Defs Mathlib.Data.Nat.Cast.NeZero Mathlib.Data.Nat.Cast.Prod Mathlib.Data.Nat.Find Mathlib.Data.Nat.Init Mathlib.Data.Nat.PSub Mathlib.Data.Nat.Size Mathlib.Data.Nat.Sqrt Mathlib.Data.Opposite Mathlib.Data.Option.Basic Mathlib.Data.Ordering.Lemmas Mathlib.Data.Prod.Basic Mathlib.Data.Quot Mathlib.Data.Sigma.Basic Mathlib.Data.Sigma.Lex Mathlib.Data.String.Lemmas Mathlib.Data.Subtype Mathlib.Data.Sum.Basic Mathlib.Data.Tree.Traversable Mathlib.Data.TwoPointing Mathlib.Data.ULift Mathlib.Deprecated.Order Mathlib.GroupTheory.EckmannHilton Mathlib.GroupTheory.GroupAction.IterateAct Mathlib.GroupTheory.GroupAction.Ring Mathlib.Lean.Meta.CongrTheorems Mathlib.LinearAlgebra.AffineSpace.Defs Mathlib.Logic.Basic Mathlib.Logic.Embedding.Basic Mathlib.Logic.Equiv.Basic Mathlib.Logic.Equiv.Bool Mathlib.Logic.Equiv.Defs Mathlib.Logic.Equiv.Option Mathlib.Logic.Equiv.Pairwise Mathlib.Logic.Equiv.Prod Mathlib.Logic.Equiv.Sum Mathlib.Logic.Function.Basic Mathlib.Logic.Function.Conjugate Mathlib.Logic.Function.Iterate Mathlib.Logic.IsEmpty Mathlib.Logic.Lemmas Mathlib.Logic.Nontrivial.Basic Mathlib.Logic.Pairwise Mathlib.Logic.Relation Mathlib.Logic.Small.Defs Mathlib.Logic.Unique Mathlib.Logic.UnivLE Mathlib.Order.Bounds.Defs Mathlib.Order.Defs.LinearOrder Mathlib.Order.Defs.PartialOrder Mathlib.Order.Defs.Unbundled Mathlib.Order.Interval.Set.Defs Mathlib.RingTheory.LocalRing.Defs Mathlib.SetTheory.Cardinal.Defs Mathlib.SetTheory.PGame.Basic Mathlib.Tactic.ArithMult Mathlib.Tactic.Basic Mathlib.Tactic.ByCases Mathlib.Tactic.ByContra Mathlib.Tactic.Choose Mathlib.Tactic.CongrExclamation Mathlib.Tactic.CongrM Mathlib.Tactic.Contrapose Mathlib.Tactic.Convert Mathlib.Tactic.DefEqTransformations Mathlib.Tactic.DeriveFintype Mathlib.Tactic.DeriveTraversable Mathlib.Tactic.Ext Mathlib.Tactic.GCongr.CoreAttrs Mathlib.Tactic.GCongr.Core Mathlib.Tactic.GCongr Mathlib.Tactic.GRewrite.Core Mathlib.Tactic.GRewrite.Elab Mathlib.Tactic.GRewrite Mathlib.Tactic.Hint Mathlib.Tactic.IrreducibleDef Mathlib.Tactic.Lift Mathlib.Tactic.MoveAdd Mathlib.Tactic.NormNum.Result Mathlib.Tactic.ProdAssoc Mathlib.Tactic.ProxyType Mathlib.Tactic.Push Mathlib.Tactic.RSuffices Mathlib.Tactic.Sat.FromLRAT Mathlib.Tactic.Says Mathlib.Tactic.SetLike Mathlib.Tactic.Simps.Basic Mathlib.Tactic.Subsingleton Mathlib.Tactic.TermCongr Mathlib.Tactic.ToAdditive Mathlib.Tactic.ToDual Mathlib.Tactic.ToFun Mathlib.Tactic.Translate.Core Mathlib.Tactic.Translate.TagUnfoldBoundary Mathlib.Tactic.Translate.ToAdditive Mathlib.Tactic.Translate.ToDual Mathlib.Tactic.WLOG Mathlib.Tactic.Widget.CongrM Mathlib.Tactic.Widget.GCongr Mathlib.Testing.Plausible.Sampleable Mathlib.Testing.Plausible.Testable	-4
153 files Mathlib.Algebra.EuclideanDomain.Defs Mathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.Group.Center Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.Irreducible.Lemmas Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Subsemigroup.Defs Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.AddTorsor Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Action.End Mathlib.Algebra.Order.Group.Action.Synonym Mathlib.Algebra.Order.Group.Basic Mathlib.Algebra.Order.Group.Defs Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Order.Group.End Mathlib.Algebra.Order.Group.Equiv Mathlib.Algebra.Order.Group.Int Mathlib.Algebra.Order.Group.Lattice Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Synonym Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.Group.Units Mathlib.Algebra.Order.GroupWithZero.Synonym Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs Mathlib.Algebra.Order.Hom.Basic Mathlib.Algebra.Order.Hom.Monoid Mathlib.Algebra.Order.Hom.TypeTags Mathlib.Algebra.Order.Hom.Units Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.Lex Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Units Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Order.Monoid.Units Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Ring.Idempotent Mathlib.Algebra.Order.Ring.Synonym Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Sub.Defs Mathlib.Algebra.Order.Sub.Prod Mathlib.Algebra.Order.Sub.Unbundled.Basic Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Order.Sum Mathlib.Algebra.Order.ZeroLEOne Mathlib.Algebra.Ring.Centralizer Mathlib.Algebra.Ring.Idempotent Mathlib.Algebra.Tropical.Basic Mathlib.Combinatorics.Quiver.ConnectedComponent Mathlib.Combinatorics.Quiver.Path.Decomposition Mathlib.Combinatorics.Quiver.Subquiver Mathlib.Data.Bundle Mathlib.Data.ENat.Defs Mathlib.Data.Int.LeastGreatest Mathlib.Data.Int.Range Mathlib.Data.List.Iterate Mathlib.Data.List.SplitLengths Mathlib.Data.List.TakeWhile Mathlib.Data.Nat.Cast.Synonym Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.Nat.Log Mathlib.Data.Nat.Order.Lemmas Mathlib.Data.Nat.Upto Mathlib.Data.Nat.WithBot Mathlib.Data.Ordmap.Ordnode Mathlib.Data.PEquiv Mathlib.Data.PNat.Defs Mathlib.Data.PNat.Equiv Mathlib.Data.PSigma.Order Mathlib.Data.Prod.Lex Mathlib.Data.Set.Basic Mathlib.Data.Set.Disjoint Mathlib.Data.Set.Inclusion Mathlib.Data.Set.Notation Mathlib.Data.Set.Operations Mathlib.Data.Set.Opposite Mathlib.Data.Set.Order Mathlib.Data.SetLike.Basic Mathlib.Data.Sigma.Order Mathlib.Data.Sum.Lattice Mathlib.Data.Sum.Order Mathlib.Deprecated.Estimator Mathlib.GroupTheory.Subsemigroup.Center Mathlib.Order.Antisymmetrization Mathlib.Order.Basic Mathlib.Order.BooleanAlgebra.Basic Mathlib.Order.BooleanAlgebra.Defs Mathlib.Order.Booleanisation Mathlib.Order.BoundedOrder.Basic Mathlib.Order.BoundedOrder.Lattice Mathlib.Order.BoundedOrder.Monotone Mathlib.Order.Comparable Mathlib.Order.Compare Mathlib.Order.Disjoint Mathlib.Order.GaloisConnection.Defs Mathlib.Order.Heyting.Basic Mathlib.Order.Heyting.Hom Mathlib.Order.Hom.Basic Mathlib.Order.Hom.BoundedLattice Mathlib.Order.Hom.Bounded Mathlib.Order.Hom.Lattice Mathlib.Order.Hom.WithTopBot Mathlib.Order.Iterate Mathlib.Order.Lattice Mathlib.Order.Max Mathlib.Order.MinMax Mathlib.Order.Monotone.Basic Mathlib.Order.Monotone.Defs Mathlib.Order.Monotone.Monovary Mathlib.Order.Nat Mathlib.Order.Notation Mathlib.Order.OrderDual Mathlib.Order.Prod.Lex.Hom Mathlib.Order.PropInstances Mathlib.Order.RelClasses Mathlib.Order.RelIso.Basic Mathlib.Order.SetIsMax Mathlib.Order.SetNotation Mathlib.Order.SymmDiff Mathlib.Order.Synonym Mathlib.Order.TypeTags Mathlib.Order.Types.Defs Mathlib.Order.ULift Mathlib.Order.WithBotTop Mathlib.Order.WithBot Mathlib.SetTheory.Lists Mathlib.Tactic.ApplyFun Mathlib.Tactic.NormNum.Core Mathlib.Tactic.NormNum.Parity Mathlib.Tactic.Zify Mathlib.Topology.ContinuousMap.Defs Mathlib.Topology.Defs.Basic	-3
19 files Mathlib.Algebra.Field.Basic Mathlib.Algebra.Field.ModEq Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.RingHom Mathlib.Algebra.Order.Sub.Unbundled.Hom Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.Basic Mathlib.Algebra.Ring.Commute Mathlib.Algebra.Ring.Hom.Defs Mathlib.Algebra.Ring.Int.Units Mathlib.Algebra.Ring.Opposite Mathlib.Algebra.Ring.Torsion Mathlib.Algebra.Ring.Units Mathlib.Data.Nat.Cast.Commute Mathlib.GroupTheory.GroupAction.Hom Mathlib.Order.Circular Mathlib.Tactic.Order	-2

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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

[Komyyy]

Thank you for your contribution!

The longest pole can be checked in the rader result, as lakeprof/longest.

!bench

[Komyyy]

@JovanGerb Can you run bench?

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 0358a17 against 4071ce7 are in! @JovanGerb

• ✅ build//instructions: -33.3G (-0.02%)

Small changes (1✅)

• ✅ build/module/Mathlib.Tactic.Nontriviality//instructions: -149.8M (-4.00%)

[Komyyy]

Metric	Submetric	Value	Delta	Detla%	Unit	Source
build/lakeprof/longest build path	wall-clock	9m 50s	-6s	-1.0%	s	runner-mathlib1
build/lakeprof/longest rebuild path	wall-clock	9m 50s	-529ms	-0.1%	s	runner-mathlib1

Great! Thank you!

[grunweg]

Thanks for doing this! Can you add a comment to Tactic/Basic or perhaps an assert_not_exists with a comment, that this is intentional to keep the critical build path short? I'll ask for another pair of eyes just to be sure, but this looks uncontroversial to me.
maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[JovanGerb]

I think the file docstring of Tactic.Basic is very clear already: "This file defines some basic utilities for tactic writing", which means that it shouldn't import specific tactics or simprocs. So it was an oversight in the review process that we missed this.

I get that you want to have an automatic way to avoid this happening in the future, but an assert_not_exists just for this one simproc seems too specific. If you want, you could try to do something with the directory dependency linter instead.

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for a345596 against a2306ec are in! @JovanGerb

• 🟥 build//instructions: +8.5G (+0.00%)

Small changes (1🟥)

• 🟥 build/module/Mathlib.Data.Rat.Encodable//instructions: +247.4M (+5.28%)