chore: remove `CovariantClass` and `ContravariantClass`

[astrainfinita]

trafficstars

Lean cannot handle CovariantClass and ContravariantClass correctly

• TC slowness
  • Zulip
  • https://github.com/leanprover-community/mathlib4/issues/6646#issuecomment-1691792488
  • It may also have made #6326 fail.
• Needs a weird hack to find instance: #9252

---

• [x] depends on: #13154

[astrainfinita]

!bench

[astrainfinita]

!bench (edit: Sorry, I thought the edit didn't work...)

[leanprover-bot]

Here are the benchmark results for commit 1b1d57010f090909ba8fb60a23daacf0772d39bb. There were no significant changes against commit b0729237203be7d86931d9c1855e81c06e31c285.

[MichaelStollBayreuth]

My script reports:

General information:
  lint:                                                -34.605 * 10⁹ (-0.288%)
  build:                                               -320.41 * 10⁹ (-0.277%)

Files that got slower:
  Mathlib.AlgebraicTopology.SimplicialObject:          +2.0389 * 10⁹ (+0.995%)
  Mathlib.Algebra.Homology.HomotopyCategory.Triangulated:
                                                       +1.4258 * 10⁹ (+0.734%)

Files that got faster:
  Mathlib.Algebra.Order.Group.Defs:                    -6.4722 * 10⁹ (-20.8%)
  Mathlib.Data.Set.Pointwise.Interval:                 -6.1749 * 10⁹ (-8.06%)
  Mathlib.Computability.AkraBazzi.GrowsPolynomially:   -4.1764 * 10⁹ (-8.02%)
  Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm:
                                                       -3.8651 * 10⁹ (-1.39%)
  Mathlib.Data.Finset.Basic:                           -3.7792 * 10⁹ (-6.91%)
  Mathlib.Computability.AkraBazzi.AkraBazzi:           -3.6013 * 10⁹ (-2.43%)
  Mathlib.SetTheory.Ordinal.Notation:                  -3.3928 * 10⁹ (-7.61%)
  Mathlib.MeasureTheory.Decomposition.Jordan:          -3.0464 * 10⁹ (-9.58%)
  Mathlib.Algebra.Order.Interval.Basic:                -2.9978 * 10⁹ (-9.64%)
  Mathlib.Analysis.PSeries:                            -2.9565 * 10⁹ (-5.02%)
  Mathlib.Algebra.Order.Monoid.Unbundled.Basic:        -2.9485 * 10⁹ (-13.4%)
  Mathlib.Algebra.Order.Floor:                         -2.9299 * 10⁹ (-3.73%)
  Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform:
                                                       -2.6359 * 10⁹ (-6.95%)
  Mathlib.Algebra.Order.Pointwise:                     -2.6224 * 10⁹ (-5.56%)
  Mathlib.Algebra.Order.CauSeq.Basic:                  -2.6120 * 10⁹ (-4.15%)
  Mathlib.Algebra.Order.CauSeq.BigOperators:           -2.5459 * 10⁹ (-8.48%)
  Mathlib.Algebra.Order.Nonneg.Ring:                   -2.5141 * 10⁹ (-7.52%)
  Mathlib.Computability.Ackermann:                     -2.4383 * 10⁹ (-13.3%)
  Mathlib.Algebra.ContinuedFractions.Computation.Approximations:
                                                       -2.4331 * 10⁹ (-8.41%)
  Mathlib.Data.Set.Card:                               -2.4285 * 10⁹ (-5.70%)
  Mathlib.Algebra.MonoidAlgebra.Degree:                -2.4205 * 10⁹ (-8.86%)
  Mathlib.MeasureTheory.Measure.Haar.Disintegration:   -2.3934 * 10⁹ (-4.70%)
  Mathlib.MeasureTheory.Measure.EverywherePos:         -2.3931 * 10⁹ (-11.2%)
  Mathlib.Combinatorics.SetFamily.FourFunctions:       -2.3198 * 10⁹ (-4.24%)
  Mathlib.Algebra.Order.Field.Basic:                   -2.2637 * 10⁹ (-3.86%)
  Mathlib.Data.Nat.Cast.Order:                         -2.2433 * 10⁹ (-16.0%)
  Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle:
                                                       -2.2324 * 10⁹ (-4.41%)
  Mathlib.Analysis.Distribution.SchwartzSpace:         -2.1352 * 10⁹ (-1.08%)
  Mathlib.Algebra.Order.Group.Abs:                     -2.1340 * 10⁹ (-9.36%)
  Mathlib.NumberTheory.Zsqrtd.Basic:                   -1.9998 * 10⁹ (-2.59%)
  Mathlib.Analysis.SpecialFunctions.Log.Base:          -1.9440 * 10⁹ (-9.53%)
  Mathlib.Algebra.Bounds:                              -1.9200 * 10⁹ (-19.0%)
  Mathlib.MeasureTheory.Measure.Hausdorff:             -1.8194 * 10⁹ (-3.08%)
  Mathlib.Algebra.Order.Module.Defs:                   -1.8006 * 10⁹ (-2.24%)
  Mathlib.Algebra.Order.Group.PosPart:                 -1.7722 * 10⁹ (-12.9%)
  Mathlib.Analysis.NormedSpace.Multilinear.Basic:      -1.7512 * 10⁹ (-0.509%)
  Mathlib.Analysis.NormedSpace.Pointwise:              -1.6777 * 10⁹ (-3.68%)
  Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk:  -1.6756 * 10⁹ (-2.23%)
  Mathlib.Algebra.Order.Positive.Ring:                 -1.6272 * 10⁹ (-18.2%)
  Mathlib.MeasureTheory.Decomposition.SignedHahn:      -1.5728 * 10⁹ (-5.89%)
  Mathlib.NumberTheory.NumberField.Discriminant:       -1.5534 * 10⁹ (-0.720%)
  Mathlib.Data.Nat.PartENat:                           -1.5516 * 10⁹ (-8.44%)
  Mathlib.Analysis.Analytic.Basic:                     -1.5438 * 10⁹ (-0.538%)
  Mathlib.Algebra.Order.Ring.Abs:                      -1.5379 * 10⁹ (-10.2%)
  Mathlib.MeasureTheory.Integral.SetToL1:              -1.5320 * 10⁹ (-0.525%)
  Mathlib.Algebra.GroupPower.Order:                    -1.5239 * 10⁹ (-5.00%)
  Mathlib.Combinatorics.Additive.AP.Three.Behrend:     -1.5219 * 10⁹ (-3.45%)
  Mathlib.Analysis.NormedSpace.Real:                   -1.4446 * 10⁹ (-8.41%)
  Mathlib.Probability.Martingale.Basic:                -1.4401 * 10⁹ (-2.75%)
  Mathlib.Analysis.Complex.AbelLimit:                  -1.4063 * 10⁹ (-4.85%)
  Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace:
                                                       -1.3841 * 10⁹ (-2.89%)
  Mathlib.MeasureTheory.Covering.Differentiation:      -1.3778 * 10⁹ (-2.82%)
  Mathlib.Algebra.Order.Kleene:                        -1.3306 * 10⁹ (-9.34%)
  Mathlib.Algebra.Order.Ring.Defs:                     -1.3260 * 10⁹ (-2.31%)
  Mathlib.NumberTheory.DiophantineApproximation:       -1.3187 * 10⁹ (-3.01%)
  Mathlib.Algebra.Order.ToIntervalMod:                 -1.3132 * 10⁹ (-1.79%)
  Mathlib.Combinatorics.Additive.PluenneckeRuzsa:      -1.3042 * 10⁹ (-1.45%)
  Mathlib.NumberTheory.PellMatiyasevic:                -1.2703 * 10⁹ (-2.80%)
  Mathlib.NumberTheory.Cyclotomic.PID:                 -1.2090 * 10⁹ (-13.0%)
  Mathlib.Algebra.GeomSum:                             -1.1794 * 10⁹ (-2.86%)
  Mathlib.Combinatorics.SimpleGraph.Density:           -1.1737 * 10⁹ (-5.95%)
  Mathlib.Analysis.Convex.Uniform:                     -1.1646 * 10⁹ (-4.84%)
  Mathlib.NumberTheory.Pell:                           -1.1618 * 10⁹ (-2.49%)
  Mathlib.LinearAlgebra.Ray:                           -1.1557 * 10⁹ (-1.86%)
  Mathlib.Data.Complex.Exponential:                    -1.1495 * 10⁹ (-0.848%)
  Mathlib.Data.Sign:                                   -1.1484 * 10⁹ (-3.64%)
  Mathlib.Analysis.Analytic.Inverse:                   -1.1471 * 10⁹ (-1.02%)
  Mathlib.Topology.Instances.ENNReal:                  -1.1404 * 10⁹ (-1.77%)
  Mathlib.Algebra.Order.Archimedean:                   -1.1321 * 10⁹ (-5.02%)
  Mathlib.MeasureTheory.Integral.Lebesgue:             -1.1229 * 10⁹ (-1.14%)
  Mathlib.Combinatorics.Enumerative.Composition:       -1.1149 * 10⁹ (-4.20%)
  Mathlib.Analysis.SpecificLimits.FloorPow:            -1.0965 * 10⁹ (-2.54%)
  Mathlib.Combinatorics.SimpleGraph.Triangle.Removal:  -1.0903 * 10⁹ (-3.18%)
  Mathlib.Data.Nat.Digits:                             -1.0682 * 10⁹ (-3.70%)
  Mathlib.Algebra.Order.Sub.Canonical:                 -1.0610 * 10⁹ (-9.72%)
  Mathlib.Analysis.Calculus.FDeriv.Measurable:         -1.0267 * 10⁹ (-1.01%)
  Mathlib.Data.Ordmap.Ordset:                          -1.0148 * 10⁹ (-1.87%)
  Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable:
                                                       -1.0111 * 10⁹ (-1.16%)
  Mathlib.Data.Num.Lemmas:                             -1.0095 * 10⁹ (-0.837%)

[github-actions[bot]]

PR summary 063f8b9c0d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Covariant.act_rel_act_of_rel + Covariant.act_rel_act_of_rel_of_rel + Covariant.act_rel_of_rel_of_act_rel + Covariant.rel_act_of_rel_of_rel_act + IsOrderedCancelSMul.contravariant_le + MulPosMono.of_covariant + MulPosMono.to_covariant_pos_mul_le + MulPosReflectLE.of_contravariant + MulPosReflectLT.of_contravariant + MulPosReflectLT.to_contravariant_pos_mul_lt + MulPosStrictMono.of_covariant + PosMulMono.of_covariant + PosMulMono.to_covariant_pos_mul_le + PosMulReflectLE.of_contravariant + PosMulReflectLT.of_contravariant + PosMulReflectLT.to_contravariant_pos_mul_lt + PosMulStrictMono.of_covariant + SMulLeftMono + SMulLeftStrictMono + VAddLeftMono + VAddLeftStrictMono + contravariant_mul_le + contravariant_mul_lt + contravariant_nonneg_mul_lt + contravariant_nonneg_swap_mul_lt + contravariant_pos_mul_le + contravariant_pos_swap_mul_le + contravariant_swap_mul_le + contravariant_swap_mul_lt + covariant_mul_le + covariant_mul_lt + covariant_nonneg_mul_le + covariant_nonneg_swap_mul_le + covariant_pos_mul_lt + covariant_pos_swap_mul_lt + covariant_smul_le + covariant_smul_lt + covariant_swap_mul_le + covariant_swap_mul_lt + instance (priority := 100) Group.mulLeftReflectLE_of_mulLeftMono [Group N] [LE N] + instance (priority := 100) Group.mulLeftReflectLT_of_mulLeftStrictMono [Group N] [LT N] + instance (priority := 100) Group.mulRightReflectLE_of_mulRightMono [Group N] [LE N] + instance (priority := 100) Group.mulRightReflectLT_of_mulRightStrictMono [Group N] [LT N] + instance : SMulLeftMono (Set S) (Submodule R M) + instance : SMulLeftMono (Submodule R A) (Submodule R M) + instance : SMulLeftMono G (ValuationSubring K) + instance : SMulLeftMono M (Ideal R) + instance : SMulLeftMono M (Subring R) + instance : SMulLeftMono M (Subsemiring R) + instance : SMulLeftMono R' (Subalgebra R A) + instance : SMulLeftMono α (Subgroup G) + instance : SMulLeftMono α (Submodule R M) + instance : SMulLeftMono α (Submonoid M) + instance [LE G] [LE P] [SMul G P] [IsOrderedSMul G P] : SMulLeftMono G P + mulLeftMono_of_mulLeftReflectLT + mulRightMono_of_mulRightReflectLT + smul_lt_smul_left ++-- addLECancellable_coe - ContravariantClass - CovariantClass - Group.mulLeftReflectLE_of_mulLeftMono - Group.mulLeftReflectLT_of_mulLeftStrictMono - Group.mulRightReflectLE_of_mulRightMono - Group.mulRightReflectLT_of_mulRightStrictMono - MulPosMono.to_covariantClass_pos_mul_le - MulPosReflectLT.to_contravariantClass_pos_mul_lt - PosMulMono.to_covariantClass_pos_mul_le - PosMulReflectLT.to_contravariantClass_pos_mul_lt - act_rel_act_of_rel - act_rel_act_of_rel_of_rel - act_rel_of_rel_of_act_rel - contravariant_lt_of_covariant_le - contravariant_swap_mul_of_contravariant_mul - covariantClass_le_of_lt - covariant_lt_of_contravariant_le - covariant_swap_mul_of_covariant_mul - instance (priority := 100) Group.covconv [Group N] [CovariantClass N N (· * ·) r] : - instance (priority := 100) Group.covconv_swap [Group N] [CovariantClass N N (swap (· * ·)) r] : - instance (priority := 200) [LE G] [LE P] [SMul G P] [IsOrderedCancelSMul G P] : - instance : CovariantClass (Set S) (Submodule R M) HSMul.hSMul LE.le - instance : CovariantClass (Submodule R A) (Submodule R M) HSMul.hSMul LE.le - instance : CovariantClass G (ValuationSubring K) HSMul.hSMul LE.le - instance : CovariantClass M (Ideal R) HSMul.hSMul LE.le - instance : CovariantClass M (Subring R) HSMul.hSMul LE.le - instance : CovariantClass M (Subsemiring R) HSMul.hSMul LE.le - instance : CovariantClass R' (Subalgebra R A) HSMul.hSMul LE.le - instance : CovariantClass α (Subgroup G) HSMul.hSMul LE.le - instance : CovariantClass α (Submodule R M) HSMul.hSMul LE.le - instance : CovariantClass α (Submonoid M) HSMul.hSMul LE.le - instance [LE G] [LE P] [SMul G P] [IsOrderedSMul G P] : CovariantClass G P (· • ·) (· ≤ ·) - rel_act_of_rel_of_rel_act

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13154~~ By Dependent Issues (🤖). Happy coding!