feat(*): define subobject classes from submonoid up to subfield (#11750)

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`:

```lean
@[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` #11758
 - [ ] remove duplicate instances like `subgroup.to_group` (replaced by the `subgroup_class.to_subgroup` instances that are added by this PR) #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:
```lean
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:
```lean
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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Why.20is.20.60int.2Ecast_abs.60.20so.20slow.3F/near/266945077)). 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.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

Author: Vierkantor

src/algebra/algebra/subalgebra/basic.lean

@@ -37,7 +37,14 @@ variables [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [al
 include R
 
 instance : set_like (subalgebra R A) A :=
-⟨subalgebra.carrier, λ p q h, by cases p; cases q; congr'⟩
+{ coe := subalgebra.carrier,
+  coe_injective' := λ p q h, by cases p; cases q; congr' }
+
+instance : subsemiring_class (subalgebra R A) A :=
+{ add_mem := add_mem',
+  mul_mem := mul_mem',
+  one_mem := one_mem',
+  zero_mem := zero_mem' }
 
 @[simp]
 lemma mem_carrier {s : subalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s := iff.rfl
@@ -101,6 +108,10 @@ S.to_subsemiring.zero_mem
 theorem add_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S :=
 S.to_subsemiring.add_mem hx hy
 
+instance {R A : Type*} [comm_ring R] [ring A] [algebra R A] : subring_class (subalgebra R A) A :=
+{ neg_mem := λ S x hx, neg_one_smul R x ▸ S.smul_mem hx _,
+  .. subalgebra.subsemiring_class }
+
 theorem neg_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
   [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) : -x ∈ S :=
 neg_one_smul R x ▸ S.smul_mem hx _

src/algebra/lie/subalgebra.lean

@@ -49,10 +49,20 @@ instance : has_zero (lie_subalgebra R L) :=
 
 instance : inhabited (lie_subalgebra R L) := ⟨0⟩
 instance : has_coe (lie_subalgebra R L) (submodule R L) := ⟨lie_subalgebra.to_submodule⟩
-instance : has_mem L (lie_subalgebra R L) := ⟨λ x L', x ∈ (L' : set L)⟩
 
 namespace lie_subalgebra
 
+open neg_mem_class
+
+instance : set_like (lie_subalgebra R L) L :=
+{ coe := λ L', L',
+  coe_injective' := λ L' L'' h, by { rcases L' with ⟨⟨⟩⟩, rcases L'' with ⟨⟨⟩⟩, congr' } }
+
+instance : add_subgroup_class (lie_subalgebra R L) L :=
+{ add_mem := λ L', L'.add_mem',
+  zero_mem := λ L', L'.zero_mem',
+  neg_mem := λ L' x hx, show -x ∈ (L' : submodule R L), from neg_mem hx }
+
 /-- A Lie subalgebra forms a new Lie ring. -/
 instance (L' : lie_subalgebra R L) : lie_ring L' :=
 { bracket      := λ x y, ⟨⁅x.val, y.val⁆, L'.lie_mem' x.property y.property⟩,
@@ -119,10 +129,10 @@ lemma coe_zero_iff_zero (x : L') : (x : L) = 0 ↔ x = 0 := (ext_iff L' x 0).sym
 
 @[ext] lemma ext (L₁' L₂' : lie_subalgebra R L) (h : ∀ x, x ∈ L₁' ↔ x ∈ L₂') :
   L₁' = L₂' :=
-by { cases L₁', cases L₂', simp only [], ext x, exact h x, }
+set_like.ext h
 
 lemma ext_iff' (L₁' L₂' : lie_subalgebra R L) : L₁' = L₂' ↔ ∀ x, x ∈ L₁' ↔ x ∈ L₂' :=
-⟨λ h x, by rw h, ext L₁' L₂'⟩
+set_like.ext_iff
 
 @[simp] lemma mk_coe (S : set L) (h₁ h₂ h₃ h₄) :
   ((⟨⟨S, h₁, h₂, h₃⟩, h₄⟩ : lie_subalgebra R L) : set L) = S := rfl
@@ -132,12 +142,10 @@ lemma ext_iff' (L₁' L₂' : lie_subalgebra R L) : L₁' = L₂' ↔ ∀ x, x 
 by { cases p, refl, }
 
 lemma coe_injective : function.injective (coe : lie_subalgebra R L → set L) :=
-by { rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ h, congr' }
-
-instance : set_like (lie_subalgebra R L) L := ⟨coe, coe_injective⟩
+set_like.coe_injective
 
 @[norm_cast] theorem coe_set_eq (L₁' L₂' : lie_subalgebra R L) :
-  (L₁' : set L) = L₂' ↔ L₁' = L₂' := coe_injective.eq_iff
+  (L₁' : set L) = L₂' ↔ L₁' = L₂' := set_like.coe_set_eq
 
 lemma to_submodule_injective :
   function.injective (coe : lie_subalgebra R L → submodule R L) :=
@@ -542,8 +550,8 @@ variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [li
 /-- An injective Lie algebra morphism is an equivalence onto its range. -/
 noncomputable def of_injective (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) :
   L₁ ≃ₗ⁅R⁆ f.range :=
-{ map_lie' := λ x y, by { apply set_coe.ext, simpa, },
-..(linear_equiv.of_injective ↑f $ by rwa [lie_hom.coe_to_linear_map])}
+{ map_lie' := λ x y, by { apply set_coe.ext, simpa },
+  .. linear_equiv.of_injective (f : L₁ →ₗ[R] L₂) $ by rwa [lie_hom.coe_to_linear_map] }
 
 @[simp] lemma of_injective_apply (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) (x : L₁) :
   ↑(of_injective f h x) = f x := rfl

src/algebra/lie/submodule.lean

@@ -49,10 +49,17 @@ namespace lie_submodule
 
 variables {R L M} (N N' : lie_submodule R L M)
 
+open neg_mem_class
+
 instance : set_like (lie_submodule R L M) M :=
 { coe := carrier,
   coe_injective' := λ N O h, by cases N; cases O; congr' }
 
+instance : add_subgroup_class (lie_submodule R L M) M :=
+{ add_mem := λ N, N.add_mem',
+  zero_mem := λ N, N.zero_mem',
+  neg_mem := λ N x hx, show -x ∈ N.to_submodule, from neg_mem hx }
+
 /-- The zero module is a Lie submodule of any Lie module. -/
 instance : has_zero (lie_submodule R L M) :=
 ⟨{ lie_mem := λ x m h, by { rw ((submodule.mem_bot R).1 h), apply lie_zero, },

src/algebra/module/submodule.lean

@@ -47,7 +47,12 @@ namespace submodule
 variables [semiring R] [add_comm_monoid M] [module R M]
 
 instance : set_like (submodule R M) M :=
-⟨submodule.carrier, λ p q h, by cases p; cases q; congr'⟩
+{ coe := submodule.carrier,
+  coe_injective' := λ p q h, by cases p; cases q; congr' }
+
+instance : add_submonoid_class (submodule R M) M :=
+{ zero_mem := zero_mem',
+  add_mem := add_mem' }
 
 @[simp] theorem mem_to_add_submonoid (p : submodule R M) (x : M) : x ∈ p.to_add_submonoid ↔ x ∈ p :=
 iff.rfl
@@ -282,7 +287,11 @@ variables {module_M : module R M}
 variables (p p' : submodule R M)
 variables {r : R} {x y : M}
 
-lemma neg_mem (hx : x ∈ p) : -x ∈ p := p.to_sub_mul_action.neg_mem hx
+instance [module R M] : add_subgroup_class (submodule R M) M :=
+{ neg_mem := λ p x, p.to_sub_mul_action.neg_mem,
+  .. submodule.add_submonoid_class }
+
+lemma neg_mem (hx : x ∈ p) : -x ∈ p := neg_mem_class.neg_mem hx
 
 /-- Reinterpret a submodule as an additive subgroup. -/
 def to_add_subgroup : add_subgroup M :=

src/analysis/inner_product_space/l2_space.lean

@@ -224,7 +224,6 @@ end
 protected lemma range_linear_isometry [Π i, complete_space (G i)] :
   hV.linear_isometry.to_linear_map.range = (⨆ i, (V i).to_linear_map.range).topological_closure :=
 begin
-  classical,
   refine le_antisymm _ _,
   { rintros x ⟨f, rfl⟩,
     refine mem_closure_of_tendsto (hV.has_sum_linear_isometry f) (eventually_of_forall _),
@@ -237,7 +236,7 @@ begin
     { refine supr_le _,
       rintros i x ⟨x, rfl⟩,
       use lp.single 2 i x,
-      convert hV.linear_isometry_apply_single _ },
+      exact hV.linear_isometry_apply_single x },
     exact hV.linear_isometry.isometry.uniform_inducing.is_complete_range.is_closed }
 end
 

src/field_theory/galois.lean

@@ -150,7 +150,7 @@ lemma alg_equiv.transfer_galois (f : E ≃ₐ[F] E') : is_galois F E ↔ is_galo
 ⟨λ h, by exactI is_galois.of_alg_equiv f, λ h, by exactI is_galois.of_alg_equiv f.symm⟩
 
 lemma is_galois_iff_is_galois_top : is_galois F (⊤ : intermediate_field F E) ↔ is_galois F E :=
-(intermediate_field.top_equiv).transfer_galois
+(intermediate_field.top_equiv : (⊤ : intermediate_field F E) ≃ₐ[F] E).transfer_galois
 
 instance is_galois_bot : is_galois F (⊥ : intermediate_field F E) :=
 (intermediate_field.bot_equiv F E).transfer_galois.mpr (is_galois.self F)
@@ -401,7 +401,8 @@ begin
   simp only [P] at *,
   rw [of_separable_splitting_field_aux hp K (multiset.mem_to_finset.mp hx),
     hK, finrank_mul_finrank],
-  exact (linear_equiv.finrank_eq (intermediate_field.lift2_alg_equiv K⟮x⟯).to_linear_equiv).symm,
+  symmetry,
+  exact linear_equiv.finrank_eq (alg_equiv.to_linear_equiv (intermediate_field.lift2_alg_equiv _))
 end
 
 /--Equivalent characterizations of a Galois extension of finite degree-/

src/field_theory/intermediate_field.lean

@@ -61,6 +61,14 @@ def to_subfield : subfield L := { ..S.to_subalgebra, ..S }
 instance : set_like (intermediate_field K L) L :=
 ⟨λ S, S.to_subalgebra.carrier, by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨h⟩, congr, }⟩
 
+instance : subfield_class (intermediate_field K L) L :=
+{ add_mem := λ s, s.add_mem',
+  zero_mem := λ s, s.zero_mem',
+  neg_mem := neg_mem',
+  mul_mem := λ s, s.mul_mem',
+  one_mem := λ s, s.one_mem',
+  inv_mem := inv_mem' }
+
 @[simp]
 lemma mem_carrier {s : intermediate_field K L} {x : L} : x ∈ s.carrier ↔ x ∈ s := iff.rfl
 

src/field_theory/subfield.lean

@@ -63,6 +63,43 @@ universes u v w
 
 variables {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M]
 
+/-- `subfield_class S K` states `S` is a type of subsets `s ⊆ K` closed under field operations. -/
+class subfield_class (S : Type*) (K : out_param $ Type*) [field K] [set_like S K]
+  extends subring_class S K, inv_mem_class S K.
+
+namespace subfield_class
+
+variables (S : Type*) [set_like S K] [h : subfield_class S K]
+include h
+
+/-- A subfield contains `1`, products and inverses.
+
+Be assured that we're not actually proving that subfields are subgroups:
+`subgroup_class` is really an abbreviation of `subgroup_with_or_without_zero_class`.
+ -/
+@[priority 100] -- See note [lower instance priority]
+instance subfield_class.to_subgroup_class : subgroup_class S K := { .. h }
+
+/-- A subfield inherits a field structure -/
+@[priority 75] -- Prefer subclasses of `field` over subclasses of `subfield_class`.
+instance to_field (s : S) : field s :=
+subtype.coe_injective.field (coe : s → K)
+  rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+  (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+
+omit h
+
+/-- A subfield of a `linear_ordered_field` is a `linear_ordered_field`. -/
+@[priority 75] -- Prefer subclasses of `field` over subclasses of `subfield_class`.
+instance to_linear_ordered_field {K} [linear_ordered_field K] [set_like S K]
+  [subfield_class S K] (s : S) :
+  linear_ordered_field s :=
+subtype.coe_injective.linear_ordered_field coe
+  rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+  (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+
+end subfield_class
+
 set_option old_structure_cmd true
 
 /-- `subfield R` is the type of subfields of `R`. A subfield of `R` is a subset `s` that is a
@@ -84,10 +121,17 @@ def to_add_subgroup (s : subfield K) : add_subgroup K :=
 def to_submonoid (s : subfield K) : submonoid K :=
 { ..s.to_subring.to_submonoid }
 
-
 instance : set_like (subfield K) K :=
 ⟨subfield.carrier, λ p q h, by cases p; cases q; congr'⟩
 
+instance : subfield_class (subfield K) K :=
+{ add_mem := add_mem',
+  zero_mem := zero_mem',
+  neg_mem := neg_mem',
+  mul_mem := mul_mem',
+  one_mem := one_mem',
+  inv_mem := inv_mem' }
+
 @[simp]
 lemma mem_carrier {s : subfield K} {x : K} : x ∈ s.carrier ↔ x ∈ s := iff.rfl