mathlib

feb99064 - fix(data/set_like): unbundled subclasses of `out_param` classes should not repeat the parents' `out_param` (#18291)

fix(data/set_like): unbundled subclasses of `out_param` classes should not repeat the parents' `out_param` (#18291) This PR is a backport for a mathlib4 fix for a large amount of issues encountered in the port of `group_theory.subgroup.basic`, leanprover-community/mathlib4#1797. Subobject classes such as `mul_mem_class` and `submonoid_class` take a `set_like` parameter, and we were used to just copy over the `M : out_param Type` declaration from `set_like`. Since Lean 3 synthesizes from left to right, we'd fill in the `out_param` from `set_like`, then the `has_mul M` instance would be available for synthesis and we'd be in business. In Lean 4 however, we will often go from right to left, so that `MulMemClass ?M S [?inst : Mul ?M]` is handled first, which can't be solved before finding a `Mul ?M` instance on the metavariable `?M`, causing search through all `Mul` instances. The solution is: whenever a class is declared that takes another class as parameter (i.e. unbundled inheritance), the `out_param`s of the parent class should be unmarked and become in-params in the child class. Then Lean will try to find the parent class instance first, fill in the `out_param`s and we'll be able to synthesize the child class instance without problems. One consequence is that sometimes we have to give slightly more type ascription when talking about membership and the types don't quite align: if `M` and `M'` are semireducibly defeq, then before `zero_mem_class S M` would work to prove `(0 : M') ∈ (s : S)`, since the `out_param` became a metavariable, was filled in, and then checked (up to semireducibility apparently) for equality. Now `M` is checked to equal `M'` before applying the instance, with instance-reducible transparency. I don't think this is a huge issue since it feels Lean 4 is stricter about these kinds of equalities anyway. Mathlib4 pair: leanprover-community/mathlib4#1832