[Merged by Bors] - perf: improve some instances in GroupTheory/Congruence

[ChrisHughes24]

---

[ChrisHughes24]

!bench

[leanprover-bot]

Here are the benchmark results for commit c077c39.
There were significant changes against commit 571a128:

  Benchmark                                                Metric         Change
  ==============================================================================
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic              instructions   -12.9%
+ ~Mathlib.Algebra.Category.GroupCat.Adjunctions           instructions    -5.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Abelian              instructions   -20.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Kernels              instructions    -9.4%
+ ~Mathlib.Algebra.Category.ModuleCat.Limits               instructions   -42.7%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic       instructions   -26.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed      instructions    -6.7%
+ ~Mathlib.Algebra.DirectLimit                             instructions    -7.7%
+ ~Mathlib.Algebra.Lie.TensorProduct                       instructions    -5.4%
+ ~Mathlib.Analysis.Complex.Arg                            instructions    -5.6%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle   instructions   -14.5%
+ ~Mathlib.Dynamics.Ergodic.AddCircle                      instructions   -12.9%
+ ~Mathlib.GroupTheory.CoprodI                             instructions   -11.9%
+ ~Mathlib.LinearAlgebra.Dual                              instructions    -8.9%
+ ~Mathlib.LinearAlgebra.FreeModule.IdealQuotient          instructions   -16.6%
+ ~Mathlib.LinearAlgebra.TensorPower                       instructions   -13.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite            instructions    -7.0%
+ ~Mathlib.MeasureTheory.Group.AddCircle                   instructions   -20.0%
+ ~Mathlib.NumberTheory.WellApproximable                   instructions   -10.4%
+ ~Mathlib.RepresentationTheory.FdRep                      instructions    -7.3%
+ ~Mathlib.RepresentationTheory.Rep                        instructions    -5.6%
+ ~Mathlib.RingTheory.Ideal.Cotangent                      instructions    -6.2%
+ ~Mathlib.RingTheory.Kaehler                              instructions    -8.3%
+ ~Mathlib.RingTheory.MatrixAlgebra                        instructions    -6.1%

[ChrisHughes24]

I think this can wait until after the related Lean4 issue, and we can see if there is still a benefit to this.

[mattrobball]

I think a note explaining situation is good here. I would hope the slowdown in unification we see here (and in related files) can be fixed further up the library. Similarly for the other explicit projections below.

[mattrobball]

bors d+

I think this is orthogonal to leanprover/lean4#2478 and it would be really nice to have it now without waiting.

[bors]

✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ChrisHughes24]

!bench

[leanprover-bot]

Here are the benchmark results for commit 36df7f7.
There were significant changes against commit b3b5ba1:

  Benchmark                                                           Metric         Change
  =========================================================================================
+ ~Mathlib.Algebra.Category.GroupCat.Adjunctions                      instructions    -5.2%
+ ~Mathlib.Algebra.Category.GroupCat.Injective                        instructions    -7.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Abelian                         instructions   -20.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Kernels                         instructions    -9.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Limits                          instructions   -42.8%
+ ~Mathlib.Algebra.DirectLimit                                        instructions    -7.5%
+ ~Mathlib.Analysis.Complex.Arg                                       instructions    -5.2%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle              instructions   -13.7%
+ ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions    -5.7%
+ ~Mathlib.Dynamics.Ergodic.AddCircle                                 instructions   -12.2%
+ ~Mathlib.GroupTheory.HNNExtension                                   instructions   -10.1%
+ ~Mathlib.LinearAlgebra.Dual                                         instructions    -8.7%
+ ~Mathlib.LinearAlgebra.FreeModule.IdealQuotient                     instructions   -16.7%
+ ~Mathlib.LinearAlgebra.TensorPower                                  instructions   -12.5%
+ ~Mathlib.MeasureTheory.Group.AddCircle                              instructions   -17.7%
+ ~Mathlib.NumberTheory.WellApproximable                              instructions    -9.1%
+ ~Mathlib.RingTheory.Ideal.Cotangent                                 instructions    -8.6%

[ChrisHughes24]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style