[Merged by Bors] - perf: fast_instance% in Mathlib.Order.Basic

[kbuzzard]

This PR adds some fast_instance% to tidy up some instance terms. We get a speedup in Mathlib.Topology.Algebra.Valued.WithVal.

---

The genesis of this PR is #39780 (scattergun fast_instance%) which when benchmarked here #39780 (comment) didn't do much in general, but did save over 10% off
Mathlib.Topology.Algebra.Valued.WithVal. This PR reverse-engineers which change caused that speedup, and makes only that change. The change looks sensible to me.

[kbuzzard]

!radar

[leanprover-radar]

Benchmark results for 48f2583 against 383a355 are in. No significant results found. @kbuzzard

• ✅ build//instructions: -19.5G (-0.01%)

Medium changes (1✅)

• ✅ build/module/Mathlib.Topology.Algebra.Valued.WithVal//instructions: -11.6G (-12.48%)

[github-actions]

PR summary 48f25832fa

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Basic	114	115	+1 (+0.88%)

Import changes for all files

Files

Import difference

254 files Mathlib.Algebra.BigOperators.Group.List.Basic Mathlib.Algebra.BigOperators.Group.List.Lemmas Mathlib.Algebra.EuclideanDomain.Defs Mathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.FreeMonoid.FreeSemigroup Mathlib.Algebra.Group.Action.End Mathlib.Algebra.Group.Center Mathlib.Algebra.Group.Conj Mathlib.Algebra.Group.End Mathlib.Algebra.GroupWithZero.Action.Basic Mathlib.Algebra.GroupWithZero.Associated Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.GroupWithZero.Conj Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.AddTorsor Mathlib.Algebra.Order.BigOperators.Group.List 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.Action.Synonym 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.IsBotOne Mathlib.Algebra.Order.Module.Synonym Mathlib.Algebra.Order.Monoid.Associated Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.Order.Monoid.OrderDual 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.Ring.Unbundled.Rat 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.Prime.Lemmas Mathlib.Algebra.Ring.Centralizer Mathlib.Algebra.Tropical.Basic Mathlib.AlgebraicTopology.DoldKan.Compatibility Mathlib.CategoryTheory.Bicategory.End Mathlib.CategoryTheory.Bicategory.EqToHom Mathlib.CategoryTheory.Bicategory.Functor.Prelax Mathlib.CategoryTheory.Bicategory.LocallyDiscrete Mathlib.CategoryTheory.Bicategory.Opposites Mathlib.CategoryTheory.Bicategory.Strict.Basic Mathlib.CategoryTheory.CatCommSq Mathlib.CategoryTheory.Category.Preorder Mathlib.CategoryTheory.Category.ULift Mathlib.CategoryTheory.CommSq Mathlib.CategoryTheory.Comma.Arrow Mathlib.CategoryTheory.Comma.Basic Mathlib.CategoryTheory.Comma.CatCommSq Mathlib.CategoryTheory.ConcreteCategory.Basic Mathlib.CategoryTheory.DinatTrans Mathlib.CategoryTheory.Discrete.Basic Mathlib.CategoryTheory.Discrete.SumsProducts Mathlib.CategoryTheory.Elementwise Mathlib.CategoryTheory.EqToHom Mathlib.CategoryTheory.Equivalence Mathlib.CategoryTheory.EssentialImage Mathlib.CategoryTheory.FiberedCategory.BasedCategory Mathlib.CategoryTheory.FiberedCategory.Cartesian Mathlib.CategoryTheory.FiberedCategory.Cocartesian Mathlib.CategoryTheory.FiberedCategory.Fiber Mathlib.CategoryTheory.FiberedCategory.Fibered Mathlib.CategoryTheory.FiberedCategory.HasFibers Mathlib.CategoryTheory.FiberedCategory.HomLift Mathlib.CategoryTheory.Functor.Const Mathlib.CategoryTheory.Functor.CurryingThree Mathlib.CategoryTheory.Functor.Currying Mathlib.CategoryTheory.Functor.OfSequence Mathlib.CategoryTheory.Functor.TwoSquare Mathlib.CategoryTheory.Join.Basic Mathlib.CategoryTheory.Join.Opposites Mathlib.CategoryTheory.Join.Sum Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform Mathlib.CategoryTheory.Monoidal.Action.Basic Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor Mathlib.CategoryTheory.Monoidal.Category Mathlib.CategoryTheory.Monoidal.CoherenceLemmas Mathlib.CategoryTheory.ObjectProperty.Basic Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms Mathlib.CategoryTheory.ObjectProperty.Equivalence Mathlib.CategoryTheory.ObjectProperty.FullSubcategory Mathlib.CategoryTheory.Opposites Mathlib.CategoryTheory.PEmpty Mathlib.CategoryTheory.PUnit Mathlib.CategoryTheory.Pi.Basic Mathlib.CategoryTheory.Products.Associator Mathlib.CategoryTheory.Products.Basic Mathlib.CategoryTheory.Products.Bifunctor Mathlib.CategoryTheory.Products.Unitor Mathlib.CategoryTheory.Square Mathlib.CategoryTheory.Sums.Associator Mathlib.CategoryTheory.Sums.Basic Mathlib.CategoryTheory.Sums.Products Mathlib.Combinatorics.Quiver.Path.Decomposition Mathlib.Combinatorics.Quiver.Path.Vertices Mathlib.Computability.Tape Mathlib.Computability.TuringMachine.Tape Mathlib.Control.Fix Mathlib.Data.Bool.Set Mathlib.Data.Bundle Mathlib.Data.Fin.Basic Mathlib.Data.FunLike.Graded Mathlib.Data.Int.GCD Mathlib.Data.Int.LeastGreatest Mathlib.Data.Int.Range Mathlib.Data.List.Chain Mathlib.Data.List.Destutter Mathlib.Data.List.DropRight Mathlib.Data.List.Infix Mathlib.Data.List.Intervals Mathlib.Data.List.Iterate Mathlib.Data.List.Lex Mathlib.Data.List.MinMax Mathlib.Data.List.Permutation Mathlib.Data.List.Prime Mathlib.Data.List.Range Mathlib.Data.List.Rotate Mathlib.Data.List.SplitBy Mathlib.Data.List.SplitLengths Mathlib.Data.List.Sublists Mathlib.Data.List.TakeWhile Mathlib.Data.Multiset.AddSub Mathlib.Data.Multiset.Basic Mathlib.Data.Multiset.Count Mathlib.Data.Multiset.Defs Mathlib.Data.Multiset.Pairwise Mathlib.Data.Multiset.Replicate Mathlib.Data.Multiset.ZeroCons Mathlib.Data.Nat.Cast.Synonym Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.Nat.Choose.Basic Mathlib.Data.Nat.GCD.Prime Mathlib.Data.Nat.Log Mathlib.Data.Nat.Order.Lemmas Mathlib.Data.Nat.Prime.Defs 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.Part Mathlib.Data.Rat.Defs Mathlib.Data.Set.Basic Mathlib.Data.Set.Disjoint Mathlib.Data.Set.Enumerate Mathlib.Data.Set.Inclusion Mathlib.Data.Set.Insert Mathlib.Data.Set.Order Mathlib.Data.Set.Subsingleton Mathlib.Data.SetLike.Basic Mathlib.Data.Sigma.Order Mathlib.Data.String.Basic Mathlib.Data.Sum.Lattice Mathlib.Data.Sum.Order Mathlib.InformationTheory.Coding.UniquelyDecodable Mathlib.Logic.Function.FiberPartition 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.Circular Mathlib.Order.Comparable Mathlib.Order.Compare Mathlib.Order.Disjoint Mathlib.Order.GaloisConnection.Defs Mathlib.Order.Heyting.Basic Mathlib.Order.Heyting.Boundary 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.Lex Mathlib.Order.Max Mathlib.Order.MinMax Mathlib.Order.Monotone.Basic Mathlib.Order.Monotone.Defs Mathlib.Order.Monotone.Monovary Mathlib.Order.Nat Mathlib.Order.OrderDual Mathlib.Order.Part Mathlib.Order.PropInstances Mathlib.Order.RelClasses Mathlib.Order.RelIso.Basic Mathlib.Order.SetIsMax Mathlib.Order.SymmDiff Mathlib.Order.Synonym Mathlib.Order.Types.Defs Mathlib.Order.ULift Mathlib.Order.WithBotTop Mathlib.Order.WithBot Mathlib.SetTheory.Lists Mathlib.Tactic.ApplyFun Mathlib.Tactic.CategoryTheory.Elementwise Mathlib.Tactic.CategoryTheory.Monoidal.Basic Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes Mathlib.Tactic.CategoryTheory.Monoidal.Normalize Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence Mathlib.Tactic.CategoryTheory.MonoidalComp Mathlib.Tactic.Widget.StringDiagram Mathlib.Tactic.Zify

1

---

Declarations diff

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

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job