[Merged by Bors] - feat(*): define subobject classes from submonoid up to subfield

[Vierkantor]

The next part of my big refactoring plans: subobject classes in the same style as morphism classes.

This PR introduces the following subclasses of set_like:

• one_mem_class, zero_mem_class, mul_mem_class, add_mem_class, inv_mem_class, neg_mem_class
• submonoid_class, add_submonoid_class
• subgroup_class, add_subgroup_class
• subsemiring_class, subring_class, subfield_class

The main purpose of this refactor is that we can replace the wide variety of lemmas like {add_submonoid,add_subgroup,subring,subfield,submodule,subwhatever}.{prod,sum}_mem with a single prod_mem lemma that is generic over all types B that extend submonoid:

@[to_additive]
lemma prod_mem {M : Type*} [comm_monoid M] [set_like B M] [submonoid_class B M]
  {ι : Type*} {t : finset ι} {f : ι → M} (h : ∀c ∈ t, f c ∈ S) : ∏ c in t, f c ∈ S

API changes

• When you extend a struct subobject, make sure to create a corresponding subobject_class instance.

Upcoming PRs

This PR splits out the first part of #11545, namely defining the subobject classes. I am planning these follow-up PRs for further parts of #11545:

• make the subobject consistently implicit in {add,mul}_mem [Merged by Bors] - feat(group_theory): use generic subobject_class lemmas #11758
• remove duplicate instances like subgroup.to_group (replaced by the subgroup_class.to_subgroup instances that are added by this PR) refactor(*): remove duplicate subobject instances  #11759
• further deduplication such as finsupp_sum_mem

Subclassing set_like

Contrary to mathlib's typical subclass pattern, we don't extend set_like, but take a set_like instance parameter:

class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M] [set_like S M] :=
(one_mem : ∀ (s : S), (1 : M) ∈ s)

instead of:

class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M]
  extends set_like S M :=
(one_mem : ∀ (s : S), (1 : M) ∈ s)

The main reason is that this avoids some big defeq checks when typechecking e.g. x * y : s, where s : S and [comm_group G] [subgroup_class S G]. Namely, the type coe_sort s could be given by subgroup_class → @@submonoid_class _ _ (comm_group.to_group.to_monoid) → set_like → has_coe_to_sort or by subgroup_class → @@submonoid_class _ _ (comm_group.to_comm_monoid.to_monoid) → set_like → has_coe_to_sort. When checking that has_mul on the first type is the same as has_mul on the second type, those two inheritance paths are unified many times over (sometimes exponentially many). So it's important to keep the size of types small, and therefore we avoid extends-based inheritance.

Defeq fixes

Adding instances like subgroup_class.to_group means that there are now two (defeq) group instances for subgroup. This makes some code more fragile, until we can replace subgroup.to_group with its more generic form in a follow-up PR. Especially when taking subgroups of subgroups I needed to help the elaborator in a few places. These should be minimally invasive for other uses of the code.

Timeout fixes

Some of the leaf files started timing out, so I made a couple of fixes. Generally these can be classed as:

• squeeze_simps
• Give inheritance subX_class S M → X s (where s : S) a lower prority than Y s → X s so that subY_class S M → Y s → X s is preferred over subY_class S M → subX_class S M → X s. This addresses slow unifications when x : s, s is a submonoid of t, which is itself a subgroup of G: existing code expects to go subgroup → group → monoid, which got changed to subgroup_class → submonoid_class → monoid; when this kind of unification issue appears in your type this results in slow unification. By tweaking the priorities, we help the elaborator find our preferred instance, avoiding the big defeq checks. (The real fix should of course be to fix the unifier so it doesn't become exponential in these kinds of cases.)
• Split a long proof with duplication into smaller parts. This was basically my last resort.

I decided to bump the limit for the fails_quickly linter for measure_theory.Lp_meas.complete_space, which apparently just barely goes over this limit now. The time difference was about 10%-20% for that specific instance.

---

• depends on: [Merged by Bors] - refactor(ring_theory): clean up algebraic_iff_integral #11773
• depends on: [Merged by Bors] - chore(geometry/euclidean): split repetitive proof #12209

[YaelDillies]

This looks great!

[leanprover-community-bot-assistant]

This PR/issue depends on:

• [Merged by Bors] - refactor(ring_theory): clean up algebraic_iff_integral #11773
• [Merged by Bors] - chore(geometry/euclidean): split repetitive proof #12209
  By Dependent Issues (🤖). Happy coding!

[eric-wieser]

• affine.simplex.orthogonal_projection_span is the new way to write orthogonal_projection (affine_span ℝ (set.range s.points)). Moving this into its own definition fixed a long string of timeouts (partially by splitting a slow declaration into two that are only half as slow, partially by guiding the elaborator a bit).

This no longer is part of this PR, right?

[riccardobrasca]

bors d+

[bors]

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

[Vierkantor]

Everything also builds on my machine, so:

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests