[Merged by Bors] - chore: bump to nightly-2023-04-11

[gebner]

---

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit 164e60f.
The entire run failed.
Found no significant differences.

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit a72c1ab.
There were significant changes against commit cd7f2d5:

  Benchmark                                                 Metric         Change
  ===============================================================================
- build                                                     linting          5.5%
- ~Mathlib.Algebra.AddTorsor                                instructions     5.9%
+ ~Mathlib.Algebra.Algebra.Equiv                            instructions   -11.9%
+ ~Mathlib.Algebra.Algebra.Hom                              instructions   -16.1%
+ ~Mathlib.Algebra.Algebra.RestrictScalars                  instructions    -6.4%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Basic                 instructions   -12.0%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Tower                 instructions   -13.9%
- ~Mathlib.Algebra.Associated                               instructions     6.7%
+ ~Mathlib.Algebra.CharP.Algebra                            instructions   -13.9%
+ ~Mathlib.Algebra.CharP.Basic                              instructions   -26.6%
+ ~Mathlib.Algebra.CharP.Pi                                 instructions   -11.5%
+ ~Mathlib.Algebra.CharP.Subring                            instructions   -10.9%
- ~Mathlib.Algebra.Divisibility.Basic                       instructions     5.7%
+ ~Mathlib.Algebra.FreeAlgebra                              instructions   -20.8%
- ~Mathlib.Algebra.GroupPower.Basic                         instructions     8.6%
- ~Mathlib.Algebra.GroupPower.Lemmas                        instructions     7.4%
- ~Mathlib.Algebra.GroupPower.Order                         instructions     7.4%
- ~Mathlib.Algebra.GroupPower.Ring                          instructions     9.0%
- ~Mathlib.Algebra.GroupWithZero.Power                      instructions     9.1%
- ~Mathlib.Algebra.Hom.GroupAction                          instructions     6.5%
- ~Mathlib.Algebra.Hom.Iterate                              instructions     7.3%
- ~Mathlib.Algebra.Hom.NonUnitalAlg                         instructions     6.1%
- ~Mathlib.Algebra.Invertible                               instructions     6.1%
+ ~Mathlib.Algebra.IsPrimePow                               instructions    -6.2%
- ~Mathlib.Algebra.Module.Basic                             instructions     6.5%
- ~Mathlib.Algebra.Module.Equiv                             instructions     5.9%
- ~Mathlib.Algebra.Module.Hom                               instructions     6.2%
- ~Mathlib.Algebra.Module.LinearMap                         instructions     6.8%
- ~Mathlib.Algebra.Module.Submodule.Basic                   instructions     5.2%
- ~Mathlib.Algebra.Module.Submodule.Bilinear                instructions     5.7%
- ~Mathlib.Algebra.Module.Submodule.Lattice                 instructions     5.5%
- ~Mathlib.Algebra.Module.Submodule.Pointwise               instructions     6.5%
- ~Mathlib.Algebra.MonoidAlgebra.Degree                     instructions     7.1%
- ~Mathlib.Algebra.Order.Field.Power                        instructions     5.3%
- ~Mathlib.Algebra.Order.Hom.Basic                          instructions    10.7%
- ~Mathlib.Algebra.Order.Ring.WithTop                       instructions     6.0%
- ~Mathlib.Algebra.Order.SMul                               instructions     5.6%
- ~Mathlib.Algebra.Order.Sub.Basic                          instructions     8.0%
- ~Mathlib.Algebra.Order.Sub.Canonical                      instructions     5.3%
- ~Mathlib.Algebra.Parity                                   instructions     5.4%
- ~Mathlib.Algebra.Periodic                                 instructions     5.7%
- ~Mathlib.Algebra.Regular.Pow                              instructions     5.3%
- ~Mathlib.Algebra.Ring.Basic                               instructions     6.9%
+ ~Mathlib.Algebra.Squarefree                               instructions    -5.2%
+ ~Mathlib.Algebra.Star.Free                                instructions    -5.2%
+ ~Mathlib.Algebra.Star.StarAlgHom                          instructions    -9.3%
+ ~Mathlib.Algebra.Star.Subalgebra                          instructions    -7.1%
- ~Mathlib.Algebra.Star.Unitary                             instructions     5.0%
+ ~Mathlib.Analysis.Normed.Field.Basic                      instructions   -10.7%
+ ~Mathlib.Analysis.Normed.Field.UnitBall                   instructions   -12.7%
+ ~Mathlib.Analysis.Normed.Group.Basic                      instructions    -9.3%
+ ~Mathlib.Analysis.Normed.Group.Hom                        instructions    -5.2%
+ ~Mathlib.Analysis.Normed.Order.Lattice                    instructions    -8.0%
+ ~Mathlib.Analysis.NormedSpace.Int                         instructions   -12.3%
- ~Mathlib.CategoryTheory.Closed.Monoidal                   instructions     5.1%
- ~Mathlib.CategoryTheory.Monad.Basic                       instructions     5.3%
- ~Mathlib.Combinatorics.HalesJewett                        instructions     6.6%
+ ~Mathlib.Computability.Language                           instructions   -14.7%
- ~Mathlib.Data.Dfinsupp.Order                              instructions     5.2%
+ ~Mathlib.Data.Finsupp.Multiset                            instructions   -10.6%
+ ~Mathlib.Data.MvPolynomial.Basic                          instructions   -20.8%
+ ~Mathlib.Data.MvPolynomial.Comap                          instructions   -15.0%
+ ~Mathlib.Data.MvPolynomial.CommRing                       instructions    -8.1%
+ ~Mathlib.Data.MvPolynomial.Counit                         instructions   -27.3%
+ ~Mathlib.Data.MvPolynomial.Equiv                          instructions    -8.8%
+ ~Mathlib.Data.MvPolynomial.Invertible                     instructions    -6.6%
+ ~Mathlib.Data.MvPolynomial.Rename                         instructions   -15.2%
+ ~Mathlib.Data.MvPolynomial.Variables                      instructions   -20.8%
- ~Mathlib.Data.Nat.Cast.Basic                              instructions     6.7%
+ ~Mathlib.Data.Nat.Choose.Sum                              instructions    -5.5%
+ ~Mathlib.Data.Polynomial.AlgebraMap                       instructions   -29.5%
+ ~Mathlib.Data.Polynomial.Basic                            instructions    -8.9%
+ ~Mathlib.Data.Polynomial.CancelLeads                      instructions    -5.5%
+ ~Mathlib.Data.Polynomial.Coeff                            instructions    -8.2%
+ ~Mathlib.Data.Polynomial.Degree.Definitions               instructions   -16.8%
+ ~Mathlib.Data.Polynomial.Degree.Lemmas                    instructions   -11.4%
+ ~Mathlib.Data.Polynomial.Div                              instructions   -13.2%
+ ~Mathlib.Data.Polynomial.EraseLead                        instructions   -14.1%
+ ~Mathlib.Data.Polynomial.Eval                             instructions    -6.5%
+ ~Mathlib.Data.Polynomial.Induction                        instructions   -11.9%
+ ~Mathlib.Data.Polynomial.Inductions                       instructions    -7.9%
+ ~Mathlib.Data.Polynomial.IntegralNormalization            instructions   -11.2%
+ ~Mathlib.Data.Polynomial.Lifts                            instructions   -11.7%
+ ~Mathlib.Data.Polynomial.Monic                            instructions    -7.5%
+ ~Mathlib.Data.Polynomial.Monomial                         instructions   -13.5%
+ ~Mathlib.Data.Polynomial.Reverse                          instructions    -9.9%
+ ~Mathlib.Data.Polynomial.RingDivision                     instructions   -20.6%
+ ~Mathlib.Data.Polynomial.Taylor                           instructions   -16.8%
- ~Mathlib.Data.Real.Basic                                  instructions     5.6%
- ~Mathlib.Data.Set.Intervals.Group                         instructions     5.6%
- ~Mathlib.Data.Set.Pointwise.Finite                        instructions     5.1%
+ ~Mathlib.Data.Set.Semiring                                instructions    -7.2%
+ ~Mathlib.Data.ZMod.Algebra                                instructions   -10.7%
+ ~Mathlib.Data.ZMod.Basic                                  instructions   -15.1%
+ ~Mathlib.FieldTheory.PerfectClosure                       instructions   -23.3%
- ~Mathlib.GroupTheory.GroupAction.Group                    instructions     7.0%
- ~Mathlib.GroupTheory.GroupAction.SubMulAction             instructions     6.9%
- ~Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise   instructions     6.0%
- ~Mathlib.GroupTheory.GroupAction.Units                    instructions     6.0%
- ~Mathlib.GroupTheory.Perm.Basic                           instructions     5.0%
- ~Mathlib.GroupTheory.Perm.Support                         instructions     5.8%
- ~Mathlib.GroupTheory.SemidirectProduct                    instructions     6.2%
- ~Mathlib.GroupTheory.Subgroup.Actions                     instructions     5.6%
- ~Mathlib.GroupTheory.Subgroup.Pointwise                   instructions     5.1%
- ~Mathlib.LinearAlgebra.AffineSpace.AffineMap              instructions     9.7%
- ~Mathlib.LinearAlgebra.AffineSpace.Midpoint               instructions     5.4%
- ~Mathlib.LinearAlgebra.BilinearMap                        instructions     5.1%
+ ~Mathlib.MeasureTheory.MeasurableSpace                    instructions   -26.0%
+ ~Mathlib.NumberTheory.Padics.PadicVal                     instructions    -7.1%
+ ~Mathlib.NumberTheory.Primorial                           instructions   -10.4%
- ~Mathlib.Order.Filter.Prod                                instructions     6.7%
- ~Mathlib.Order.Heyting.Hom                                instructions     6.1%
+ ~Mathlib.RingTheory.Adjoin.Basic                          instructions    -8.5%
- ~Mathlib.RingTheory.Coprime.Basic                         instructions     5.6%
+ ~Mathlib.RingTheory.Ideal.Operations                      instructions    -6.0%
+ ~Mathlib.RingTheory.Int.Basic                             instructions    -9.4%
+ ~Mathlib.RingTheory.Localization.NumDen                   instructions   -11.9%
+ ~Mathlib.RingTheory.Multiplicity                          instructions   -26.9%
+ ~Mathlib.RingTheory.MvPolynomial.Symmetric                instructions    -7.5%
+ ~Mathlib.RingTheory.MvPolynomial.Tower                    instructions   -21.0%
+ ~Mathlib.RingTheory.Nilpotent                             instructions   -18.8%
+ ~Mathlib.RingTheory.Polynomial.Content                    instructions   -12.6%
+ ~Mathlib.RingTheory.Polynomial.Opposites                  instructions   -16.2%
+ ~Mathlib.RingTheory.Polynomial.ScaleRoots                 instructions   -17.0%
+ ~Mathlib.RingTheory.Polynomial.Tower                      instructions   -24.5%
- ~Mathlib.RingTheory.Subring.Pointwise                     instructions     5.4%
- ~Mathlib.RingTheory.Subsemiring.Pointwise                 instructions     6.4%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain             instructions   -17.7%
+ ~Mathlib.RingTheory.Valuation.Basic                       instructions   -34.5%
+ ~Mathlib.RingTheory.Valuation.Integers                    instructions   -33.8%
- ~Mathlib.Topology.Algebra.ConstMulAction                  instructions     5.9%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.Basic            instructions   -19.0%
+ ~Mathlib.Topology.Algebra.OpenSubgroup                    instructions   -15.5%
+ ~Mathlib.Topology.Algebra.Ring.Ideal                      instructions    -6.0%
+ ~Mathlib.Topology.Algebra.UniformGroup                    instructions    -6.5%
- ~Mathlib.Topology.Bornology.Constructions                 instructions     5.7%
- ~Mathlib.Topology.Constructions                           instructions     5.8%
+ ~Mathlib.Topology.Covering                                instructions   -14.6%
+ ~Mathlib.Topology.FiberBundle.Basic                       instructions   -21.3%
+ ~Mathlib.Topology.FiberBundle.Trivialization              instructions   -30.0%
+ ~Mathlib.Topology.Instances.Real                          instructions    -5.2%
+ ~Mathlib.Topology.MetricSpace.Antilipschitz               instructions    -5.6%
- ~Mathlib.Topology.MetricSpace.IsometricSMul               instructions     5.8%
+ ~Mathlib.Topology.MetricSpace.Isometry                    instructions   -18.8%
+ ~Mathlib.Topology.MetricSpace.Lipschitz                   instructions    -5.7%
- ~Mathlib.Topology.Paracompact                             instructions     7.5%
+ ~Mathlib.Topology.PathConnected                           instructions    -6.5%
+ ~Mathlib.Topology.Semicontinuous                          instructions   -10.1%
+ ~Mathlib.Topology.Sequences                               instructions   -10.0%
+ ~Mathlib.Topology.Sets.Compacts                           instructions   -23.5%
- ~Qq.AssertInstancesCommute                                instructions    11.1%

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit fd79213.
There were significant changes against commit cd7f2d5:

  Benchmark                           Metric         Change
  =========================================================
- ~Mathlib.Algebra.GroupPower.Basic   instructions     5.1%
- ~Mathlib.Algebra.Order.Hom.Basic    instructions     7.3%
- ~Mathlib.Data.Real.Basic            instructions     6.1%
- ~Mathlib.Order.Heyting.Hom          instructions     5.3%
- ~Qq.AssertInstancesCommute          instructions    10.6%

[semorrison]

!bench

[leanprover-bot]

Here are the benchmark results for commit 15b289c.
There were significant changes against commit c5372bb:

  Benchmark                                    Metric         Change
  ==================================================================
+ build                                        linting         -6.2%
- ~Mathlib.Algebra.GroupPower.Basic            instructions     5.6%
- ~Mathlib.Algebra.Order.Hom.Basic             instructions     7.6%
- ~Mathlib.Algebra.Order.Sub.Basic             instructions     5.2%
- ~Mathlib.CategoryTheory.Category.Cat.Limit   instructions     6.5%
+ ~Mathlib.Combinatorics.Catalan               instructions    -7.4%
- ~Mathlib.Combinatorics.Composition           instructions     5.5%
+ ~Mathlib.Data.Nat.Fib                        instructions    -6.4%
+ ~Mathlib.Data.Polynomial.Monomial            instructions    -5.1%
+ ~Mathlib.NumberTheory.ADEInequality          instructions   -17.4%
- ~Mathlib.Order.Heyting.Hom                   instructions     5.7%
- ~Qq.AssertInstancesCommute                   instructions    10.7%
- ~Std.Data.AssocList                          instructions     8.1%
- ~Std.Data.HashMap.Basic                      instructions     6.9%
- ~Std.Data.HashMap.WF                         instructions     7.3%
- ~Std.Data.String                             instructions     5.9%
+ ~Std.Tactic.Lint.TypeClass                   instructions   -73.4%

[semorrison]

bors merge

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[ChrisHughes24]

I think this is breaking the build

bors r-

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style