feat(data/set_like): remove repeated boilerplate from subobjects (#6768)

This just scratches the surface, and removes all of the boilerplate that is just a consequence of the injective map to a `set`.
Already this trims more than 150 lines.

For every lemma of the form `set_like.*` added in this PR, the corresponding `submonoid.*`, `add_submonoid.*`, `sub_mul_action.*`, `submodule.*`, `subsemiring.*`, `subring.*`, `subfield.*`, `subalgebra.*`, and `intermediate_field.*` lemmas have been removed.
Often these lemmas only existed for one or two of these subtypes, so this means that we have lemmas for more things not fewer.

Note that while the `ext_iff`, `ext'`, and `ext'_iff` lemmas have been removed, we still need the `ext` lemma as `set_like.ext` cannot directly be tagged `@[ext]`.

Author: eric-wieser

src/algebra/algebra/basic.lean

@@ -1480,7 +1480,7 @@ variables (R S M)
 
 lemma restrict_scalars_injective :
   function.injective (restrict_scalars R : submodule S M → submodule R M) :=
-λ V₁ V₂ h, ext $ by convert set.ext_iff.1 (ext'_iff.1 h); refl
+λ V₁ V₂ h, ext $ by convert set.ext_iff.1 (set_like.ext'_iff.1 h); refl
 
 @[simp] lemma restrict_scalars_inj {V₁ V₂ : submodule S M} :
   restrict_scalars R V₁ = restrict_scalars R V₂ ↔ V₁ = V₂ :=

src/algebra/algebra/operations.lean

@@ -207,7 +207,9 @@ variables (M)
 lemma pow_subset_pow {n : ℕ} : (↑M : set A)^n ⊆ ↑(M^n : submodule R A) :=
 begin
   induction n with n ih,
-  { erw [pow_zero, pow_zero, set.singleton_subset_iff], rw [mem_coe, ← one_le], exact le_refl _ },
+  { erw [pow_zero, pow_zero, set.singleton_subset_iff],
+    rw [set_like.mem_coe, ← one_le],
+    exact le_refl _ },
   { rw [pow_succ, pow_succ],
     refine set.subset.trans (set.mul_subset_mul (subset.refl _) ih) _,
     apply mul_subset_mul }
@@ -275,7 +277,7 @@ begin
   apply le_antisymm,
   { rw span_le,
     rintros _ ⟨b, m, hb, hm, rfl⟩,
-    rw [mem_coe, mem_map, set.mem_singleton_iff.mp hb],
+    rw [set_like.mem_coe, mem_map, set.mem_singleton_iff.mp hb],
     exact ⟨m, hm, rfl⟩ },
   { rintros _ ⟨m, hm, rfl⟩, exact subset_span ⟨a, m, set.mem_singleton a, hm, rfl⟩ }
 end

src/algebra/algebra/subalgebra.lean

@@ -34,26 +34,13 @@ variables {R : Type u} {A : Type v} {B : Type w}
 variables [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B]
 include R
 
-/- While we could add coercion aliases for `to_subsemiring` and `to_submodule`, they're not needed
-very often, harder to use than the projections themselves, and none of the other subobjects define
-that type of coercion. -/
-instance : has_coe_t (subalgebra R A) (set A) := ⟨λ s, s.carrier⟩
-instance : has_mem A (subalgebra R A) := ⟨λ x p, x ∈ (p : set A)⟩
-instance : has_coe_to_sort (subalgebra R A) := ⟨_, λ p, {x : A // x ∈ p}⟩
-
-lemma coe_injective : function.injective (coe : subalgebra R A → set A) :=
-λ S T h, by cases S; cases T; congr'
+instance : set_like (subalgebra R A) A :=
+⟨subalgebra.carrier, λ p q h, by cases p; cases q; congr'⟩
 
 @[simp]
 lemma mem_carrier {s : subalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s := iff.rfl
 
-@[simp] theorem mem_coe {s : subalgebra R A} {x : A} : x ∈ (s : set A) ↔ x ∈ s := iff.rfl
-
-@[ext] theorem ext {S T : subalgebra R A} (h : ∀ x : A, x ∈ S ↔ x ∈ T) : S = T :=
-coe_injective $ set.ext h
-
-theorem ext_iff {S T : subalgebra R A} : S = T ↔ (∀ x : A, x ∈ S ↔ x ∈ T) :=
-coe_injective.eq_iff.symm.trans set.ext_iff
+@[ext] theorem ext {S T : subalgebra R A} (h : ∀ x : A, x ∈ S ↔ x ∈ T) : S = T := set_like.ext h
 
 variables (S : subalgebra R A)
 
@@ -287,12 +274,6 @@ we define it as a `linear_equiv` to avoid type equalities. -/
 def to_submodule_equiv (S : subalgebra R A) : S.to_submodule ≃ₗ[R] S :=
 linear_equiv.of_eq _ _ rfl
 
-instance : partial_order (subalgebra R A) :=
-{ le := λ p q, ∀ ⦃x⦄, x ∈ p → x ∈ q,
-  ..partial_order.lift (coe : subalgebra R A → set A) coe_injective }
-
-lemma le_def {p q : subalgebra R A} : p ≤ q ↔ (p : set A) ⊆ q := iff.rfl
-
 /-- Reinterpret an `S`-subalgebra as an `R`-subalgebra in `comap R S A`. -/
 def comap {R : Type u} {S : Type v} {A : Type w}
   [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A]
@@ -329,7 +310,7 @@ set.image_subset_iff
 
 lemma map_injective {S₁ S₂ : subalgebra R A} (f : A →ₐ[R] B)
   (hf : function.injective f) (ih : S₁.map f = S₂.map f) : S₁ = S₂ :=
-ext $ set.ext_iff.1 $ set.image_injective.2 hf $ set.ext $ ext_iff.mp ih
+ext $ set.ext_iff.1 $ set.image_injective.2 hf $ set.ext $ set_like.ext_iff.mp ih
 
 lemma mem_map {S : subalgebra R A} {f : A →ₐ[R] B} {y : B} :
   y ∈ map S f ↔ ∃ x ∈ S, f x = y :=
@@ -369,7 +350,7 @@ protected def range (φ : A →ₐ[R] B) : subalgebra R B :=
 theorem mem_range_self (φ : A →ₐ[R] B) (x : A) : φ x ∈ φ.range := φ.mem_range.2 ⟨x, rfl⟩
 
 @[simp] lemma coe_range (φ : A →ₐ[R] B) : (φ.range : set B) = set.range φ :=
-by { ext, rw [subalgebra.mem_coe, mem_range], refl }
+by { ext, rw [set_like.mem_coe, mem_range], refl }
 
 /-- Restrict the codomain of an algebra homomorphism. -/
 def cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S) : A →ₐ[R] S :=
@@ -487,7 +468,7 @@ instance : inhabited (subalgebra R A) := ⟨⊥⟩
 
 theorem mem_bot {x : A} : x ∈ (⊥ : subalgebra R A) ↔ x ∈ set.range (algebra_map R A) :=
 suffices (of_id R A).range = (⊥ : subalgebra R A),
-by { rw [← this, ←subalgebra.mem_coe, alg_hom.coe_range], refl },
+by { rw [← this, ←set_like.mem_coe, alg_hom.coe_range], refl },
 le_bot_iff.mp (λ x hx, subalgebra.range_le _ ((of_id R A).coe_range ▸ hx))
 
 theorem to_submodule_bot : (⊥ : subalgebra R A).to_submodule = R ∙ 1 :=

src/algebra/direct_limit.lean

@@ -96,7 +96,7 @@ that respect the directed system structure (i.e. make some diagram commute) give
 to a unique map out of the direct limit. -/
 def lift : direct_limit G f →ₗ[R] P :=
 liftq _ (direct_sum.to_module R ι P g)
-  (span_le.2 $ λ a ⟨i, j, hij, x, hx⟩, by rw [← hx, mem_coe, linear_map.sub_mem_ker_iff,
+  (span_le.2 $ λ a ⟨i, j, hij, x, hx⟩, by rw [← hx, set_like.mem_coe, linear_map.sub_mem_ker_iff,
     direct_sum.to_module_lof, direct_sum.to_module_lof, Hg])
 variables {R ι G f}
 
@@ -503,7 +503,7 @@ ideal.quotient.lift _ (free_comm_ring.lift $ λ (x : Σ i, G i), g x.1 x.2) begi
     ideal.comap (free_comm_ring.lift (λ (x : Σ (i : ι), G i), g (x.fst) (x.snd))) ⊥,
   { intros x hx, exact (mem_bot P).1 (this hx) },
   rw ideal.span_le, intros x hx,
-  rw [mem_coe, ideal.mem_comap, mem_bot],
+  rw [set_like.mem_coe, ideal.mem_comap, mem_bot],
   rcases hx with ⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩;
   simp only [ring_hom.map_sub, lift_of, Hg, ring_hom.map_one, ring_hom.map_add, ring_hom.map_mul,
       (g i).map_one, (g i).map_add, (g i).map_mul, sub_self]

src/algebra/lie/cartan_subalgebra.lean

@@ -45,7 +45,7 @@ lemma mem_normalizer_iff (x : L) : x ∈ H.normalizer ↔ ∀ (y : L), (y ∈ H)
 lemma le_normalizer : H ≤ H.normalizer :=
 begin
   rw le_def, intros x hx,
-  simp only [submodule.mem_coe, mem_coe_submodule, coe_coe, mem_normalizer_iff] at ⊢ hx,
+  simp only [set_like.mem_coe, mem_coe_submodule, coe_coe, mem_normalizer_iff] at ⊢ hx,
   intros y, exact H.lie_mem hx,
 end
 

src/algebra/lie/subalgebra.lean

@@ -114,7 +114,7 @@ lemma coe_injective : function.injective (coe : lie_subalgebra R L → set L) :=
 
 lemma to_submodule_injective :
   function.injective (coe : lie_subalgebra R L → submodule R L) :=
-λ L₁' L₂' h, by { rw submodule.ext'_iff at h, rw ← coe_set_eq, exact h, }
+λ L₁' L₂' h, by { rw set_like.ext'_iff at h, rw ← coe_set_eq, exact h, }
 
 @[simp] lemma coe_to_submodule_eq_iff (L₁' L₂' : lie_subalgebra R L) :
   (L₁' : submodule R L) = (L₂' : submodule R L) ↔ L₁' = L₂' :=
@@ -338,7 +338,7 @@ def hom_of_le : K →ₗ⁅R⁆ K' :=
 lemma hom_of_le_apply (x : K) : hom_of_le h x = ⟨x.1, h x.2⟩ := rfl
 
 lemma hom_of_le_injective : function.injective (hom_of_le h) :=
-λ x y, by simp only [hom_of_le_apply, imp_self, subtype.mk_eq_mk, submodule.coe_eq_coe,
+λ x y, by simp only [hom_of_le_apply, imp_self, subtype.mk_eq_mk, set_like.coe_eq_coe,
   subtype.val_eq_coe]
 
 /-- Given two nested Lie subalgebras `K ⊆ K'`, we can view `K` as a Lie subalgebra of `K'`,

src/algebra/lie/submodule.lean

@@ -337,7 +337,7 @@ def hom_of_le : N →ₗ⁅R,L⁆ N' :=
 lemma hom_of_le_apply (m : N) : hom_of_le h m = ⟨m.1, h m.2⟩ := rfl
 
 lemma hom_of_le_injective : function.injective (hom_of_le h) :=
-λ x y, by simp only [hom_of_le_apply, imp_self, subtype.mk_eq_mk, submodule.coe_eq_coe,
+λ x y, by simp only [hom_of_le_apply, imp_self, subtype.mk_eq_mk, set_like.coe_eq_coe,
   subtype.val_eq_coe]
 
 end inclusion_maps
@@ -441,7 +441,7 @@ def comap : lie_ideal R L :=
 
 @[simp] lemma map_coe_submodule (h : ↑(map f I) = f '' I) :
   (map f I : submodule R L') = (I : submodule R L).map f :=
-by { rw [submodule.ext'_iff, lie_submodule.coe_to_submodule, h, submodule.map_coe], refl, }
+by { rw [set_like.ext'_iff, lie_submodule.coe_to_submodule, h, submodule.map_coe], refl, }
 
 @[simp] lemma comap_coe_submodule : (comap f J : submodule R L) = (J : submodule R L').comap f :=
 rfl
@@ -603,7 +603,7 @@ begin
       have hy' : ∃ (x : L), x ∈ I ∧ f x = y, { simpa [hy], },
       obtain ⟨z₂, hz₂, rfl⟩ := hy',
       obtain ⟨z₁, rfl⟩ := h x,
-      simp only [lie_hom.coe_to_linear_map, submodule.mem_coe, set.mem_image,
+      simp only [lie_hom.coe_to_linear_map, set_like.mem_coe, set.mem_image,
         lie_submodule.mem_coe_submodule, submodule.mem_carrier, submodule.map_coe],
       use ⁅z₁, z₂⁆,
       exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩,
@@ -644,7 +644,7 @@ lemma hom_of_le_apply {I₁ I₂ : lie_ideal R L} (h : I₁ ≤ I₂) (x : I₁)
 
 lemma hom_of_le_injective {I₁ I₂ : lie_ideal R L} (h : I₁ ≤ I₂) :
   function.injective (hom_of_le h) :=
-λ x y, by simp only [hom_of_le_apply, imp_self, subtype.mk_eq_mk, submodule.coe_eq_coe,
+λ x y, by simp only [hom_of_le_apply, imp_self, subtype.mk_eq_mk, set_like.coe_eq_coe,
   subtype.val_eq_coe]
 
 @[simp] lemma map_sup_ker_eq_map : lie_ideal.map f (I ⊔ f.ker) = lie_ideal.map f I :=

src/algebra/module/submodule.lean

@@ -45,42 +45,26 @@ namespace submodule
 
 variables [semiring R] [add_comm_monoid M] [semimodule R M]
 
-instance : has_coe_t (submodule R M) (set M) := ⟨λ s, s.carrier⟩
-instance : has_mem M (submodule R M) := ⟨λ x p, x ∈ (p : set M)⟩
-instance : has_coe_to_sort (submodule R M) := ⟨_, λ p, {x : M // x ∈ p}⟩
+instance : set_like (submodule R M) M :=
+⟨submodule.carrier, λ p q h, by cases p; cases q; congr'⟩
 
-variables (p q : submodule R M)
-
-@[simp, norm_cast] theorem coe_sort_coe : ↥(p : set M) = p := rfl
-
-variables {p q}
-
-protected theorem «exists» {q : p → Prop} : (∃ x, q x) ↔ (∃ x ∈ p, q ⟨x, ‹_›⟩) := set_coe.exists
-
-protected theorem «forall» {q : p → Prop} : (∀ x, q x) ↔ (∀ x ∈ p, q ⟨x, ‹_›⟩) := set_coe.forall
-
-theorem coe_injective : injective (coe : submodule R M → set M) :=
-λ p q h, by cases p; cases q; congr'
-
-@[simp, norm_cast] theorem coe_set_eq : (p : set M) = q ↔ p = q := coe_injective.eq_iff
+variables {p q : submodule R M}
 
 @[simp] lemma mk_coe (S : set M) (h₁ h₂ h₃) :
   ((⟨S, h₁, h₂, h₃⟩ : submodule R M) : set M) = S := rfl
 
-theorem ext'_iff : p = q ↔ (p : set M) = q := coe_set_eq.symm
-
-@[ext] theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := coe_injective $ set.ext h
+@[ext] theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h
 
 theorem to_add_submonoid_injective :
   injective (to_add_submonoid : submodule R M → add_submonoid M) :=
-λ p q h, ext'_iff.2 $ add_submonoid.ext'_iff.1 h
+λ p q h, set_like.ext'_iff.2 (show _, from set_like.ext'_iff.1 h)
 
 @[simp] theorem to_add_submonoid_eq : p.to_add_submonoid = q.to_add_submonoid ↔ p = q :=
 to_add_submonoid_injective.eq_iff
 
 theorem to_sub_mul_action_injective :
   injective (to_sub_mul_action : submodule R M → sub_mul_action R M) :=
-λ p q h, ext'_iff.2 $ sub_mul_action.ext'_iff.1 h
+λ p q h, set_like.ext'_iff.2 (show _, from set_like.ext'_iff.1 h)
 
 @[simp] theorem to_sub_mul_action_eq : p.to_sub_mul_action = q.to_sub_mul_action ↔ p = q :=
 to_sub_mul_action_injective.eq_iff
@@ -104,8 +88,6 @@ variables [has_scalar S R] [semimodule S M] [is_scalar_tower S R M]
 variables (p)
 @[simp] lemma mem_carrier : x ∈ p.carrier ↔ x ∈ (p : set M) := iff.rfl
 
-@[simp] theorem mem_coe : x ∈ (p : set M) ↔ x ∈ p := iff.rfl
-
 @[simp] lemma zero_mem : (0 : M) ∈ p := p.zero_mem'
 
 lemma add_mem (h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p := p.add_mem' h₁ h₂
@@ -134,17 +116,15 @@ protected lemma nonempty : (p : set M).nonempty := ⟨0, p.zero_mem⟩
 @[simp] lemma mk_eq_zero {x} (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 := subtype.ext_iff_val
 
 variables {p}
-@[simp, norm_cast] lemma coe_eq_coe {x y : p} : (x : M) = y ↔ x = y := subtype.ext_iff_val.symm
-@[simp, norm_cast] lemma coe_eq_zero {x : p} : (x : M) = 0 ↔ x = 0 := @coe_eq_coe _ _ _ _ _ _ x 0
+@[simp, norm_cast] lemma coe_eq_zero {x : p} : (x : M) = 0 ↔ x = 0 :=
+(set_like.coe_eq_coe : (x : M) = (0 : p) ↔ x = 0)
 @[simp, norm_cast] lemma coe_add (x y : p) : (↑(x + y) : M) = ↑x + ↑y := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : p) : M) = 0 := rfl
 @[norm_cast] lemma coe_smul (r : R) (x : p) : ((r • x : p) : M) = r • ↑x := rfl
 @[simp, norm_cast] lemma coe_smul_of_tower (r : S) (x : p) : ((r • x : p) : M) = r • ↑x := rfl
 @[simp, norm_cast] lemma coe_mk (x : M) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : M) = x := rfl
 @[simp] lemma coe_mem (x : p) : (x : M) ∈ p := x.2
 
-@[simp] protected lemma eta (x : p) (hx : (x : M) ∈ p) : (⟨x, hx⟩ : p) = x := subtype.eta x hx
-
 variables (p)
 
 instance : add_comm_monoid p :=

src/algebra/module/submodule_lattice.lean

@@ -30,25 +30,6 @@ variables {p q : submodule R M}
 
 namespace submodule
 
-instance : partial_order (submodule R M) :=
-{ le := λ p q, ∀ ⦃x⦄, x ∈ p → x ∈ q,
-  ..partial_order.lift (coe : submodule R M → set M) coe_injective }
-
-lemma le_def : p ≤ q ↔ (p : set M) ⊆ q := iff.rfl
-
-@[simp, norm_cast] lemma coe_subset_coe : (p : set M) ⊆ q ↔ p ≤ q := iff.rfl
-
-lemma le_def' : p ≤ q ↔ ∀ x ∈ p, x ∈ q := iff.rfl
-
-lemma lt_def : p < q ↔ (p : set M) ⊂ q := iff.rfl
-
-lemma not_le_iff_exists : ¬ (p ≤ q) ↔ ∃ x ∈ p, x ∉ q := set.not_subset
-
-lemma exists_of_lt {p q : submodule R M} : p < q → ∃ x ∈ q, x ∉ p := set.exists_of_ssubset
-
-lemma lt_iff_le_and_exists : p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p :=
-by rw [lt_iff_le_not_le, not_le_iff_exists]
-
 /-- The set `{0}` is the bottom element of the lattice of submodules. -/
 instance : has_bot (submodule R M) :=
 ⟨{ carrier := {0}, smul_mem' := by simp { contextual := tt }, .. (⊥ : add_submonoid M)}⟩
@@ -68,14 +49,14 @@ instance unique_bot : unique (⊥ : submodule R M) :=
 
 lemma nonzero_mem_of_bot_lt {I : submodule R M} (bot_lt : ⊥ < I) : ∃ a : I, a ≠ 0 :=
 begin
-  have h := (submodule.lt_iff_le_and_exists.1 bot_lt).2,
+  have h := (set_like.lt_iff_le_and_exists.1 bot_lt).2,
   tidy,
 end
 
 instance : order_bot (submodule R M) :=
 { bot := ⊥,
   bot_le := λ p x, by simp {contextual := tt},
-  ..submodule.partial_order }
+  ..set_like.partial_order }
 
 protected lemma eq_bot_iff (p : submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x = (0 : M) :=
 ⟨ λ h, h.symm ▸ λ x hx, (mem_bot R).mp hx,
@@ -97,7 +78,7 @@ instance : has_top (submodule R M) :=
 instance : order_top (submodule R M) :=
 { top := ⊤,
   le_top := λ p x _, trivial,
-  ..submodule.partial_order }
+  ..set_like.partial_order }
 
 lemma eq_top_iff' {p : submodule R M} : p = ⊤ ↔ ∀ x, x ∈ p :=
 eq_top_iff.trans ⟨λ h x, h trivial, λ h x _, h x⟩
@@ -157,7 +138,7 @@ set.mem_bInter_iff
 
 @[simp] theorem mem_infi {ι} (p : ι → submodule R M) {x} :
   x ∈ (⨅ i, p i) ↔ ∀ i, x ∈ p i :=
-by rw [← mem_coe, infi_coe, set.mem_Inter]; refl
+by rw [← set_like.mem_coe, infi_coe, set.mem_Inter]; refl
 
 lemma mem_sup_left {S T : submodule R M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T :=
 show S ≤ S ⊔ T, from le_sup_left

src/algebra/pointwise.lean

@@ -476,8 +476,8 @@ end
 @[to_additive]
 lemma closure_mul_le (S T : set M) : closure (S * T) ≤ closure S ⊔ closure T :=
 Inf_le $ λ x ⟨s, t, hs, ht, hx⟩, hx ▸ (closure S ⊔ closure T).mul_mem
-    (le_def.mp le_sup_left $ subset_closure hs)
-    (le_def.mp le_sup_right $ subset_closure ht)
+    (set_like.le_def.mp le_sup_left $ subset_closure hs)
+    (set_like.le_def.mp le_sup_right $ subset_closure ht)
 
 @[to_additive]
 lemma sup_eq_closure (H K : submonoid M) : H ⊔ K = closure (H * K) :=