diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean index c8bc3eb4d3a7f..9b50be5026852 100644 --- a/src/algebra/algebra/basic.lean +++ b/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₂ := diff --git a/src/algebra/algebra/operations.lean b/src/algebra/algebra/operations.lean index 7f57387fade39..1a62ffbb7f7d8 100644 --- a/src/algebra/algebra/operations.lean +++ b/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 diff --git a/src/algebra/algebra/subalgebra.lean b/src/algebra/algebra/subalgebra.lean index 397b631da99c8..eb5027850d369 100644 --- a/src/algebra/algebra/subalgebra.lean +++ b/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 := diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean index d89f2796877dd..368b705cb6998 100644 --- a/src/algebra/direct_limit.lean +++ b/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] diff --git a/src/algebra/lie/cartan_subalgebra.lean b/src/algebra/lie/cartan_subalgebra.lean index d6ad5b1ccc3ad..861ccec6aa53c 100644 --- a/src/algebra/lie/cartan_subalgebra.lean +++ b/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 diff --git a/src/algebra/lie/subalgebra.lean b/src/algebra/lie/subalgebra.lean index cac8ada9f5f8a..a57f1e2295e3b 100644 --- a/src/algebra/lie/subalgebra.lean +++ b/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'`, diff --git a/src/algebra/lie/submodule.lean b/src/algebra/lie/submodule.lean index 769bdc77c14b5..3a99d0b13dad9 100644 --- a/src/algebra/lie/submodule.lean +++ b/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 := diff --git a/src/algebra/module/submodule.lean b/src/algebra/module/submodule.lean index 27c91abfbf9e3..962d4a368872c 100644 --- a/src/algebra/module/submodule.lean +++ b/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,8 +116,8 @@ 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 @@ -143,8 +125,6 @@ variables {p} @[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 := diff --git a/src/algebra/module/submodule_lattice.lean b/src/algebra/module/submodule_lattice.lean index d31a37ae57f82..03dbd746a252b 100644 --- a/src/algebra/module/submodule_lattice.lean +++ b/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 diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean index 00dbb73ba1e17..a2d697c7e40df 100644 --- a/src/algebra/pointwise.lean +++ b/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) := diff --git a/src/algebraic_geometry/prime_spectrum.lean b/src/algebraic_geometry/prime_spectrum.lean index 77676b9f20e3f..deaba4f6a7ce4 100644 --- a/src/algebraic_geometry/prime_spectrum.lean +++ b/src/algebraic_geometry/prime_spectrum.lean @@ -135,14 +135,14 @@ lemma coe_vanishing_ideal (t : set (prime_spectrum R)) : (vanishing_ideal t : set R) = {f : R | ∀ x : prime_spectrum R, x ∈ t → f ∈ x.as_ideal} := begin ext f, - rw [vanishing_ideal, submodule.mem_coe, submodule.mem_infi], + rw [vanishing_ideal, set_like.mem_coe, submodule.mem_infi], apply forall_congr, intro x, rw [submodule.mem_infi], end lemma mem_vanishing_ideal (t : set (prime_spectrum R)) (f : R) : f ∈ vanishing_ideal t ↔ ∀ x : prime_spectrum R, x ∈ t → f ∈ x.as_ideal := -by rw [← submodule.mem_coe, coe_vanishing_ideal, set.mem_set_of_eq] +by rw [← set_like.mem_coe, coe_vanishing_ideal, set.mem_set_of_eq] @[simp] lemma vanishing_ideal_singleton (x : prime_spectrum R) : vanishing_ideal ({x} : set (prime_spectrum R)) = x.as_ideal := @@ -448,7 +448,7 @@ subtype.coe_lt_coe lemma le_iff_mem_closure (x y : prime_spectrum R) : x ≤ y ↔ y ∈ closure ({x} : set (prime_spectrum R)) := by rw [← as_ideal_le_as_ideal, ← zero_locus_vanishing_ideal_eq_closure, - mem_zero_locus, vanishing_ideal_singleton, submodule.le_def] + mem_zero_locus, vanishing_ideal_singleton, set_like.coe_subset_coe] end order diff --git a/src/analysis/calculus/tangent_cone.lean b/src/analysis/calculus/tangent_cone.lean index 538f9027d13cf..e4c4a2958f718 100644 --- a/src/analysis/calculus/tangent_cone.lean +++ b/src/analysis/calculus/tangent_cone.lean @@ -309,7 +309,7 @@ begin have : _ ≤ submodule.span 𝕜 (tangent_cone_at 𝕜 (s.prod t) (x, y)) := submodule.span_mono (union_subset (subset_tangent_cone_prod_left ht.2) (subset_tangent_cone_prod_right hs.2)), - rw [linear_map.span_inl_union_inr, submodule.le_def, submodule.prod_coe] at this, + rw [linear_map.span_inl_union_inr, set_like.le_def] at this, exact (hs.1.prod ht.1).mono this end diff --git a/src/analysis/convex/cone.lean b/src/analysis/convex/cone.lean index b78e74355ca88..0f016eef646be 100644 --- a/src/analysis/convex/cone.lean +++ b/src/analysis/convex/cone.lean @@ -404,7 +404,7 @@ lemma step (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x) (dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s) (hdom : f.domain ≠ ⊤) : ∃ g, f < g ∧ ∀ x : g.domain, (x : E) ∈ s → 0 ≤ g x := begin - rcases exists_of_lt (lt_top_iff_ne_top.2 hdom) with ⟨y, hy', hy⟩, clear hy', + rcases set_like.exists_of_lt (lt_top_iff_ne_top.2 hdom) with ⟨y, hy', hy⟩, clear hy', obtain ⟨c, le_c, c_le⟩ : ∃ c, (∀ x : f.domain, -(x:E) - y ∈ s → f x ≤ c) ∧ (∀ x : f.domain, (x:E) + y ∈ s → c ≤ f x), { set Sp := f '' {x : f.domain | (x:E) + y ∈ s}, diff --git a/src/data/polynomial/algebra_map.lean b/src/data/polynomial/algebra_map.lean index 5dd2ffd8c4f30..09d65087f3134 100644 --- a/src/data/polynomial/algebra_map.lean +++ b/src/data/polynomial/algebra_map.lean @@ -46,7 +46,7 @@ rfl instance [nontrivial A] : nontrivial (subalgebra R (polynomial A)) := ⟨⟨⊥, ⊤, begin - rw [ne.def, subalgebra.ext_iff, not_forall], + rw [ne.def, set_like.ext_iff, not_forall], refine ⟨X, _⟩, simp only [algebra.mem_bot, not_exists, set.mem_range, iff_true, algebra.mem_top, algebra_map_apply, not_forall], diff --git a/src/data/polynomial/coeff.lean b/src/data/polynomial/coeff.lean index 019a9be24390c..f1b419fa95fa2 100644 --- a/src/data/polynomial/coeff.lean +++ b/src/data/polynomial/coeff.lean @@ -169,7 +169,7 @@ lemma span_le_of_coeff_mem_C_inverse (cf : ∀ (i : ℕ), f.coeff i ∈ (C ⁻¹ begin refine bInter_subset_of_mem _, rintros _ ⟨i, rfl⟩, - exact (mem_coe _).mpr (cf i), + exact set_like.mem_coe.mpr (cf i), end lemma mem_span_C_coeff : diff --git a/src/data/set_like.lean b/src/data/set_like.lean new file mode 100644 index 0000000000000..a09a0c0b04a67 --- /dev/null +++ b/src/data/set_like.lean @@ -0,0 +1,114 @@ +/- +Copyright (c) 2021 Eric Wieser. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eric Wieser +-/ +import data.set.basic + +/-! +# Typeclass for a type `A` with an injective map to `set B` + +This typecalss is primary for use by subobjects like `submonoid` and `submodule`. + +A typical subobject should be declared as: +``` +structure my_subobject (X : Type*) := +(carrier : set X) +(op_mem : ∀ {x : X}, x ∈ carrier → sorry ∈ carrier) + +namespace my_subobject + +instance : set_like (my_subobject R) M := +⟨sub_mul_action.carrier, λ p q h, by cases p; cases q; congr'⟩ + +@[simp] lemma mem_carrier {p : my_subobject R} : x ∈ p.carrier ↔ x ∈ (p : set M) := iff.rfl + +@[ext] theorem ext {p q : my_subobject R} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h + +end my_subobject +``` + +This file will then provide a `coe_sort`, a `coe` to set, a `partial_order`, and various +extensionality and simp lemmas. + +-/ +set_option old_structure_cmd true + +/-- A class to indicate that there is a canonical injection between `A` and `set B`. -/ +@[protect_proj] +class set_like (A : Type*) (B : out_param $ Type*) := +(coe : A → set B) +(coe_injective' : function.injective coe) + +namespace set_like + +variables {A : Type*} {B : Type*} [i : set_like A B] + +include i + +instance : has_coe_t A (set B) := ⟨set_like.coe⟩ + +@[priority 100] +instance : has_mem B A := ⟨λ x p, x ∈ (p : set B)⟩ + +-- `dangerous_instance` does not know that `B` is used only as an `out_param` +@[nolint dangerous_instance, priority 100] +instance : has_coe_to_sort A := ⟨_, λ p, {x : B // x ∈ p}⟩ + +variables (p q : A) + +@[simp, norm_cast] theorem coe_sort_coe : ↥(p : set B) = 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 : function.injective (coe : A → set B) := +λ x y h, set_like.coe_injective' h + +@[simp, norm_cast] theorem coe_set_eq : (p : set B) = q ↔ p = q := coe_injective.eq_iff + +theorem ext' (h : (p : set B) = q) : p = q := coe_injective h + +theorem ext'_iff : p = q ↔ (p : set B) = q := coe_set_eq.symm + +/-- Note: implementers of `set_like` must copy this lemma in order to tag it with `@[ext]`. -/ +theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := coe_injective $ set.ext h + +theorem ext_iff : p = q ↔ (∀ x, x ∈ p ↔ x ∈ q) := coe_injective.eq_iff.symm.trans set.ext_iff + +@[simp] theorem mem_coe {x : B} : x ∈ (p : set B) ↔ x ∈ p := iff.rfl + +@[simp, norm_cast] lemma coe_eq_coe {x y : p} : (x : B) = y ↔ x = y := subtype.ext_iff_val.symm + +@[simp, norm_cast] lemma coe_mk (x : B) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : B) = x := rfl +@[simp] lemma coe_mem (x : p) : (x : B) ∈ p := x.2 + +@[simp] protected lemma eta (x : p) (hx : (x : B) ∈ p) : (⟨x, hx⟩ : p) = x := subtype.eta x hx + +-- `dangerous_instance` does not know that `B` is used only as an `out_param` +@[nolint dangerous_instance, priority 100] +instance : partial_order A := +{ le := λ H K, ∀ ⦃x⦄, x ∈ H → x ∈ K, + .. partial_order.lift (coe : A → set B) coe_injective } + +lemma le_def {S T : A} : S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T := iff.rfl + +@[simp, norm_cast] +lemma coe_subset_coe {S T : A} : (S : set B) ⊆ T ↔ S ≤ T := iff.rfl + +@[simp, norm_cast] +lemma coe_ssubset_coe {S T : A} : (S : set B) ⊂ T ↔ S < T := iff.rfl + +lemma not_le_iff_exists : ¬(p ≤ q) ↔ ∃ x ∈ p, x ∉ q := set.not_subset + +lemma exists_of_lt : 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] + +end set_like diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 1392214309b76..650537e0402a8 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -126,7 +126,7 @@ by { ext, rw [mem_lift2, mem_bot], exact set.ext_iff.mp subtype.range_coe x } @[simp] lemma coe_top_eq_top (K : intermediate_field F E) : ↑(⊤ : intermediate_field K E) = (⊤ : intermediate_field F E) := -intermediate_field.ext'_iff.mpr (set.ext_iff.mpr (λ _, iff_of_true mem_top mem_top)) +set_like.ext_iff.mpr $ λ _, mem_lift2.trans (iff_of_true mem_top mem_top) end lattice @@ -190,7 +190,7 @@ lemma adjoin_subset_adjoin_iff {F' : Type*} [field F'] [algebra F' E] /-- `F[S][T] = F[S ∪ T]` -/ lemma adjoin_adjoin_left (T : set E) : ↑(adjoin (adjoin F S) T) = adjoin F (S ∪ T) := begin - rw intermediate_field.ext'_iff, + rw set_like.ext'_iff, change ↑(adjoin (adjoin F S) T) = _, apply set.eq_of_subset_of_subset; rw adjoin_subset_adjoin_iff; split, { rintros _ ⟨⟨x, hx⟩, rfl⟩, exact adjoin.mono _ _ _ (set.subset_union_left _ _) hx }, diff --git a/src/field_theory/finite/polynomial.lean b/src/field_theory/finite/polynomial.lean index 7f634f322450f..d90fce72f931e 100644 --- a/src/field_theory/finite/polynomial.lean +++ b/src/field_theory/finite/polynomial.lean @@ -123,7 +123,7 @@ rfl lemma map_restrict_dom_evalₗ : (restrict_degree σ K (fintype.card K - 1)).map (evalₗ K σ) = ⊤ := begin - refine top_unique (submodule.le_def'.2 $ assume e _, mem_map.2 _), + refine top_unique (set_like.le_def.2 $ assume e _, mem_map.2 _), refine ⟨∑ n : σ → K, e n • indicator n, _, _⟩, { exact sum_mem _ (assume c _, smul_mem _ _ (indicator_mem_restrict_degree _)) }, { ext n, diff --git a/src/field_theory/galois.lean b/src/field_theory/galois.lean index 7d26f61968a62..f1460cb6a2046 100644 --- a/src/field_theory/galois.lean +++ b/src/field_theory/galois.lean @@ -221,8 +221,9 @@ theorem fixing_subgroup_fixed_field [finite_dimensional F E] : begin have H_le : H ≤ (fixing_subgroup (fixed_field H)) := (le_iff_le _ _).mp (le_refl _), suffices : fintype.card H = fintype.card (fixing_subgroup (fixed_field H)), - { exact subgroup.ext' (set.eq_of_inclusion_surjective ((fintype.bijective_iff_injective_and_card - (set.inclusion H_le)).mpr ⟨set.inclusion_injective H_le, this⟩).2).symm }, + { exact set_like.coe_injective + (set.eq_of_inclusion_surjective ((fintype.bijective_iff_injective_and_card + (set.inclusion H_le)).mpr ⟨set.inclusion_injective H_le, this⟩).2).symm }, apply fintype.card_congr, refine (fixed_points.to_alg_hom_equiv H E).trans _, refine (alg_equiv_equiv_alg_hom (fixed_field H) E).symm.trans _, @@ -377,9 +378,10 @@ lemma of_separable_splitting_field [sp : p.is_splitting_field F E] (hp : p.separ begin haveI hFE : finite_dimensional F E := polynomial.is_splitting_field.finite_dimensional E p, let s := (p.map (algebra_map F E)).roots.to_finset, - have adjoin_root := intermediate_field.ext (subalgebra.ext_iff.mp (eq.trans (top_le_iff.mp - (eq.trans_le sp.adjoin_roots.symm (intermediate_field.algebra_adjoin_le_adjoin F ↑s))) - intermediate_field.top_to_subalgebra.symm)), + have adjoin_root : intermediate_field.adjoin F ↑s = ⊤, + { apply intermediate_field.to_subalgebra_injective, + rw [intermediate_field.top_to_subalgebra, ←top_le_iff, ←sp.adjoin_roots], + apply intermediate_field.algebra_adjoin_le_adjoin, }, let P : intermediate_field F E → Prop := λ K, fintype.card (K →ₐ[F] E) = findim F K, suffices : P (intermediate_field.adjoin F ↑s), { rw adjoin_root at this, diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean index 34e8eab0fb4d0..940dd417d4930 100644 --- a/src/field_theory/intermediate_field.lean +++ b/src/field_theory/intermediate_field.lean @@ -61,41 +61,30 @@ variables {K L} (S : intermediate_field K L) namespace intermediate_field -instance : has_coe (intermediate_field K L) (set L) := -⟨intermediate_field.carrier⟩ +instance : set_like (intermediate_field K L) L := +⟨intermediate_field.carrier, λ p q h, by cases p; cases q; congr'⟩ -@[simp] lemma coe_to_subalgebra : (S.to_subalgebra : set L) = S := rfl +@[simp] +lemma mem_carrier {s : intermediate_field K L} {x : L} : x ∈ s.carrier ↔ x ∈ s := iff.rfl -@[simp] lemma coe_to_subfield : (S.to_subfield : set L) = S := rfl +/-- Two intermediate fields are equal if they have the same elements. -/ +@[ext] theorem ext {S T : intermediate_field K L} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := +set_like.ext h -instance : has_coe_to_sort (intermediate_field K L) := ⟨Type*, λ S, S.carrier⟩ +@[simp] lemma coe_to_subalgebra : (S.to_subalgebra : set L) = S := rfl -instance : has_mem L (intermediate_field K L) := ⟨λ m S, m ∈ (S : set L)⟩ +@[simp] lemma coe_to_subfield : (S.to_subfield : set L) = S := rfl @[simp] lemma mem_mk (s : set L) (hK : ∀ x, algebra_map K L x ∈ s) (ho hm hz ha hn hi) (x : L) : x ∈ intermediate_field.mk s ho hm hz ha hK hn hi ↔ x ∈ s := iff.rfl -@[simp] lemma mem_coe (x : L) : x ∈ (S : set L) ↔ x ∈ S := iff.rfl - @[simp] lemma mem_to_subalgebra (s : intermediate_field K L) (x : L) : x ∈ s.to_subalgebra ↔ x ∈ s := iff.rfl @[simp] lemma mem_to_subfield (s : intermediate_field K L) (x : L) : x ∈ s.to_subfield ↔ x ∈ s := iff.rfl -/-- Two intermediate fields are equal if the underlying subsets are equal. -/ -theorem ext' ⦃s t : intermediate_field K L⦄ (h : (s : set L) = t) : s = t := -by { cases s, cases t, congr' } - -/-- Two intermediate fields are equal if and only if the underlying subsets are equal. -/ -protected theorem ext'_iff {s t : intermediate_field K L} : s = t ↔ (s : set L) = t := -⟨λ h, h ▸ rfl, λ h, ext' h⟩ - -/-- Two intermediate fields are equal if they have the same elements. -/ -@[ext] theorem ext {S T : intermediate_field K L} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := -ext' $ set.ext h - /-- An intermediate field contains the image of the smaller field. -/ theorem algebra_map_mem (x : K) : algebra_map K L x ∈ S := S.algebra_map_mem' x @@ -247,12 +236,6 @@ lemma to_subalgebra_injective {S S' : intermediate_field K L} (h : S.to_subalgebra = S'.to_subalgebra) : S = S' := by { ext, rw [← mem_to_subalgebra, ← mem_to_subalgebra, h] } -instance : partial_order (intermediate_field K L) := -{ le := λ S T, (S : set L) ⊆ T, - le_refl := λ S, set.subset.refl S, - le_trans := λ _ _ _, set.subset.trans, - le_antisymm := λ S T hst hts, ext $ λ x, ⟨@hst x, @hts x⟩ } - variables (S) lemma set_range_subset : set.range (algebra_map K L) ⊆ S := @@ -341,7 +324,7 @@ right K F L variables {F} {E} @[simp] lemma to_subalgebra_eq_iff : F.to_subalgebra = E.to_subalgebra ↔ F = E := -by { rw [subalgebra.ext_iff, intermediate_field.ext'_iff, set.ext_iff], refl } +by { rw [set_like.ext_iff, set_like.ext'_iff, set.ext_iff], refl } lemma eq_of_le_of_findim_le [finite_dimensional K L] (h_le : F ≤ E) (h_findim : findim K E ≤ findim K F) : F = E := diff --git a/src/field_theory/polynomial_galois_group.lean b/src/field_theory/polynomial_galois_group.lean index 12ef4c5b5a9c1..47bb202fbf0aa 100644 --- a/src/field_theory/polynomial_galois_group.lean +++ b/src/field_theory/polynomial_galois_group.lean @@ -43,21 +43,21 @@ namespace gal @[ext] lemma ext {σ τ : p.gal} (h : ∀ x ∈ p.root_set p.splitting_field, σ x = τ x) : σ = τ := begin refine alg_equiv.ext (λ x, (alg_hom.mem_equalizer σ.to_alg_hom τ.to_alg_hom x).mp - ((subalgebra.ext_iff.mp _ x).mpr algebra.mem_top)), + ((set_like.ext_iff.mp _ x).mpr algebra.mem_top)), rwa [eq_top_iff, ←splitting_field.adjoin_roots, algebra.adjoin_le_iff], end instance [h : fact (p.splits (ring_hom.id F))] : unique p.gal := { default := 1, uniq := λ f, alg_equiv.ext (λ x, by { obtain ⟨y, rfl⟩ := algebra.mem_bot.mp - ((subalgebra.ext_iff.mp ((is_splitting_field.splits_iff _ p).mp h.1) x).mp algebra.mem_top), + ((set_like.ext_iff.mp ((is_splitting_field.splits_iff _ p).mp h.1) x).mp algebra.mem_top), rw [alg_equiv.commutes, alg_equiv.commutes] }) } /-- If `p` splits in `F` then the `p.gal` is trivial. -/ def unique_gal_of_splits (h : p.splits (ring_hom.id F)) : unique p.gal := { default := 1, uniq := λ f, alg_equiv.ext (λ x, by { obtain ⟨y, rfl⟩ := algebra.mem_bot.mp - ((subalgebra.ext_iff.mp ((is_splitting_field.splits_iff _ p).mp h) x).mp algebra.mem_top), + ((set_like.ext_iff.mp ((is_splitting_field.splits_iff _ p).mp h) x).mp algebra.mem_top), rw [alg_equiv.commutes, alg_equiv.commutes] }) } instance unique_gal_zero : unique (0 : polynomial F).gal := @@ -172,7 +172,7 @@ begin intros ϕ hϕ, let equalizer := alg_hom.equalizer ϕ.to_alg_hom (alg_hom.id F p.splitting_field), suffices : equalizer = ⊤, - { exact alg_equiv.ext (λ x, (subalgebra.ext_iff.mp this x).mpr algebra.mem_top) }, + { exact alg_equiv.ext (λ x, (set_like.ext_iff.mp this x).mpr algebra.mem_top) }, rw [eq_top_iff, ←splitting_field.adjoin_roots, algebra.adjoin_le_iff], intros x hx, have key := equiv.perm.ext_iff.mp hϕ (roots_equiv_roots p E ⟨x, hx⟩), @@ -210,7 +210,7 @@ begin dsimp only [restrict_prod, restrict_dvd] at hfg, simp only [dif_neg hpq, monoid_hom.prod_apply, prod.mk.inj_iff] at hfg, suffices : alg_hom.equalizer f.to_alg_hom g.to_alg_hom = ⊤, - { exact alg_equiv.ext (λ x, (subalgebra.ext_iff.mp this x).mpr algebra.mem_top) }, + { exact alg_equiv.ext (λ x, (set_like.ext_iff.mp this x).mpr algebra.mem_top) }, rw [eq_top_iff, ←splitting_field.adjoin_roots, algebra.adjoin_le_iff], intros x hx, rw [map_mul, polynomial.roots_mul] at hx, diff --git a/src/field_theory/splitting_field.lean b/src/field_theory/splitting_field.lean index 736cf359d3c47..a744680255b0c 100644 --- a/src/field_theory/splitting_field.lean +++ b/src/field_theory/splitting_field.lean @@ -446,8 +446,9 @@ alg_equiv.symm $ alg_equiv.of_bijective ⟨(alg_hom.injective_cod_restrict _ _ _).2 $ (alg_hom.injective_iff _).2 $ λ p, adjoin_root.induction_on _ p $ λ p hp, ideal.quotient.eq_zero_iff_mem.2 $ ideal.mem_span_singleton.2 $ minpoly.dvd F x hp, - λ y, let ⟨p, _, hp⟩ := (subalgebra.ext_iff.1 (algebra.adjoin_singleton_eq_range F x) y).1 y.2 in - ⟨adjoin_root.mk _ p, subtype.eq hp⟩⟩ + λ y, + let ⟨p, _, hp⟩ := (set_like.ext_iff.1 (algebra.adjoin_singleton_eq_range F x) (y : R)).1 y.2 in + ⟨adjoin_root.mk _ p, subtype.eq hp⟩⟩ open finset @@ -709,7 +710,7 @@ theorem splits_iff (f : polynomial K) [is_splitting_field K L f] : ⟨λ h, eq_bot_iff.2 $ adjoin_roots L f ▸ (roots_map (algebra_map K L) h).symm ▸ algebra.adjoin_le_iff.2 (λ y hy, let ⟨x, hxs, hxy⟩ := finset.mem_image.1 (by rwa multiset.to_finset_map at hy) in - hxy ▸ subalgebra.mem_coe.2 $ subalgebra.algebra_map_mem _ _), + hxy ▸ set_like.mem_coe.2 $ subalgebra.algebra_map_mem _ _), λ h, @ring_equiv.to_ring_hom_refl K _ ▸ ring_equiv.trans_symm (ring_equiv.of_bijective _ $ algebra.bijective_algebra_map_iff.2 h) ▸ by { rw ring_equiv.to_ring_hom_trans, exact splits_comp_of_splits _ _ (splits L f) }⟩ diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean index 684e288910f7c..b703e7370d1f4 100644 --- a/src/field_theory/subfield.lean +++ b/src/field_theory/subfield.lean @@ -84,14 +84,19 @@ def to_add_subgroup (s : subfield K) : add_subgroup K := def to_submonoid (s : subfield K) : submonoid K := { ..s.to_subring.to_submonoid } -instance : has_coe (subfield K) (set K) := ⟨subfield.carrier⟩ -@[simp] lemma coe_to_subring (s : subfield K) : (s.to_subring : set K) = s := -rfl +instance : set_like (subfield K) K := +⟨subfield.carrier, λ p q h, by cases p; cases q; congr'⟩ + +@[simp] +lemma mem_carrier {s : subfield K} {x : K} : x ∈ s.carrier ↔ x ∈ s := iff.rfl -instance : has_coe_to_sort (subfield K) := ⟨Type*, λ S, S.carrier⟩ +/-- Two subfields are equal if they have the same elements. -/ +@[ext] theorem ext {S T : subfield K} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := set_like.ext h -instance : has_mem K (subfield K) := ⟨λ m S, m ∈ (S : set K)⟩ + +@[simp] lemma coe_to_subring (s : subfield K) : (s.to_subring : set K) = s := +rfl @[simp] lemma mem_mk (s : set K) (ho hm hz ha hn hi) (x : K) : x ∈ subfield.mk s ho hm hz ha hn hi ↔ x ∈ s := iff.rfl @@ -101,14 +106,6 @@ instance : has_mem K (subfield K) := ⟨λ m S, m ∈ (S : set K)⟩ end subfield -protected lemma subfield.exists {s : subfield K} {p : s → Prop} : - (∃ x : s, p x) ↔ ∃ x ∈ s, p ⟨x, ‹x ∈ s›⟩ := -set_coe.exists - -protected lemma subfield.forall {s : subfield K} {p : s → Prop} : - (∀ x : s, p x) ↔ ∀ x ∈ s, p ⟨x, ‹x ∈ s›⟩ := -set_coe.forall - /-- A `subring` containing inverses is a `subfield`. -/ def subring.to_subfield (s : subring K) (hinv : ∀ x ∈ s, x⁻¹ ∈ s) : subfield K := { inv_mem' := hinv @@ -118,17 +115,6 @@ namespace subfield variables (s t : subfield K) -/-- Two subfields are equal if the underlying subsets are equal. -/ -theorem ext' ⦃s t : subfield K⦄ (h : (s : set K) = t) : s = t := -by { cases s, cases t, congr' } - -/-- Two subfields are equal if and only if the underlying subsets are equal. -/ -protected theorem ext'_iff {s t : subfield K} : s = t ↔ (s : set K) = t := -⟨λ h, h ▸ rfl, λ h, ext' h⟩ - -/-- Two subfields are equal if they have the same elements. -/ -@[ext] theorem ext {S T : subfield K} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := ext' $ set.ext h - /-- A subfield contains the ring's 1. -/ theorem one_mem : (1 : K) ∈ s := s.one_mem' @@ -225,26 +211,8 @@ instance to_algebra : algebra s K := ring_hom.to_algebra s.subtype /-! # Partial order -/ -instance : partial_order (subfield K) := -{ le := λ s t, ∀ ⦃x⦄, x ∈ s → x ∈ t, - .. partial_order.lift (coe : subfield K → set K) ext' } - -variables {s t} - -lemma le_def : s ≤ t ↔ ∀ ⦃x : K⦄, x ∈ s → x ∈ t := iff.rfl - -@[simp, norm_cast] lemma coe_subset_coe : (s : set K) ⊆ t ↔ s ≤ t := iff.rfl - -@[simp, norm_cast] lemma coe_ssubset_coe : (s : set K) ⊂ t ↔ s < t := iff.rfl - -@[simp, norm_cast] -lemma mem_coe {m : K} : m ∈ (s : set K) ↔ m ∈ s := iff.rfl - variables (s t) -@[simp, norm_cast] -lemma coe_coe (s : subfield K) : ↥(s : set K) = s := rfl - @[simp] lemma mem_to_submonoid {s : subfield K} {x : K} : x ∈ s.to_submonoid ↔ x ∈ s := iff.rfl @[simp] lemma coe_to_submonoid : (s.to_submonoid : set K) = s := rfl @[simp] lemma mem_to_add_subgroup {s : subfield K} {x : K} : @@ -295,7 +263,7 @@ def map (s : subfield K) : subfield L := set.mem_image_iff_bex lemma map_map (g : L →+* M) (f : K →+* L) : (s.map f).map g = s.map (g.comp f) := -ext' $ set.image_image _ _ _ +set_like.ext' $ set.image_image _ _ _ lemma map_le_iff_le_comap {f : K →+* L} {s : subfield K} {t : subfield L} : s.map f ≤ t ↔ s ≤ t.comap f := @@ -381,7 +349,7 @@ end lemma is_glb_Inf (S : set (subfield K)) : is_glb S (Inf S) := begin - refine is_glb.of_image (λ s t, show (s : set K) ≤ t ↔ s ≤ t, from coe_subset_coe) _, + refine is_glb.of_image (λ s t, show (s : set K) ≤ t ↔ s ≤ t, from set_like.coe_subset_coe) _, convert is_glb_binfi, exact coe_Inf _ end @@ -519,7 +487,7 @@ lemma comap_infi {ι : Sort*} (f : K →+* L) (s : ι → subfield L) : lemma mem_supr_of_directed {ι} [hι : nonempty ι] {S : ι → subfield K} (hS : directed (≤) S) {x : K} : x ∈ (⨆ i, S i) ↔ ∃ i, x ∈ S i := begin - refine ⟨_, λ ⟨i, hi⟩, (le_def.1 $ le_supr S i) hi⟩, + refine ⟨_, λ ⟨i, hi⟩, (set_like.le_def.1 $ le_supr S i) hi⟩, suffices : x ∈ closure (⋃ i, (S i : set K)) → ∃ i, x ∈ S i, by simpa only [closure_Union, closure_eq], refine λ hx, closure_induction hx (λ x, set.mem_Union.mp) _ _ _ _ _, @@ -602,7 +570,7 @@ eq_of_eq_on_subfield_top $ hs ▸ eq_on_field_closure h lemma field_closure_preimage_le (f : K →+* L) (s : set L) : closure (f ⁻¹' s) ≤ (closure s).comap f := -closure_le.2 $ λ x hx, mem_coe.2 $ mem_comap.2 $ subset_closure hx +closure_le.2 $ λ x hx, set_like.mem_coe.2 $ mem_comap.2 $ subset_closure hx /-- The image under a ring homomorphism of the subfield generated by a set equals the subfield generated by the image of the set. -/ @@ -624,7 +592,7 @@ def inclusion {S T : subfield K} (h : S ≤ T) : S →+* T := S.subtype.cod_restrict_field _ (λ x, h x.2) @[simp] lemma field_range_subtype (s : subfield K) : s.subtype.field_range = s := -ext' $ (coe_srange _).trans subtype.range_coe +set_like.ext' $ (coe_srange _).trans subtype.range_coe end subfield @@ -635,7 +603,7 @@ variables {s t : subfield K} /-- Makes the identity isomorphism from a proof two subfields of a multiplicative monoid are equal. -/ def subfield_congr (h : s = t) : s ≃+* t := -{ map_mul' := λ _ _, rfl, map_add' := λ _ _, rfl, ..equiv.set_congr $ subfield.ext'_iff.1 h } +{ map_mul' := λ _ _, rfl, map_add' := λ _ _, rfl, ..equiv.set_congr $ set_like.ext'_iff.1 h } end ring_equiv @@ -645,6 +613,6 @@ variables {s : set K} lemma closure_preimage_le (f : K →+* L) (s : set L) : closure (f ⁻¹' s) ≤ (closure s).comap f := -closure_le.2 $ λ x hx, mem_coe.2 $ mem_comap.2 $ subset_closure hx +closure_le.2 $ λ x hx, set_like.mem_coe.2 $ mem_comap.2 $ subset_closure hx end subfield diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean index 40d9ad2044c94..f210dc945c2e9 100644 --- a/src/group_theory/coset.lean +++ b/src/group_theory/coset.lean @@ -130,11 +130,11 @@ mem_right_coset a (one_mem s) @[to_additive mem_left_add_coset_left_add_coset] lemma mem_left_coset_left_coset {a : α} (ha : a *l s = s) : a ∈ s := -by rw [←submonoid.mem_coe, ←ha]; exact mem_own_left_coset s a +by rw [←set_like.mem_coe, ←ha]; exact mem_own_left_coset s a @[to_additive mem_right_add_coset_right_add_coset] lemma mem_right_coset_right_coset {a : α} (ha : (s : set α) *r a = s) : a ∈ s := -by rw [←submonoid.mem_coe, ←ha]; exact mem_own_right_coset s a +by rw [←set_like.mem_coe, ←ha]; exact mem_own_right_coset s a end coset_submonoid @@ -284,7 +284,7 @@ lemma preimage_image_coe (N : subgroup α) (s : set α) : coe ⁻¹' ((coe : α → quotient N) '' s) = ⋃ x : N, (λ y : α, y * x) '' s := begin ext x, - simp only [quotient_group.eq, subgroup.exists, exists_prop, set.mem_preimage, set.mem_Union, + simp only [quotient_group.eq, set_like.exists, exists_prop, set.mem_preimage, set.mem_Union, set.mem_image, subgroup.coe_mk, ← eq_inv_mul_iff_mul_eq], exact ⟨λ ⟨y, hs, hN⟩, ⟨_, hN, y, hs, rfl⟩, λ ⟨z, hN, y, hs, hyz⟩, ⟨y, hs, hyz ▸ hN⟩⟩ end diff --git a/src/group_theory/group_action/sub_mul_action.lean b/src/group_theory/group_action/sub_mul_action.lean index 7112d739aaf46..81abf2bde26e5 100644 --- a/src/group_theory/group_action/sub_mul_action.lean +++ b/src/group_theory/group_action/sub_mul_action.lean @@ -3,9 +3,10 @@ Copyright (c) 2020 Eric Wieser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ -import group_theory.group_action.basic import algebra.group_action_hom import algebra.module.basic +import data.set_like +import group_theory.group_action.basic /-! # Sets invariant to a `mul_action` @@ -43,37 +44,19 @@ namespace sub_mul_action variables [has_scalar R M] -instance : has_coe_t (sub_mul_action R M) (set M) := ⟨λ s, s.carrier⟩ -instance : has_mem M (sub_mul_action R M) := ⟨λ x p, x ∈ (p : set M)⟩ -instance : has_coe_to_sort (sub_mul_action R M) := ⟨_, λ p, {x : M // x ∈ p}⟩ +instance : set_like (sub_mul_action R M) M := +⟨sub_mul_action.carrier, λ p q h, by cases p; cases q; congr'⟩ -instance : has_top (sub_mul_action R M) := -⟨{ carrier := set.univ, smul_mem' := λ _ _ _, set.mem_univ _ }⟩ +@[simp] lemma mem_carrier {p : sub_mul_action R M} {x : M} : x ∈ p.carrier ↔ x ∈ (p : set M) := +iff.rfl + +@[ext] theorem ext {p q : sub_mul_action R M} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h instance : has_bot (sub_mul_action R M) := ⟨{ carrier := ∅, smul_mem' := λ c, set.not_mem_empty}⟩ instance : inhabited (sub_mul_action R M) := ⟨⊥⟩ -variables (p q : sub_mul_action 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 : sub_mul_action 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 - -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 - end sub_mul_action namespace sub_mul_action @@ -84,22 +67,14 @@ variables [has_scalar R M] variables (p : sub_mul_action R M) variables {r : R} {x : M} -@[simp] theorem mem_coe : x ∈ (p : set M) ↔ x ∈ p := iff.rfl - lemma smul_mem (r : R) (h : x ∈ p) : r • x ∈ p := p.smul_mem' r h instance : has_scalar R p := { smul := λ c x, ⟨c • x.1, smul_mem _ c x.2⟩ } 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_smul (r : R) (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 - -variables {p} - -@[simp] protected lemma eta (x : p) (hx : (x : M) ∈ p) : (⟨x, hx⟩ : p) = x := subtype.eta x hx variables (p) diff --git a/src/group_theory/monoid_localization.lean b/src/group_theory/monoid_localization.lean index 62272387ffb01..0e11e10162039 100644 --- a/src/group_theory/monoid_localization.lean +++ b/src/group_theory/monoid_localization.lean @@ -927,7 +927,7 @@ a localization map for `S` and `k : P ≃* M` is an isomorphism of `comm_monoid` def of_mul_equiv_of_dom {k : P ≃* M} (H : T.map k.to_monoid_hom = S) : localization_map T N := let H' : S.comap k.to_monoid_hom = T := - H ▸ (submonoid.ext' $ T.1.preimage_image_eq k.to_equiv.injective) in + H ▸ (set_like.coe_injective $ T.1.preimage_image_eq k.to_equiv.injective) in (f.to_map.comp k.to_monoid_hom).to_localization_map (λ y, let ⟨z, hz⟩ := f.map_units ⟨k y, H ▸ set.mem_image_of_mem k y.2⟩ in ⟨z, hz⟩) (λ z, let ⟨x, hx⟩ := f.surj z in let ⟨v, hv⟩ := k.to_equiv.surjective x.1 in diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean index 8064635a08969..bf5ee0beb80fe 100644 --- a/src/group_theory/order_of_element.lean +++ b/src/group_theory/order_of_element.lean @@ -513,7 +513,7 @@ variable (a) /-- TODO: Generalise to `submonoid.powers`.-/ lemma image_range_order_of [decidable_eq α] : finset.image (λ i, a ^ i) (finset.range (order_of a)) = (gpowers a : set α).to_finset := -by { ext x, rw [set.mem_to_finset, mem_coe, mem_gpowers_iff_mem_range_order_of] } +by { ext x, rw [set.mem_to_finset, set_like.mem_coe, mem_gpowers_iff_mem_range_order_of] } open nat @@ -566,7 +566,7 @@ lemma is_cyclic_of_order_of_eq_card [fintype α] (x : α) begin classical, use x, - simp_rw ← mem_coe, + simp_rw ← set_like.mem_coe, rw ← set.eq_univ_iff_forall, apply set.eq_of_subset_of_card_le (set.subset_univ _), rw [fintype.card_congr (equiv.set.univ α), ← hx, order_eq_card_gpowers], @@ -699,7 +699,7 @@ variables [decidable_eq α] [fintype α] lemma is_cyclic.image_range_order_of (ha : ∀ x : α, x ∈ gpowers a) : finset.image (λ i, a ^ i) (range (order_of a)) = univ := begin - simp_rw [←subgroup.mem_coe] at ha, + simp_rw [←set_like.mem_coe] at ha, simp only [image_range_order_of, set.eq_univ_iff_forall.mpr ha], convert set.to_finset_univ end diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean index 4961c7c1f0122..cd7d21ba756ad 100644 --- a/src/group_theory/subgroup.lean +++ b/src/group_theory/subgroup.lean @@ -140,26 +140,14 @@ subgroup G ≃ add_subgroup (additive G) := namespace subgroup @[to_additive] -instance : has_coe (subgroup G) (set G) := { coe := subgroup.carrier } +instance : set_like (subgroup G) G := +⟨subgroup.carrier, λ p q h, by cases p; cases q; congr'⟩ @[simp, to_additive] -lemma coe_to_submonoid (K : subgroup G) : (K.to_submonoid : set G) = K := rfl - -@[to_additive] -instance : has_mem G (subgroup G) := ⟨λ m K, m ∈ (K : set G)⟩ - -@[to_additive] -instance : has_coe_to_sort (subgroup G) := ⟨_, λ G, (G : Type*)⟩ - -@[simp, norm_cast, to_additive] -lemma mem_coe {K : subgroup G} {g : G} : g ∈ (K : set G) ↔ g ∈ K := iff.rfl +lemma mem_carrier {s : subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s := iff.rfl -@[simp, norm_cast, to_additive] -lemma coe_coe (K : subgroup G) : ↥(K : set G) = K := rfl - --- note that `to_additive` transfers the `simp` attribute over but not the `norm_cast` attribute -attribute [norm_cast] add_subgroup.mem_coe -attribute [norm_cast] add_subgroup.coe_coe +@[simp, to_additive] +lemma coe_to_submonoid (K : subgroup G) : (K.to_submonoid : set G) = K := rfl @[to_additive] instance (K : subgroup G) [d : decidable_pred K.carrier] [fintype G] : fintype K := @@ -167,15 +155,6 @@ show fintype {g : G // g ∈ K.carrier}, from infer_instance end subgroup -@[to_additive] -protected lemma subgroup.exists {K : subgroup G} {p : K → Prop} : - (∃ x : K, p x) ↔ ∃ x ∈ K, p ⟨x, ‹x ∈ K›⟩ := -set_coe.exists - -@[to_additive] -protected lemma subgroup.forall {K : subgroup G} {p : K → Prop} : - (∀ x : K, p x) ↔ ∀ x ∈ K, p ⟨x, ‹x ∈ K›⟩ := -set_coe.forall namespace subgroup @@ -191,20 +170,9 @@ protected def copy (K : subgroup G) (s : set G) (hs : s = K) : subgroup G := mul_mem' := hs.symm ▸ K.mul_mem', inv_mem' := hs.symm ▸ K.inv_mem' } -/- Two subgroups are equal if the underlying set are the same. -/ -@[to_additive "Two `add_group`s are equal if the underlying subsets are equal."] -theorem ext' {H K : subgroup G} (h : (H : set G) = K) : H = K := -by { cases H, cases K, congr, exact h } - -/- Two subgroups are equal if and only if the underlying subsets are equal. -/ -@[to_additive "Two `add_subgroup`s are equal if and only if the underlying subsets are equal."] -protected theorem ext'_iff {H K : subgroup G} : - H = K ↔ (H : set G) = K := ⟨λ h, h ▸ rfl, ext'⟩ - /-- Two subgroups are equal if they have the same elements. -/ @[ext, to_additive "Two `add_subgroup`s are equal if they have the same elements."] -theorem ext {H K : subgroup G} - (h : ∀ x, x ∈ H ↔ x ∈ K) : H = K := ext' $ set.ext h +theorem ext {H K : subgroup G} (h : ∀ x, x ∈ H ↔ x ∈ K) : H = K := set_like.ext h attribute [ext] add_subgroup.ext @@ -334,15 +302,6 @@ coe_subtype H ▸ monoid_hom.map_pow _ _ _ @[simp, norm_cast] lemma coe_gpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = x ^ n := coe_subtype H ▸ monoid_hom.map_gpow _ _ _ -@[to_additive] -instance : has_le (subgroup G) := ⟨λ H K, ∀ ⦃x⦄, x ∈ H → x ∈ K⟩ - -@[to_additive] -lemma le_def {H K : subgroup G} : H ≤ K ↔ ∀ ⦃x : G⦄, x ∈ H → x ∈ K := iff.rfl - -@[simp, to_additive] -lemma coe_subset_coe {H K : subgroup G} : (H : set G) ⊆ K ↔ H ≤ K := iff.rfl - /-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/ @[to_additive "The inclusion homomorphism from a additive subgroup `H` contained in `K` to `K`."] def inclusion {H K : subgroup G} (h : H ≤ K) : H →* K := @@ -357,10 +316,6 @@ lemma subtype_comp_inclusion {H K : subgroup G} (hH : H ≤ K) : K.subtype.comp (inclusion hH) = H.subtype := by { ext, simp } -@[to_additive] -instance : partial_order (subgroup G) := -{ le := (≤), - .. partial_order.lift (coe : subgroup G → set G) (λ a b, ext') } /-- The subgroup `G` of the group `G`. -/ @[to_additive "The `add_subgroup G` of the `add_group G`."] @@ -468,7 +423,7 @@ instance : complete_lattice (subgroup G) := inf_le_left := λ a b x, and.left, inf_le_right := λ a b x, and.right, .. complete_lattice_of_Inf (subgroup G) $ λ s, is_glb.of_image - (λ H K, show (H : set G) ≤ K ↔ H ≤ K, from coe_subset_coe) is_glb_binfi } + (λ H K, show (H : set G) ≤ K ↔ H ≤ K, from set_like.coe_subset_coe) is_glb_binfi } @[to_additive] lemma mem_sup_left {S T : subgroup G} : ∀ {x : G}, x ∈ S → x ∈ S ⊔ T := @@ -646,7 +601,7 @@ lemma mem_supr_of_directed {ι} [hι : nonempty ι] {K : ι → subgroup G} (hK {x : G} : x ∈ (supr K : subgroup G) ↔ ∃ i, x ∈ K i := begin - refine ⟨_, λ ⟨i, hi⟩, (le_def.1 $ le_supr K i) hi⟩, + refine ⟨_, λ ⟨i, hi⟩, (set_like.le_def.1 $ le_supr K i) hi⟩, suffices : x ∈ closure (⋃ i, (K i : set G)) → ∃ i, x ∈ K i, by simpa only [closure_Union, closure_eq (K _)] using this, refine (λ hx, closure_induction hx (λ _, mem_Union.1) _ _ _), @@ -713,7 +668,7 @@ mem_image_iff_bex @[to_additive] lemma map_map (g : N →* P) (f : G →* N) : (K.map f).map g = K.map (g.comp f) := -ext' $ image_image _ _ _ +set_like.coe_injective $ image_image _ _ _ @[to_additive] lemma map_le_iff_le_comap {f : G →* N} {K : subgroup G} {H : subgroup N} : @@ -798,7 +753,7 @@ lemma top_prod_top : (⊤ : subgroup G).prod (⊤ : subgroup N) = ⊤ := (top_prod _).trans $ comap_top _ @[to_additive] lemma bot_prod_bot : (⊥ : subgroup G).prod (⊥ : subgroup N) = ⊥ := -ext' $ by simp [coe_prod, prod.one_eq_mk] +set_like.coe_injective $ by simp [coe_prod, prod.one_eq_mk] /-- Product of subgroups is isomorphic to their product as groups. -/ @[to_additive prod_equiv "Product of additive subgroups is isomorphic to their product @@ -1111,7 +1066,7 @@ by rw [range_eq_map, range_eq_map]; exact (⊤ : subgroup G).map_map g f @[to_additive] lemma range_top_iff_surjective {N} [group N] {f : G →* N} : f.range = (⊤ : subgroup N) ↔ function.surjective f := -subgroup.ext'_iff.trans $ iff.trans (by rw [coe_range, coe_top]) set.range_iff_surjective +set_like.ext'_iff.trans $ iff.trans (by rw [coe_range, coe_top]) set.range_iff_surjective /-- The range of a surjective monoid homomorphism is the whole of the codomain. -/ @[to_additive "The range of a surjective `add_monoid` homomorphism is the whole of the codomain."] @@ -1187,7 +1142,7 @@ eq_of_eq_on_top $ hs ▸ eq_on_closure h @[to_additive] lemma gclosure_preimage_le (f : G →* N) (s : set N) : closure (f ⁻¹' s) ≤ (closure s).comap f := -(closure_le _).2 $ λ x hx, by rw [mem_coe, mem_comap]; exact subset_closure hx +(closure_le _).2 $ λ x hx, by rw [set_like.mem_coe, mem_comap]; exact subset_closure hx /-- The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup generated by the image of the set. -/ @@ -1409,7 +1364,7 @@ variables {H K : subgroup G} @[to_additive "Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal."] def subgroup_congr (h : H = K) : H ≃* K := -{ map_mul' := λ _ _, rfl, ..equiv.set_congr $ subgroup.ext'_iff.1 h } +{ map_mul' := λ _ _, rfl, ..equiv.set_congr $ congr_arg _ h } end mul_equiv @@ -1439,7 +1394,7 @@ by rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem _ @[to_additive] lemma mem_sup' : x ∈ s ⊔ t ↔ ∃ (y : s) (z : t), (y:C) * z = x := -mem_sup.trans $ by simp only [subgroup.exists, coe_mk] +mem_sup.trans $ by simp only [set_like.exists, coe_mk] @[to_additive] instance : is_modular_lattice (subgroup C) := @@ -1461,8 +1416,8 @@ namespace subgroup @[to_additive] lemma closure_mul_le (S T : set G) : 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 : subgroup G) : H ⊔ K = closure (H * K) := diff --git a/src/group_theory/submonoid/basic.lean b/src/group_theory/submonoid/basic.lean index a5b024b75e518..ccfd9b80eaa04 100644 --- a/src/group_theory/submonoid/basic.lean +++ b/src/group_theory/submonoid/basic.lean @@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzza Amelia Livingston, Yury Kudryashov -/ import data.set.lattice +import data.set_like /-! # Submonoids: definition and `complete_lattice` structure @@ -68,50 +69,16 @@ attribute [to_additive] submonoid namespace submonoid @[to_additive] -instance : has_coe (submonoid M) (set M) := ⟨submonoid.carrier⟩ - - -@[to_additive] -instance : has_mem M (submonoid M) := ⟨λ m S, m ∈ (S:set M)⟩ - -@[to_additive] -instance : has_coe_to_sort (submonoid M) := ⟨Type*, λ S, {x : M // x ∈ S}⟩ +instance : set_like (submonoid M) M := +⟨submonoid.carrier, λ p q h, by cases p; cases q; congr'⟩ @[simp, to_additive] lemma mem_carrier {s : submonoid M} {x : M} : x ∈ s.carrier ↔ x ∈ s := iff.rfl -@[simp, norm_cast, to_additive] -lemma mem_coe {S : submonoid M} {m : M} : m ∈ (S : set M) ↔ m ∈ S := iff.rfl - -@[simp, norm_cast, to_additive] -lemma coe_coe (s : submonoid M) : ↥(s : set M) = s := rfl - -attribute [norm_cast] add_submonoid.mem_coe add_submonoid.coe_coe - -@[to_additive] -protected lemma «exists» {s : submonoid M} {p : s → Prop} : - (∃ x : s, p x) ↔ ∃ x ∈ s, p ⟨x, ‹x ∈ s›⟩ := -set_coe.exists - -@[to_additive] -protected lemma «forall» {s : submonoid M} {p : s → Prop} : - (∀ x : s, p x) ↔ ∀ x ∈ s, p ⟨x, ‹x ∈ s›⟩ := -set_coe.forall - -/-- Two submonoids are equal if the underlying subsets are equal. -/ -@[to_additive "Two `add_submonoid`s are equal if the underlying subsets are equal."] -theorem ext' ⦃S T : submonoid M⦄ (h : (S : set M) = T) : S = T := -by cases S; cases T; congr' - -/-- Two submonoids are equal if and only if the underlying subsets are equal. -/ -@[to_additive "Two `add_submonoid`s are equal if and only if the underlying subsets are equal."] -protected theorem ext'_iff {S T : submonoid M} : S = T ↔ (S : set M) = T := -⟨λ h, h ▸ rfl, λ h, ext' h⟩ - /-- Two submonoids are equal if they have the same elements. -/ @[ext, to_additive "Two `add_submonoid`s are equal if they have the same elements."] theorem ext {S T : submonoid M} - (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := ext' $ set.ext h + (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := set_like.ext h attribute [ext] add_submonoid.ext @@ -127,7 +94,8 @@ variable {S : submonoid M} @[simp, to_additive] lemma coe_copy {s : set M} (hs : s = S) : (S.copy s hs : set M) = s := rfl -@[to_additive] lemma copy_eq {s : set M} (hs : s = S) : S.copy s hs = S := ext' hs +@[to_additive] lemma copy_eq {s : set M} (hs : s = S) : S.copy s hs = S := +set_like.coe_injective hs variable (S) @@ -139,30 +107,6 @@ theorem one_mem : (1 : M) ∈ S := S.one_mem' @[to_additive "An `add_submonoid` is closed under addition."] theorem mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S := submonoid.mul_mem' S -@[to_additive] lemma coe_injective : function.injective (coe : S → M) := subtype.val_injective - -@[simp, to_additive] lemma coe_eq_coe (x y : S) : (x : M) = y ↔ x = y := set_coe.ext_iff -attribute [norm_cast] coe_eq_coe add_submonoid.coe_eq_coe - -@[to_additive] -instance : has_le (submonoid M) := ⟨λ S T, ∀ ⦃x⦄, x ∈ S → x ∈ T⟩ - -@[to_additive] -lemma le_def {S T : submonoid M} : S ≤ T ↔ ∀ ⦃x : M⦄, x ∈ S → x ∈ T := iff.rfl - -@[simp, norm_cast, to_additive] -lemma coe_subset_coe {S T : submonoid M} : (S : set M) ⊆ T ↔ S ≤ T := iff.rfl - -@[to_additive] -instance : partial_order (submonoid M) := -{ le := λ S T, ∀ ⦃x⦄, x ∈ S → x ∈ T, - .. partial_order.lift (coe : submonoid M → set M) ext' } - -@[simp, norm_cast, to_additive] -lemma coe_ssubset_coe {S T : submonoid M} : (S : set M) ⊂ T ↔ S < T := iff.rfl - -attribute [norm_cast] add_submonoid.coe_subset_coe add_submonoid.coe_ssubset_coe - /-- The submonoid `M` of the monoid `M`. -/ @[to_additive "The additive submonoid `M` of the `add_monoid M`."] instance : has_top (submonoid M) := @@ -244,7 +188,8 @@ instance : complete_lattice (submonoid M) := inf_le_left := λ a b x, and.left, inf_le_right := λ a b x, and.right, .. complete_lattice_of_Inf (submonoid M) $ λ s, - is_glb.of_image (λ S T, show (S : set M) ≤ T ↔ S ≤ T, from coe_subset_coe) is_glb_binfi } + is_glb.of_image (λ S T, + show (S : set M) ≤ T ↔ S ≤ T, from set_like.coe_subset_coe) is_glb_binfi } @[to_additive] lemma subsingleton_iff : subsingleton M ↔ subsingleton (submonoid M) := diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean index 96866f8dc4ce2..f50172080f405 100644 --- a/src/group_theory/submonoid/membership.lean +++ b/src/group_theory/submonoid/membership.lean @@ -93,7 +93,7 @@ lemma mem_supr_of_directed {ι} [hι : nonempty ι] {S : ι → submonoid M} (hS {x : M} : x ∈ (⨆ i, S i) ↔ ∃ i, x ∈ S i := begin - refine ⟨_, λ ⟨i, hi⟩, (le_def.1 $ le_supr S i) hi⟩, + refine ⟨_, λ ⟨i, hi⟩, (set_like.le_def.1 $ le_supr S i) hi⟩, suffices : x ∈ closure (⋃ i, (S i : set M)) → ∃ i, x ∈ S i, by simpa only [closure_Union, closure_eq (S _)] using this, refine (λ hx, closure_induction hx (λ _, mem_Union.1) _ _), @@ -219,7 +219,7 @@ by rw [mrange, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_i @[to_additive] lemma mem_sup {s t : submonoid N} {x : N} : x ∈ s ⊔ t ↔ ∃ (y ∈ s) (z ∈ t), y * z = x := -by simp only [sup_eq_range, mem_mrange, coprod_apply, prod.exists, submonoid.exists, +by simp only [sup_eq_range, mem_mrange, coprod_apply, prod.exists, set_like.exists, coe_subtype, subtype.coe_mk] end submonoid diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean index d8db5c0757c84..6a6b9d376a23f 100644 --- a/src/group_theory/submonoid/operations.lean +++ b/src/group_theory/submonoid/operations.lean @@ -157,7 +157,7 @@ mem_image_of_mem f x.2 @[to_additive] lemma map_map (g : N →* P) (f : M →* N) : (S.map f).map g = S.map (g.comp f) := -ext' $ image_image _ _ _ +set_like.coe_injective $ image_image _ _ _ @[to_additive] lemma map_le_iff_le_comap {f : M →* N} {S : submonoid M} {T : submonoid N} : @@ -324,34 +324,34 @@ attribute [norm_cast] add_submonoid.coe_add add_submonoid.coe_zero @[to_additive "An `add_submonoid` of an `add_monoid` inherits an `add_monoid` structure."] instance to_monoid {M : Type*} [monoid M] (S : submonoid M) : monoid S := -S.coe_injective.monoid coe rfl (λ _ _, rfl) +subtype.coe_injective.monoid coe rfl (λ _ _, rfl) /-- A submonoid of a `comm_monoid` is a `comm_monoid`. -/ @[to_additive "An `add_submonoid` of an `add_comm_monoid` is an `add_comm_monoid`."] instance to_comm_monoid {M} [comm_monoid M] (S : submonoid M) : comm_monoid S := -S.coe_injective.comm_monoid coe rfl (λ _ _, rfl) +subtype.coe_injective.comm_monoid coe rfl (λ _ _, rfl) /-- A submonoid of an `ordered_comm_monoid` is an `ordered_comm_monoid`. -/ @[to_additive "An `add_submonoid` of an `ordered_add_comm_monoid` is an `ordered_add_comm_monoid`."] instance to_ordered_comm_monoid {M} [ordered_comm_monoid M] (S : submonoid M) : ordered_comm_monoid S := -S.coe_injective.ordered_comm_monoid coe rfl (λ _ _, rfl) +subtype.coe_injective.ordered_comm_monoid coe rfl (λ _ _, rfl) /-- A submonoid of a `linear_ordered_comm_monoid` is a `linear_ordered_comm_monoid`. -/ @[to_additive "An `add_submonoid` of a `linear_ordered_add_comm_monoid` is a `linear_ordered_add_comm_monoid`."] instance to_linear_ordered_comm_monoid {M} [linear_ordered_comm_monoid M] (S : submonoid M) : linear_ordered_comm_monoid S := -S.coe_injective.linear_ordered_comm_monoid coe rfl (λ _ _, rfl) +subtype.coe_injective.linear_ordered_comm_monoid coe rfl (λ _ _, rfl) /-- A submonoid of an `ordered_cancel_comm_monoid` is an `ordered_cancel_comm_monoid`. -/ @[to_additive "An `add_submonoid` of an `ordered_cancel_add_comm_monoid` is an `ordered_cancel_add_comm_monoid`."] instance to_ordered_cancel_comm_monoid {M} [ordered_cancel_comm_monoid M] (S : submonoid M) : ordered_cancel_comm_monoid S := -S.coe_injective.ordered_cancel_comm_monoid coe rfl (λ _ _, rfl) +subtype.coe_injective.ordered_cancel_comm_monoid coe rfl (λ _ _, rfl) /-- A submonoid of a `linear_ordered_cancel_comm_monoid` is a `linear_ordered_cancel_comm_monoid`. -/ @@ -359,7 +359,7 @@ S.coe_injective.ordered_cancel_comm_monoid coe rfl (λ _ _, rfl) a `linear_ordered_cancel_add_comm_monoid`."] instance to_linear_ordered_cancel_comm_monoid {M} [linear_ordered_cancel_comm_monoid M] (S : submonoid M) : linear_ordered_cancel_comm_monoid S := -S.coe_injective.linear_ordered_cancel_comm_monoid coe rfl (λ _ _, rfl) +subtype.coe_injective.linear_ordered_cancel_comm_monoid coe rfl (λ _ _, rfl) /-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/ @[to_additive "The natural monoid hom from an `add_submonoid` of `add_monoid` `M` to `M`."] @@ -433,7 +433,7 @@ lemma top_prod_top : (⊤ : submonoid M).prod (⊤ : submonoid N) = ⊤ := (top_prod _).trans $ comap_top _ @[to_additive] lemma bot_prod_bot : (⊥ : submonoid M).prod (⊥ : submonoid N) = ⊥ := -ext' $ by simp [coe_prod, prod.one_eq_mk] +set_like.coe_injective $ by simp [coe_prod, prod.one_eq_mk] /-- The product of submonoids is isomorphic to their product as monoids. -/ @[to_additive prod_equiv "The product of additive submonoids is isomorphic to their product @@ -486,7 +486,7 @@ lemma map_mrange (g : N →* P) (f : M →* N) : f.mrange.map g = (g.comp f).mra @[to_additive] lemma mrange_top_iff_surjective {N} [monoid N] {f : M →* N} : f.mrange = (⊤ : submonoid N) ↔ function.surjective f := -submonoid.ext'_iff.trans $ iff.trans (by rw [coe_mrange, coe_top]) set.range_iff_surjective +set_like.ext'_iff.trans $ iff.trans (by rw [coe_mrange, coe_top]) set.range_iff_surjective /-- The range of a surjective monoid hom is the whole of the codomain. -/ @[to_additive "The range of a surjective `add_monoid` hom is the whole of the codomain."] @@ -500,7 +500,7 @@ lemma mrange_eq_map (f : M →* N) : f.mrange = map f ⊤ := rfl @[to_additive] lemma mclosure_preimage_le (f : M →* N) (s : set N) : closure (f ⁻¹' s) ≤ (closure s).comap f := -closure_le.2 $ λ x hx, mem_coe.2 $ mem_comap.2 $ subset_closure hx +closure_le.2 $ λ x hx, set_like.mem_coe.2 $ mem_comap.2 $ subset_closure hx /-- The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set. -/ @@ -573,7 +573,7 @@ S.subtype.cod_mrestrict _ (λ x, h x.2) @[simp, to_additive] lemma range_subtype (s : submonoid M) : s.subtype.mrange = s := -ext' $ (coe_mrange _).trans $ subtype.range_coe +set_like.coe_injective $ (coe_mrange _).trans $ subtype.range_coe @[to_additive] lemma eq_top_iff' : S = ⊤ ↔ ∀ x : M, x ∈ S := eq_top_iff.trans ⟨λ h m, h $ mem_top m, λ h m _, h m⟩ @@ -636,6 +636,6 @@ variables {S} {T : submonoid M} @[to_additive "Makes the identity additive isomorphism from a proof two submonoids of an additive monoid are equal."] def submonoid_congr (h : S = T) : S ≃* T := -{ map_mul' := λ _ _, rfl, ..equiv.set_congr $ submonoid.ext'_iff.1 h } +{ map_mul' := λ _ _, rfl, ..equiv.set_congr $ congr_arg _ h } end mul_equiv diff --git a/src/linear_algebra/affine_space/affine_subspace.lean b/src/linear_algebra/affine_space/affine_subspace.lean index db8cb682b87ef..3a41f55dbf66e 100644 --- a/src/linear_algebra/affine_space/affine_subspace.lean +++ b/src/linear_algebra/affine_space/affine_subspace.lean @@ -247,7 +247,7 @@ only if it is the subtraction of two vectors in the subspace. -/ lemma mem_direction_iff_eq_vsub {s : affine_subspace k P} (h : (s : set P).nonempty) (v : V) : v ∈ s.direction ↔ ∃ p1 ∈ s, ∃ p2 ∈ s, v = p1 -ᵥ p2 := begin - rw [←submodule.mem_coe, coe_direction_eq_vsub_set h], + rw [←set_like.mem_coe, coe_direction_eq_vsub_set h], exact ⟨λ ⟨p1, p2, hp1, hp2, hv⟩, ⟨p1, hp1, p2, hp2, hv.symm⟩, λ ⟨p1, hp1, p2, hp2, hv⟩, ⟨p1, p2, hp1, hp2, hv.symm⟩⟩ end @@ -299,7 +299,7 @@ lemma coe_direction_eq_vsub_set_left {s : affine_subspace k P} {p : P} (hp : p (s.direction : set V) = (-ᵥ) p '' s := begin ext v, - rw [submodule.mem_coe, ←submodule.neg_mem_iff, ←submodule.mem_coe, + rw [set_like.mem_coe, ←submodule.neg_mem_iff, ←set_like.mem_coe, coe_direction_eq_vsub_set_right hp, set.mem_image_iff_bex, set.mem_image_iff_bex], conv_lhs { congr, funext, rw [←neg_vsub_eq_vsub_rev, neg_inj] } end @@ -309,7 +309,7 @@ if and only if it results from subtracting that point on the right. -/ lemma mem_direction_iff_eq_vsub_right {s : affine_subspace k P} {p : P} (hp : p ∈ s) (v : V) : v ∈ s.direction ↔ ∃ p2 ∈ s, v = p2 -ᵥ p := begin - rw [←submodule.mem_coe, coe_direction_eq_vsub_set_right hp], + rw [←set_like.mem_coe, coe_direction_eq_vsub_set_right hp], exact ⟨λ ⟨p2, hp2, hv⟩, ⟨p2, hp2, hv.symm⟩, λ ⟨p2, hp2, hv⟩, ⟨p2, hp2, hv.symm⟩⟩ end @@ -318,7 +318,7 @@ if and only if it results from subtracting that point on the left. -/ lemma mem_direction_iff_eq_vsub_left {s : affine_subspace k P} {p : P} (hp : p ∈ s) (v : V) : v ∈ s.direction ↔ ∃ p2 ∈ s, v = p -ᵥ p2 := begin - rw [←submodule.mem_coe, coe_direction_eq_vsub_set_left hp], + rw [←set_like.mem_coe, coe_direction_eq_vsub_set_left hp], exact ⟨λ ⟨p2, hp2, hv⟩, ⟨p2, hp2, hv.symm⟩, λ ⟨p2, hp2, hv⟩, ⟨p2, hp2, hv.symm⟩⟩ end @@ -455,8 +455,8 @@ begin have hp1s1 : p1 ∈ (s1 : set P) := set.mem_of_mem_of_subset hp1 h, refine vadd_mem_of_mem_direction _ hp1s1, have hs : vector_span k s ≤ s1.direction := vector_span_mono k h, - rw submodule.le_def at hs, - rw ←submodule.mem_coe, + rw set_like.le_def at hs, + rw ←set_like.mem_coe, exact set.mem_of_mem_of_subset hv hs end @@ -493,7 +493,7 @@ begin apply le_antisymm, { refine submodule.span_le.2 _, rintros v ⟨p1, p3, ⟨p2, hp2, v1, hv1, hp1⟩, ⟨p4, hp4, v2, hv2, hp3⟩, rfl⟩, - rw [hp1, hp3, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, submodule.mem_coe], + rw [hp1, hp3, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, set_like.mem_coe], exact (vector_span k s).sub_mem ((vector_span k s).add_mem hv1 (vsub_mem_vector_span k hp2 hp4)) hv2 }, { exact vector_span_mono k (subset_span_points k s) } @@ -748,7 +748,7 @@ begin cases hn with p hp, rw lt_iff_le_and_exists at h, rcases h with ⟨hle, p2, hp2, hp2s1⟩, - rw submodule.lt_iff_le_and_exists, + rw set_like.lt_iff_le_and_exists, use [direction_le hle, p2 -ᵥ p, vsub_mem_direction hp2 (hle hp)], intro hm, rw vsub_right_mem_direction_iff_mem hp p2 at hm, @@ -774,7 +774,7 @@ lemma sup_direction_lt_of_nonempty_of_inter_empty {s1 s2 : affine_subspace k P} begin cases h1 with p1 hp1, cases h2 with p2 hp2, - rw submodule.lt_iff_le_and_exists, + rw set_like.lt_iff_le_and_exists, use [sup_direction_le s1 s2, p2 -ᵥ p1, vsub_mem_direction ((le_sup_right : s2 ≤ s1 ⊔ s2) hp2) ((le_sup_left : s1 ≤ s1 ⊔ s2) hp1)], intro h, @@ -850,7 +850,7 @@ begin { rw submodule.span_le, rintros v ⟨p1, p2, hp1, hp2, hv⟩, rw ←vsub_sub_vsub_cancel_left p1 p2 p at hv, - rw [←hv, submodule.mem_coe, submodule.mem_span], + rw [←hv, set_like.mem_coe, submodule.mem_span], exact λ m hm, submodule.sub_mem _ (hm ⟨p2, hp2, rfl⟩) (hm ⟨p1, hp1, rfl⟩) }, { rintros v ⟨p2, hp2, hv⟩, exact ⟨p, p2, hp, hp2, hv⟩ } @@ -866,7 +866,7 @@ begin { rw submodule.span_le, rintros v ⟨p1, p2, hp1, hp2, hv⟩, rw ←vsub_sub_vsub_cancel_right p1 p2 p at hv, - rw [←hv, submodule.mem_coe, submodule.mem_span], + rw [←hv, set_like.mem_coe, submodule.mem_span], exact λ m hm, submodule.sub_mem _ (hm ⟨p1, hp1, rfl⟩) (hm ⟨p2, hp2, rfl⟩) }, { rintros v ⟨p2, hp2, hv⟩, exact ⟨p2, p, hp2, hp, hv⟩ } @@ -1036,10 +1036,10 @@ begin submodule.span_le], rintros v ⟨p3, hp3, rfl⟩, cases hp3, - { rw [sup_assoc, sup_comm, submodule.mem_coe, submodule.mem_sup], + { rw [sup_assoc, sup_comm, set_like.mem_coe, submodule.mem_sup], use [0, submodule.zero_mem _, p3 -ᵥ p1, vsub_mem_direction hp3 hp1], rw zero_add }, - { rw [sup_assoc, submodule.mem_coe, submodule.mem_sup], + { rw [sup_assoc, set_like.mem_coe, submodule.mem_sup], use [0, submodule.zero_mem _, p3 -ᵥ p1], rw [and_comm, zero_add], use rfl, diff --git a/src/linear_algebra/affine_space/finite_dimensional.lean b/src/linear_algebra/affine_space/finite_dimensional.lean index b549876d87c2e..dc4004f93cb51 100644 --- a/src/linear_algebra/affine_space/finite_dimensional.lean +++ b/src/linear_algebra/affine_space/finite_dimensional.lean @@ -316,13 +316,13 @@ begin have hs : vector_span k s ≤ k ∙ v, { rw [vector_span_eq_span_vsub_set_right k h, submodule.span_le, set.subset_def], intros x hx, - rw [submodule.mem_coe, submodule.mem_span_singleton], + rw [set_like.mem_coe, submodule.mem_span_singleton], rw set.mem_image at hx, rcases hx with ⟨p, hp, rfl⟩, rcases hp₀v p hp with ⟨r, rfl⟩, use r, simp }, - have hw' := submodule.le_def'.1 hs w hw, + have hw' := set_like.le_def.1 hs hw, rwa submodule.mem_span_singleton at hw' } end diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index 474d6b2973178..ed83da273018a 100644 --- a/src/linear_algebra/basic.lean +++ b/src/linear_algebra/basic.lean @@ -134,7 +134,7 @@ ext $ assume b, rfl /-- Restrict domain and codomain of an endomorphism. -/ def restrict (f : M →ₗ[R] M) {p : submodule R M} (hf : ∀ x ∈ p, f x ∈ p) : p →ₗ[R] p := -(f.dom_restrict p).cod_restrict p $ submodule.forall.2 hf +(f.dom_restrict p).cod_restrict p $ set_like.forall.2 hf lemma restrict_apply {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ x ∈ p, f x ∈ p) (x : p) : @@ -597,7 +597,7 @@ submodule.ext $ λ a, by simp lemma map_comp (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (p : submodule R M) : map (g.comp f) p = map g (map f p) := -submodule.coe_injective $ by simp [map_coe]; rw ← image_comp +set_like.coe_injective $ by simp [map_coe]; rw ← image_comp lemma map_mono {f : M →ₗ[R] M₂} {p p' : submodule R M} : p ≤ p' → map f p ≤ map f p' := image_subset _ @@ -623,7 +623,7 @@ def comap (f : M →ₗ[R] M₂) (p : submodule R M₂) : submodule R M := x ∈ comap f p ↔ f x ∈ p := iff.rfl lemma comap_id : comap linear_map.id p = p := -submodule.coe_injective rfl +set_like.coe_injective rfl lemma comap_comp (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (p : submodule R M₃) : comap (g.comp f) p = comap f (comap g p) := rfl @@ -739,7 +739,7 @@ end (submodule.gi R M).gc.l_bot @[simp] lemma span_univ : span R (univ : set M) = ⊤ := -eq_top_iff.2 $ le_def.2 $ subset_span +eq_top_iff.2 $ set_like.le_def.2 $ subset_span lemma span_union (s t : set M) : span R (s ∪ t) = span R s ⊔ span R t := (submodule.gi R M).gc.l_sup @@ -779,7 +779,7 @@ sum_mem _ $ λ i hi, mem_supr_of_mem i (h i) @[simp] theorem mem_supr_of_directed {ι} [nonempty ι] (S : ι → submodule R M) (H : directed (≤) S) {x} : x ∈ supr S ↔ ∃ i, x ∈ S i := -by { rw [← mem_coe, coe_supr_of_directed S H, mem_Union], refl } +by { rw [← set_like.mem_coe, coe_supr_of_directed S H, mem_Union], refl } theorem mem_Sup_of_directed {s : set (submodule R M)} {z} (hs : s.nonempty) (hdir : directed_on (≤) s) : @@ -811,7 +811,7 @@ by rintro ⟨y, hy, z, hz, rfl⟩; exact add_mem _ ((le_sup_right : p' ≤ p ⊔ p') hz)⟩ lemma mem_sup' : x ∈ p ⊔ p' ↔ ∃ (y : p) (z : p'), (y:M) + z = x := -mem_sup.trans $ by simp only [submodule.exists, coe_mk] +mem_sup.trans $ by simp only [set_like.exists, coe_mk] end @@ -842,7 +842,7 @@ by rintro ⟨a, y, rfl⟩; exact lemma le_span_singleton_iff {s : submodule R M} {v₀ : M} : s ≤ (R ∙ v₀) ↔ ∀ v ∈ s, ∃ r : R, r • v₀ = v := -by simp_rw [le_def', mem_span_singleton] +by simp_rw [set_like.le_def, mem_span_singleton] @[simp] lemma span_zero_singleton : (R ∙ (0:M)) = ⊥ := by { ext, simp [mem_span_singleton, eq_comm] } @@ -852,7 +852,7 @@ set.ext $ λ x, mem_span_singleton lemma span_singleton_smul_le (r : R) (x : M) : (R ∙ (r • x)) ≤ R ∙ x := begin - rw [span_le, set.singleton_subset_iff, mem_coe], + rw [span_le, set.singleton_subset_iff, set_like.mem_coe], exact smul_mem _ _ (mem_span_singleton_self _) end @@ -930,14 +930,14 @@ le_antisymm (span_le.mpr $ Union_subset_iff.mpr $ assume i m hm, mem_supr_of_mem i hm) lemma span_singleton_le_iff_mem (m : M) (p : submodule R M) : (R ∙ m) ≤ p ↔ m ∈ p := -by rw [span_le, singleton_subset_iff, mem_coe] +by rw [span_le, singleton_subset_iff, set_like.mem_coe] lemma singleton_span_is_compact_element (x : M) : complete_lattice.is_compact_element (span R {x} : submodule R M) := begin rw complete_lattice.is_compact_element_iff_le_of_directed_Sup_le, intros d hemp hdir hsup, - have : x ∈ Sup d, from (le_def.mp hsup) (mem_span_singleton_self x), + have : x ∈ Sup d, from (set_like.le_def.mp hsup) (mem_span_singleton_self x), obtain ⟨y, ⟨hyd, hxy⟩⟩ := (mem_Sup_of_directed hemp hdir).mp this, exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff]⟩⟩, end @@ -961,7 +961,7 @@ begin have h2 := gt_of_ge_of_gt h1 h, exact lt_irrefl I h2, }, { intro h, - apply lt_iff_le_and_exists.mpr, split, + apply set_like.lt_iff_le_and_exists.mpr, split, simp only [add_eq_sup, le_sup_left], use a, split, swap, { assumption, }, @@ -1029,14 +1029,14 @@ lemma prod_mono {p p' : submodule R M} {q q' : submodule R M₂} : p ≤ p' → q ≤ q' → prod p q ≤ prod p' q' := prod_mono @[simp] lemma prod_inf_prod : prod p q ⊓ prod p' q' = prod (p ⊓ p') (q ⊓ q') := -coe_injective set.prod_inter_prod +set_like.coe_injective set.prod_inter_prod @[simp] lemma prod_sup_prod : prod p q ⊔ prod p' q' = prod (p ⊔ p') (q ⊔ q') := begin refine le_antisymm (sup_le (prod_mono le_sup_left le_sup_left) (prod_mono le_sup_right le_sup_right)) _, - simp [le_def'], intros xx yy hxx hyy, + simp [set_like.le_def], intros xx yy hxx hyy, rcases mem_sup.1 hxx with ⟨x, hx, x', hx', rfl⟩, rcases mem_sup.1 hyy with ⟨y, hy, y', hy', rfl⟩, refine mem_sup.2 ⟨(x, y), ⟨hx, hy⟩, (x', y'), ⟨hx', hy'⟩, rfl⟩ @@ -1141,7 +1141,7 @@ by { rintros ⟨x⟩, exact ⟨x, rfl⟩ } lemma nontrivial_of_lt_top (h : p < ⊤) : nontrivial (p.quotient) := begin - obtain ⟨x, _, not_mem_s⟩ := exists_of_lt h, + obtain ⟨x, _, not_mem_s⟩ := set_like.exists_of_lt h, refine ⟨⟨mk x, 0, _⟩⟩, simpa using not_mem_s end @@ -1272,7 +1272,7 @@ theorem range_comp_le_range (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : r by rw range_comp; exact map_mono le_top theorem range_eq_top {f : M →ₗ[R] M₂} : range f = ⊤ ↔ surjective f := -by rw [submodule.ext'_iff, range_coe, top_coe, set.range_iff_surjective] +by rw [set_like.ext'_iff, range_coe, top_coe, set.range_iff_surjective] lemma range_le_iff_comap {f : M →ₗ[R] M₂} {p : submodule R M₂} : range f ≤ p ↔ comap f p = ⊤ := by rw [range, map_le_iff_le_comap, eq_top_iff] @@ -1453,10 +1453,10 @@ by simpa [disjoint] using @disjoint_ker' _ _ _ _ _ _ _ _ f ⊤ lemma ker_le_iff {p : submodule R M} : ker f ≤ p ↔ ∃ (y ∈ range f), f ⁻¹' {y} ⊆ p := begin split, - { intros h, use 0, rw [← mem_coe, f.range_coe], exact ⟨⟨0, map_zero f⟩, h⟩, }, + { intros h, use 0, rw [← set_like.mem_coe, f.range_coe], exact ⟨⟨0, map_zero f⟩, h⟩, }, { rintros ⟨y, h₁, h₂⟩, - rw le_def, intros z hz, simp only [mem_ker, mem_coe] at hz, - rw [← mem_coe, f.range_coe, set.mem_range] at h₁, obtain ⟨x, hx⟩ := h₁, + rw set_like.le_def, intros z hz, simp only [mem_ker, set_like.mem_coe] at hz, + rw [← set_like.mem_coe, f.range_coe, set.mem_range] at h₁, obtain ⟨x, hx⟩ := h₁, have hx' : x ∈ p, { exact h₂ hx, }, have hxz : z + x ∈ p, { apply h₂, simp [hx, hz], }, suffices : z + x - x ∈ p, { simpa only [this, add_sub_cancel], }, @@ -1768,7 +1768,7 @@ variables {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} variables (e e' : M ≃ₗ[R] M₂) lemma map_eq_comap {p : submodule R M} : (p.map e : submodule R M₂) = p.comap e.symm := -submodule.coe_injective $ by simp [e.image_eq_preimage] +set_like.coe_injective $ by simp [e.image_eq_preimage] /-- A linear equivalence of two modules restricts to a linear equivalence from any submodule of the domain onto the image of the submodule. -/ @@ -1866,7 +1866,7 @@ linear_map.range_eq_top.2 e.to_equiv.surjective lemma eq_bot_of_equiv [semimodule R M₂] (e : p ≃ₗ[R] (⊥ : submodule R M₂)) : p = ⊥ := begin - refine bot_unique (submodule.le_def'.2 $ assume b hb, (submodule.mem_bot R).2 _), + refine bot_unique (set_like.le_def.2 $ assume b hb, (submodule.mem_bot R).2 _), rw [← p.mk_eq_zero hb, ← e.map_eq_zero_iff], apply submodule.eq_zero_of_bot_submodule end @@ -2084,7 +2084,7 @@ linear_equiv.trans lemma to_span_nonzero_singleton_one (x : M) (h : x ≠ 0) : to_span_nonzero_singleton K M x h 1 = (⟨x, submodule.mem_span_singleton_self x⟩ : K ∙ x) := begin - apply submodule.coe_eq_coe.mp, + apply set_like.coe_eq_coe.mp, have : ↑(to_span_nonzero_singleton K M x h 1) = to_span_singleton K M x 1 := rfl, rw [this, to_span_singleton_one, submodule.coe_mk], end @@ -2116,8 +2116,8 @@ def comap_subtype_equiv_of_le {p q : submodule R M} (hpq : p ≤ q) : comap q.subtype p ≃ₗ[R] p := { to_fun := λ x, ⟨x, x.2⟩, inv_fun := λ x, ⟨⟨x, hpq x.2⟩, x.2⟩, - left_inv := λ x, by simp only [coe_mk, submodule.eta, coe_coe], - right_inv := λ x, by simp only [subtype.coe_mk, submodule.eta, coe_coe], + left_inv := λ x, by simp only [coe_mk, set_like.eta, coe_coe], + right_inv := λ x, by simp only [subtype.coe_mk, set_like.eta, coe_coe], map_add' := λ x y, rfl, map_smul' := λ c x, rfl } @@ -2167,7 +2167,7 @@ end lemma comap_le_comap_smul (f : M →ₗ[R] M₂) (c : R) : comap f q ≤ comap (c • f) q := begin - rw le_def', + rw set_like.le_def, intros m h, change c • (f m) ∈ q, change f m ∈ q at h, @@ -2177,7 +2177,7 @@ end lemma inf_comap_le_comap_add (f₁ f₂ : M →ₗ[R] M₂) : comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q := begin - rw le_def', + rw set_like.le_def, intros m h, change f₁ m + f₂ m ∈ q, change f₁ m ∈ q ∧ f₂ m ∈ q at h, diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean index 03cd4f0c2f2de..b59c462974ad5 100644 --- a/src/linear_algebra/basis.lean +++ b/src/linear_algebra/basis.lean @@ -535,7 +535,7 @@ open submodule linear_map lemma submodule.exists_le_ker_of_lt_top (p : submodule K V) (hp : p < ⊤) : ∃ f ≠ (0 : V →ₗ[K] K), p ≤ ker f := begin - rcases submodule.exists_of_lt hp with ⟨v, -, hpv⟩, clear hp, + rcases set_like.exists_of_lt hp with ⟨v, -, hpv⟩, clear hp, rcases (linear_pmap.sup_span_singleton ⟨p, 0⟩ v (1 : K) hpv).to_fun.exists_extend with ⟨f, hf⟩, refine ⟨f, _, _⟩, { rintro rfl, rw [linear_map.zero_comp] at hf, diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean index c4c0af0815a0a..9f4396fe69b66 100644 --- a/src/linear_algebra/dimension.lean +++ b/src/linear_algebra/dimension.lean @@ -379,7 +379,7 @@ begin { rw [eq_top_iff, range_cod_restrict, ← map_le_iff_le_comap, map_top, range_subtype], rintros ⟨d, e⟩, have h := eq₂ d (-e), - simp only [add_eq_zero_iff_eq_neg, prod_apply, mem_ker, mem_coe, prod.mk.inj_iff, + simp only [add_eq_zero_iff_eq_neg, prod_apply, mem_ker, set_like.mem_coe, prod.mk.inj_iff, coprod_apply, map_neg, neg_apply, linear_map.mem_range] at ⊢ h, assume hde, rcases h hde with ⟨c, h₁, h₂⟩, diff --git a/src/linear_algebra/dual.lean b/src/linear_algebra/dual.lean index 9b5f279077e6b..798bc2edc12f1 100644 --- a/src/linear_algebra/dual.lean +++ b/src/linear_algebra/dual.lean @@ -648,7 +648,7 @@ begin { ext x, rw dual_map_apply, rw submodule.mem_dual_annihilator at hφ, - exact hφ (f x) ⟨x, (submodule.mem_coe _).mpr submodule.mem_top, rfl⟩ } + exact hφ (f x) ⟨x, set_like.mem_coe.mpr submodule.mem_top, rfl⟩ } end lemma range_dual_map_le_dual_annihilator_ker : diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean index af89c9331a5ee..9eb88efd9d9ea 100644 --- a/src/linear_algebra/finite_dimensional.lean +++ b/src/linear_algebra/finite_dimensional.lean @@ -1078,7 +1078,7 @@ begin -- To show `b i ∈ span (b '' (univ \ {i}))`, we use that it's a weighted sum -- of the other `b j`s. - rw [j_eq, mem_coe, show b i = -((g i)⁻¹ • (s.erase i).sum (λ j, g j • b j)), from _], + rw [j_eq, set_like.mem_coe, show b i = -((g i)⁻¹ • (s.erase i).sum (λ j, g j • b j)), from _], { refine submodule.neg_mem _ (smul_mem _ _ (sum_mem _ (λ k hk, _))), obtain ⟨k_ne_i, k_mem⟩ := finset.mem_erase.mp hk, refine smul_mem _ _ (subset_span ⟨k, _, rfl⟩), diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean index 47e6ac5cbbf51..b66eec4501ce6 100644 --- a/src/linear_algebra/finsupp.lean +++ b/src/linear_algebra/finsupp.lean @@ -109,7 +109,7 @@ lemma lsingle_range_le_ker_lapply (s t : set α) (h : disjoint s t) : (⨆a∈s, (lsingle a : M →ₗ[R] (α →₀ M)).range) ≤ (⨅a∈t, ker (lapply a)) := begin refine supr_le (assume a₁, supr_le $ assume h₁, range_le_iff_comap.2 _), - simp only [(ker_comp _ _).symm, eq_top_iff, le_def', mem_ker, comap_infi, mem_infi], + simp only [(ker_comp _ _).symm, eq_top_iff, set_like.le_def, mem_ker, comap_infi, mem_infi], assume b hb a₂ h₂, have : a₁ ≠ a₂ := assume eq, h ⟨h₁, eq.symm ▸ h₂⟩, exact single_eq_of_ne this @@ -117,13 +117,13 @@ end lemma infi_ker_lapply_le_bot : (⨅a, ker (lapply a : (α →₀ M) →ₗ[R] M)) ≤ ⊥ := begin - simp only [le_def', mem_infi, mem_ker, mem_bot, lapply_apply], + simp only [set_like.le_def, mem_infi, mem_ker, mem_bot, lapply_apply], exact assume a h, finsupp.ext h end lemma supr_lsingle_range : (⨆a, (lsingle a : M →ₗ[R] (α →₀ M)).range) = ⊤ := begin - refine (eq_top_iff.2 $ le_def'.2 $ assume f _, _), + refine (eq_top_iff.2 $ set_like.le_def.2 $ assume f _, _), rw [← sum_single f], refine sum_mem _ (assume a ha, submodule.mem_supr_of_mem a $ set.mem_image_of_mem _ trivial) end @@ -180,7 +180,7 @@ set.subset.trans support_single_subset (finset.singleton_subset_set_iff.2 h) lemma supported_eq_span_single (s : set α) : supported R R s = span R ((λ i, single i 1) '' s) := begin - refine (span_eq_of_le _ _ (le_def'.2 $ λ l hl, _)).symm, + refine (span_eq_of_le _ _ (set_like.le_def.2 $ λ l hl, _)).symm, { rintro _ ⟨_, hp, rfl ⟩ , exact single_mem_supported R 1 hp }, { rw ← l.sum_single, refine sum_mem _ (λ i il, _), @@ -391,7 +391,7 @@ theorem lmap_domain_disjoint_ker (f : α → α') {s : set α} disjoint (supported M R s) (lmap_domain M R f).ker := begin rintro l ⟨h₁, h₂⟩, - rw [mem_coe, mem_ker, lmap_domain_apply, map_domain] at h₂, + rw [set_like.mem_coe, mem_ker, lmap_domain_apply, map_domain] at h₂, simp, ext x, haveI := classical.dec_pred (λ x, x ∈ s), by_cases xs : x ∈ s, @@ -455,7 +455,7 @@ begin { apply span_le.2, intros x hx, rcases hx with ⟨i, hi⟩, - rw [mem_coe, linear_map.mem_range], + rw [set_like.mem_coe, linear_map.mem_range], use finsupp.single i 1, simp [hi] } end @@ -617,7 +617,7 @@ begin use s, simp only [mem_supr, supr_le_iff], assume N hN, - rw [finsupp.total_apply, finsupp.sum, ← submodule.mem_coe], + rw [finsupp.total_apply, finsupp.sum, ← set_like.mem_coe], apply N.sum_mem, assume x hx, apply submodule.smul_mem, diff --git a/src/linear_algebra/pi.lean b/src/linear_algebra/pi.lean index 864766385389e..d6ce528e2148e 100644 --- a/src/linear_algebra/pi.lean +++ b/src/linear_algebra/pi.lean @@ -66,7 +66,7 @@ lemma proj_pi (f : Πi, M₂ →ₗ[R] φ i) (i : ι) : (proj i).comp (pi f) = f ext $ assume c, rfl lemma infi_ker_proj : (⨅i, ker (proj i) : submodule R (Πi, φ i)) = ⊥ := -bot_unique $ submodule.le_def'.2 $ assume a h, +bot_unique $ set_like.le_def.2 $ assume a h, begin simp only [mem_infi, mem_ker, proj_apply] at h, exact (mem_bot _).2 (funext $ assume i, h i) diff --git a/src/linear_algebra/prod.lean b/src/linear_algebra/prod.lean index 67ce80059f119..68a944de4c467 100644 --- a/src/linear_algebra/prod.lean +++ b/src/linear_algebra/prod.lean @@ -216,7 +216,7 @@ theorem map_coprod_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) map (coprod f g) (p.prod q) = map f p ⊔ map g q := begin refine le_antisymm _ (sup_le (map_le_iff_le_comap.2 _) (map_le_iff_le_comap.2 _)), - { rw le_def', rintro _ ⟨x, ⟨h₁, h₂⟩, rfl⟩, + { rw set_like.le_def, rintro _ ⟨x, ⟨h₁, h₂⟩, rfl⟩, exact mem_sup.2 ⟨_, ⟨_, h₁, rfl⟩, _, ⟨_, h₂, rfl⟩, rfl⟩ }, { exact λ x hx, ⟨(x, 0), by simp [hx]⟩ }, { exact λ x hx, ⟨(0, x), by simp [hx]⟩ } @@ -246,7 +246,8 @@ by rw [ker, ← prod_bot, comap_prod_prod]; refl lemma range_prod_le (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : range (prod f g) ≤ (range f).prod (range g) := begin - simp only [le_def', prod_apply, mem_range, mem_coe, mem_prod, exists_imp_distrib], + simp only [set_like.le_def, prod_apply, mem_range, set_like.mem_coe, mem_prod, + exists_imp_distrib], rintro _ x rfl, exact ⟨⟨x, rfl⟩, ⟨x, rfl⟩⟩ end @@ -261,7 +262,7 @@ variables [add_comm_monoid M] [add_comm_monoid M₂] variables [semimodule R M] [semimodule R M₂] lemma sup_eq_range (p q : submodule R M) : p ⊔ q = (p.subtype.coprod q.subtype).range := -submodule.ext $ λ x, by simp [submodule.mem_sup, submodule.exists] +submodule.ext $ λ x, by simp [submodule.mem_sup, set_like.exists] variables (p : submodule R M) (q : submodule R M₂) @@ -368,8 +369,8 @@ lemma range_prod_eq {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : ker f ⊔ range (prod f g) = (range f).prod (range g) := begin refine le_antisymm (f.range_prod_le g) _, - simp only [le_def', prod_apply, mem_range, mem_coe, mem_prod, exists_imp_distrib, and_imp, - prod.forall], + simp only [set_like.le_def, prod_apply, mem_range, set_like.mem_coe, mem_prod, exists_imp_distrib, + and_imp, prod.forall], rintros _ _ x rfl y rfl, simp only [prod.mk.inj_iff, ← sub_mem_ker_iff], have : y - x ∈ ker f ⊔ ker g, { simp only [h, mem_top] }, diff --git a/src/linear_algebra/projection.lean b/src/linear_algebra/projection.lean index a1da27d146ca7..7a24b999effd8 100644 --- a/src/linear_algebra/projection.lean +++ b/src/linear_algebra/projection.lean @@ -52,8 +52,8 @@ lemma is_compl_of_proj {f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) : begin split, { rintros x ⟨hpx, hfx⟩, - erw [mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx, - simp only [hfx, mem_coe, zero_mem] }, + erw [set_like.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx, + simp only [hfx, set_like.mem_coe, zero_mem] }, { intros x hx, rw [mem_sup'], refine ⟨f x, ⟨x - f x, _⟩, add_sub_cancel'_right _ _⟩, diff --git a/src/linear_algebra/std_basis.lean b/src/linear_algebra/std_basis.lean index 4c643cef93609..c5ba442c5e529 100644 --- a/src/linear_algebra/std_basis.lean +++ b/src/linear_algebra/std_basis.lean @@ -78,7 +78,7 @@ lemma supr_range_std_basis_le_infi_ker_proj (I J : set ι) (h : disjoint I J) : (⨆i∈I, range (std_basis R φ i)) ≤ (⨅i∈J, ker (proj i)) := begin refine (supr_le $ assume i, supr_le $ assume hi, range_le_iff_comap.2 _), - simp only [(ker_comp _ _).symm, eq_top_iff, le_def', mem_ker, comap_infi, mem_infi], + simp only [(ker_comp _ _).symm, eq_top_iff, set_like.le_def, mem_ker, comap_infi, mem_infi], assume b hb j hj, have : i ≠ j := assume eq, h ⟨hi, eq.symm ▸ hj⟩, rw [proj_std_basis_ne R φ j i this.symm, zero_apply] @@ -86,7 +86,7 @@ end lemma infi_ker_proj_le_supr_range_std_basis {I : finset ι} {J : set ι} (hu : set.univ ⊆ ↑I ∪ J) : (⨅ i∈J, ker (proj i)) ≤ (⨆i∈I, range (std_basis R φ i)) := -submodule.le_def'.2 +set_like.le_def.2 begin assume b hb, simp only [mem_infi, mem_ker, proj_apply] at hb, @@ -127,7 +127,7 @@ begin refine disjoint.mono (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ disjoint_compl_right) (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ disjoint_compl_right) _, - simp only [disjoint, submodule.le_def', mem_infi, mem_inf, mem_ker, mem_bot, proj_apply, + simp only [disjoint, set_like.le_def, mem_infi, mem_inf, mem_ker, mem_bot, proj_apply, funext_iff], rintros b ⟨hI, hJ⟩ i, classical, diff --git a/src/ring_theory/adjoin/basic.lean b/src/ring_theory/adjoin/basic.lean index a083c72c7fef3..ad5ea5b4b4a91 100644 --- a/src/ring_theory/adjoin/basic.lean +++ b/src/ring_theory/adjoin/basic.lean @@ -129,7 +129,7 @@ le_antisymm exact subalgebra.mul_mem _ ih (subset_adjoin rfl) })) lemma adjoin_singleton_one : adjoin R ({1} : set A) = ⊥ := -eq_bot_iff.2 $ adjoin_le $ set.singleton_subset_iff.2 $ subalgebra.mem_coe.2 $ subalgebra.one_mem ⊥ +eq_bot_iff.2 $ adjoin_le $ set.singleton_subset_iff.2 $ set_like.mem_coe.2 $ one_mem _ theorem adjoin_union_coe_submodule : (adjoin R (s ∪ t)).to_submodule = (adjoin R s).to_submodule * (adjoin R t).to_submodule := diff --git a/src/ring_theory/adjoin_root.lean b/src/ring_theory/adjoin_root.lean index d3d24d4c9c20e..8c7305cacffc9 100644 --- a/src/ring_theory/adjoin_root.lean +++ b/src/ring_theory/adjoin_root.lean @@ -154,7 +154,7 @@ end lift_hom f (ϕ (root f)) (aeval_alg_hom_eq_zero f ϕ) = ϕ := begin suffices : ϕ.equalizer (lift_hom f (ϕ (root f)) (aeval_alg_hom_eq_zero f ϕ)) = ⊤, - { exact (alg_hom.ext (λ x, (subalgebra.ext_iff.mp (this) x).mpr algebra.mem_top)).symm }, + { exact (alg_hom.ext (λ x, (set_like.ext_iff.mp (this) x).mpr algebra.mem_top)).symm }, rw [eq_top_iff, ←adjoin_root_eq_top, algebra.adjoin_le_iff, set.singleton_subset_iff], exact (@lift_root _ _ _ _ _ _ _ (aeval_alg_hom_eq_zero f ϕ)).symm, end diff --git a/src/ring_theory/algebra_tower.lean b/src/ring_theory/algebra_tower.lean index d7d0074893fdb..430e764047570 100644 --- a/src/ring_theory/algebra_tower.lean +++ b/src/ring_theory/algebra_tower.lean @@ -213,7 +213,7 @@ begin { rw mul_one, exact subset_span (set.mem_insert _ _) }, { rw one_mul, exact subset_span (set.mem_insert_of_mem _ hyj) }, { rw mul_one, exact subset_span (set.mem_insert_of_mem _ hyi) }, - { rw ← hf (yi * yj), exact (submodule.mem_coe _).2 (sum_mem _ $ λ yk hyk, smul_mem + { rw ← hf (yi * yj), exact set_like.mem_coe.2 (sum_mem _ $ λ yk hyk, smul_mem (span (algebra.adjoin A (↑s : set B)) (insert 1 ↑y : set C)) ⟨f (yi * yj) yk, algebra.subset_adjoin $ hsy yi yj yk hyi hyj hyk⟩ (subset_span $ set.mem_insert_of_mem _ hyk : yk ∈ _)) } }, diff --git a/src/ring_theory/euclidean_domain.lean b/src/ring_theory/euclidean_domain.lean index 4db7cc9e630ca..83e3caea25d8a 100644 --- a/src/ring_theory/euclidean_domain.lean +++ b/src/ring_theory/euclidean_domain.lean @@ -29,7 +29,7 @@ theorem span_gcd {α} [euclidean_domain α] (x y : α) : begin apply le_antisymm, { refine span_le.2 (λ x, _), - simp only [set.mem_singleton_iff, submodule.mem_coe, mem_span_pair], + simp only [set.mem_singleton_iff, set_like.mem_coe, mem_span_pair], rintro rfl, exact ⟨gcd_a x y, gcd_b x y, by simp [gcd_eq_gcd_ab, mul_comm]⟩ }, { assume z , diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean index 85a596412bca1..a9de343bb9234 100644 --- a/src/ring_theory/fractional_ideal.lean +++ b/src/ring_theory/fractional_ideal.lean @@ -645,7 +645,7 @@ variables {I J : fractional_ideal g} (h : g.codomain →ₐ[R] g'.codomain) lemma exists_ne_zero_mem_is_integer [nontrivial R] (hI : I ≠ 0) : ∃ x ≠ (0 : R), g.to_map x ∈ I := begin - obtain ⟨y, y_mem, y_not_mem⟩ := submodule.exists_of_lt (bot_lt_iff_ne_bot.mpr hI), + obtain ⟨y, y_mem, y_not_mem⟩ := set_like.exists_of_lt (bot_lt_iff_ne_bot.mpr hI), have y_ne_zero : y ≠ 0 := by simpa using y_not_mem, obtain ⟨z, ⟨x, hx⟩⟩ := g.exists_integer_multiple y, refine ⟨x, _, _⟩, @@ -697,7 +697,7 @@ lemma fractional_div_of_nonzero {I J : fractional_ideal g} (h : J ≠ 0) : begin rcases I with ⟨I, aI, haI, hI⟩, rcases J with ⟨J, aJ, haJ, hJ⟩, - obtain ⟨y, mem_J, not_mem_zero⟩ := exists_of_lt (bot_lt_iff_ne_bot.mpr h), + obtain ⟨y, mem_J, not_mem_zero⟩ := set_like.exists_of_lt (bot_lt_iff_ne_bot.mpr h), obtain ⟨y', hy'⟩ := hJ y mem_J, use (aI * y'), split, diff --git a/src/ring_theory/hahn_series.lean b/src/ring_theory/hahn_series.lean index ec44c67174634..406b972e91b71 100644 --- a/src/ring_theory/hahn_series.lean +++ b/src/ring_theory/hahn_series.lean @@ -576,7 +576,7 @@ theorem algebra_map_apply {r : R} : instance [nontrivial Γ] [nontrivial R] : nontrivial (subalgebra R (hahn_series Γ R)) := ⟨⟨⊥, ⊤, begin - rw [ne.def, subalgebra.ext_iff, not_forall], + rw [ne.def, set_like.ext_iff, not_forall], obtain ⟨a, ha⟩ := exists_ne (0 : Γ), refine ⟨single a 1, _⟩, simp only [algebra.mem_bot, not_exists, set.mem_range, iff_true, algebra.mem_top], diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean index 6eaac02ab6791..f7235863644b8 100644 --- a/src/ring_theory/ideal/basic.lean +++ b/src/ring_theory/ideal/basic.lean @@ -608,7 +608,7 @@ begin rw [bot_lt_iff_ne_bot, lt_top_iff_ne_top], exact ⟨mt ideal.span_singleton_eq_bot.mp nz, mt ideal.span_singleton_eq_top.mp nu⟩ }, { rintros ⟨I, bot_lt, lt_top⟩ hf, - obtain ⟨x, mem, ne_zero⟩ := submodule.exists_of_lt bot_lt, + obtain ⟨x, mem, ne_zero⟩ := set_like.exists_of_lt bot_lt, rw submodule.mem_bot at ne_zero, obtain ⟨y, hy⟩ := hf.mul_inv_cancel ne_zero, rw [lt_top_iff_ne_top, ne.def, ideal.eq_top_iff_one, ← hy] at lt_top, diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean index 4c5428765748b..30a2357306cf9 100644 --- a/src/ring_theory/ideal/operations.lean +++ b/src/ring_theory/ideal/operations.lean @@ -633,7 +633,7 @@ begin { exact hs (or.inl $ or.inr $ add_sub_cancel' r s ▸ (f b).sub_mem hb hrb) }, { exact hri (add_sub_cancel r s ▸ (f i).sub_mem hi hsi) }, { rw set.mem_bUnion_iff at ht, rcases ht with ⟨j, hjt, hj⟩, - simp only [finset.inf_eq_infi, submodule.mem_coe, submodule.mem_infi] at hr, + simp only [finset.inf_eq_infi, set_like.mem_coe, submodule.mem_infi] at hr, exact hs (or.inr $ set.mem_bUnion hjt $ add_sub_cancel' r s ▸ (f j).sub_mem hj $ hr j hjt) } end @@ -1068,10 +1068,10 @@ lemma ker_eq : ((ker f) : set R) = is_add_group_hom.ker f := rfl lemma ker_eq_comap_bot (f : R →+* S) : f.ker = ideal.comap f ⊥ := rfl lemma injective_iff_ker_eq_bot : function.injective f ↔ ker f = ⊥ := -by rw [submodule.ext'_iff, ker_eq]; exact is_add_group_hom.injective_iff_trivial_ker f +by rw [set_like.ext'_iff, ker_eq]; exact is_add_group_hom.injective_iff_trivial_ker f lemma ker_eq_bot_iff_eq_zero : ker f = ⊥ ↔ ∀ x, f x = 0 → x = 0 := -by rw [submodule.ext'_iff, ker_eq]; exact is_add_group_hom.trivial_ker_iff_eq_zero f +by rw [set_like.ext'_iff, ker_eq]; exact is_add_group_hom.trivial_ker_iff_eq_zero f /-- If the target is not the zero ring, then one is not in the kernel.-/ lemma not_one_mem_ker [nontrivial S] (f : R →+* S) : (1:R) ∉ ker f := diff --git a/src/ring_theory/ideal/over.lean b/src/ring_theory/ideal/over.lean index 906726b161e19..0a517d69988eb 100644 --- a/src/ring_theory/ideal/over.lean +++ b/src/ring_theory/ideal/over.lean @@ -161,7 +161,7 @@ lemma comap_lt_comap_of_root_mem_sdiff [I.is_prime] (hIJ : I ≤ J) {p : polynomial R} (p_ne_zero : p.map (quotient.mk (I.comap f)) ≠ 0) (hp : p.eval₂ f r ∈ I) : I.comap f < J.comap f := let ⟨i, hJ, hI⟩ := exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff hIJ hr p_ne_zero hp -in lt_iff_le_and_exists.mpr ⟨comap_mono hIJ, p.coeff i, hJ, hI⟩ +in set_like.lt_iff_le_and_exists.mpr ⟨comap_mono hIJ, p.coeff i, hJ, hI⟩ variables [algebra R S] @@ -204,7 +204,7 @@ lemma is_maximal_of_is_integral_of_is_maximal_comap (hRS : algebra.is_integral R S) (I : ideal S) [I.is_prime] (hI : is_maximal (I.comap (algebra_map R S))) : is_maximal I := ⟨⟨mt comap_eq_top_iff.mpr hI.1.1, - λ J I_lt_J, let ⟨I_le_J, x, hxJ, hxI⟩ := lt_iff_le_and_exists.mp I_lt_J in + λ J I_lt_J, let ⟨I_le_J, x, hxJ, hxI⟩ := set_like.lt_iff_le_and_exists.mp I_lt_J in comap_eq_top_iff.1 $ hI.1.2 _ (comap_lt_comap_of_integral_mem_sdiff I_le_J ⟨hxJ, hxI⟩ (hRS x))⟩⟩ lemma is_maximal_of_is_integral_of_is_maximal_comap' {R S : Type*} [comm_ring R] [integral_domain S] @@ -237,7 +237,7 @@ imp_of_not_imp_not _ _ integral_closure.comap_ne_bot lemma integral_closure.comap_lt_comap {I J : ideal (integral_closure R S)} [I.is_prime] (I_lt_J : I < J) : I.comap (algebra_map R (integral_closure R S)) < J.comap (algebra_map _ _) := -let ⟨I_le_J, x, hxJ, hxI⟩ := lt_iff_le_and_exists.mp I_lt_J in +let ⟨I_le_J, x, hxJ, hxI⟩ := set_like.lt_iff_le_and_exists.mp I_lt_J in comap_lt_comap_of_integral_mem_sdiff I_le_J ⟨hxJ, hxI⟩ (integral_closure.is_integral x) lemma integral_closure.is_maximal_of_is_maximal_comap diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean index d4819624823d3..de0d80ff55b02 100644 --- a/src/ring_theory/integral_closure.lean +++ b/src/ring_theory/integral_closure.lean @@ -227,7 +227,7 @@ begin have : span S₀ (insert 1 ↑y : set A) = (algebra.adjoin S₀ (↑y : set A)).to_submodule, { refine le_antisymm (span_le.2 $ set.insert_subset.2 ⟨(algebra.adjoin S₀ ↑y).one_mem, algebra.subset_adjoin⟩) (λ z hz, _), - rw [subalgebra.mem_to_submodule, algebra.mem_adjoin_iff] at hz, rw ← submodule.mem_coe, + rw [subalgebra.mem_to_submodule, algebra.mem_adjoin_iff] at hz, rw ← set_like.mem_coe, refine ring.closure_subset (set.union_subset (set.range_subset_iff.2 $ λ t, _) (λ t ht, subset_span $ or.inr ht)) hz, rw algebra.algebra_map_eq_smul_one, diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean index 0ba6bdcb2beab..11e999998f2e9 100644 --- a/src/ring_theory/noetherian.lean +++ b/src/ring_theory/noetherian.lean @@ -219,15 +219,15 @@ begin rw [submodule.span_le, image_subset_iff], intros i hi, refine submodule.span_induction hi (λ x hx, _) _ (λ x y hx hy, _) (λ r x hx, _), - { simp only [mem_coe, mem_preimage], + { simp only [set_like.mem_coe, mem_preimage], suffices : f x ∈ f '' X, { exact ideal.subset_span this }, exact mem_image_of_mem ⇑f hx }, - { simp only [mem_coe, ring_hom.map_zero, mem_preimage, zero_mem] }, - { simp only [mem_coe, mem_preimage] at hx hy, - simp only [ring_hom.map_add, mem_coe, mem_preimage], + { simp only [set_like.mem_coe, ring_hom.map_zero, mem_preimage, zero_mem] }, + { simp only [set_like.mem_coe, mem_preimage] at hx hy, + simp only [ring_hom.map_add, set_like.mem_coe, mem_preimage], exact submodule.add_mem _ hx hy }, - { simp only [mem_coe, mem_preimage] at hx, - simp only [algebra.id.smul_eq_mul, mem_coe, mem_preimage, ring_hom.map_mul], + { simp only [set_like.mem_coe, mem_preimage] at hx, + simp only [algebra.id.smul_eq_mul, set_like.mem_coe, mem_preimage, ring_hom.map_mul], exact submodule.smul_mem _ _ hx } end diff --git a/src/ring_theory/polynomial/basic.lean b/src/ring_theory/polynomial/basic.lean index e53eacdc88cf3..264fa9cb624f8 100644 --- a/src/ring_theory/polynomial/basic.lean +++ b/src/ring_theory/polynomial/basic.lean @@ -441,7 +441,7 @@ theorem leading_coeff_nth_mono {m n : ℕ} (H : m ≤ n) : I.leading_coeff_nth m ≤ I.leading_coeff_nth n := begin intros r hr, - simp only [submodule.mem_coe, mem_leading_coeff_nth] at hr ⊢, + simp only [set_like.mem_coe, mem_leading_coeff_nth] at hr ⊢, rcases hr with ⟨p, hpI, hpdeg, rfl⟩, refine ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, _, leading_coeff_mul_X_pow⟩, refine le_trans (degree_mul_le _ _) _, diff --git a/src/ring_theory/power_series/basic.lean b/src/ring_theory/power_series/basic.lean index 122d16873f04e..58ba67ba3238a 100644 --- a/src/ring_theory/power_series/basic.lean +++ b/src/ring_theory/power_series/basic.lean @@ -459,7 +459,7 @@ end instance [nonempty σ] [nontrivial R] : nontrivial (subalgebra R (mv_power_series σ R)) := ⟨⟨⊥, ⊤, begin - rw [ne.def, subalgebra.ext_iff, not_forall], + rw [ne.def, set_like.ext_iff, not_forall], inhabit σ, refine ⟨X (default σ), _⟩, simp only [algebra.mem_bot, not_exists, set.mem_range, iff_true, algebra.mem_top], diff --git a/src/ring_theory/principal_ideal_domain.lean b/src/ring_theory/principal_ideal_domain.lean index 2a9153a4285b9..bf394c1ae4390 100644 --- a/src/ring_theory/principal_ideal_domain.lean +++ b/src/ring_theory/principal_ideal_domain.lean @@ -145,7 +145,7 @@ is_noetherian_ring_iff.2 ⟨assume s : ideal R, begin rcases (is_principal_ideal_ring.principal s).principal with ⟨a, rfl⟩, rw [← finset.coe_singleton], - exact ⟨{a}, submodule.coe_injective rfl⟩ + exact ⟨{a}, set_like.coe_injective rfl⟩ end⟩ lemma is_maximal_of_irreducible {p : R} (hp : irreducible p) : diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean index 3935b2bce5444..cfd6ff9366a34 100644 --- a/src/ring_theory/roots_of_unity.lean +++ b/src/ring_theory/roots_of_unity.lean @@ -94,7 +94,7 @@ lemma map_roots_of_unity (f : units M →* units N) (k : ℕ+) : (roots_of_unity k M).map f ≤ roots_of_unity k N := begin rintros _ ⟨ζ, h, rfl⟩, - simp only [←monoid_hom.map_pow, *, mem_roots_of_unity, subgroup.mem_coe, monoid_hom.map_one] at * + simp only [←monoid_hom.map_pow, *, mem_roots_of_unity, set_like.mem_coe, monoid_hom.map_one] at * end lemma mem_roots_of_unity_iff_mem_nth_roots {ζ : units R} : @@ -545,7 +545,7 @@ h.zmod_equiv_gpowers_symm_apply_pow i lemma gpowers_eq {k : ℕ+} {ζ : units R} (h : is_primitive_root ζ k) : subgroup.gpowers ζ = roots_of_unity k R := begin - apply subgroup.ext', + apply set_like.coe_injective, haveI : fact (0 < (k : ℕ)) := ⟨k.pos⟩, haveI F : fintype (subgroup.gpowers ζ) := fintype.of_equiv _ (h.zmod_equiv_gpowers).to_equiv, refine @set.eq_of_subset_of_card_le (units R) (subgroup.gpowers ζ) (roots_of_unity k R) diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean index a5a804ca37962..b843d16620be7 100644 --- a/src/ring_theory/subring.lean +++ b/src/ring_theory/subring.lean @@ -86,11 +86,14 @@ def to_submonoid (s : subring R) : submonoid R := { carrier := s.carrier, ..s.to_subsemiring.to_submonoid } -instance : has_coe (subring R) (set R) := ⟨subring.carrier⟩ +instance : set_like (subring R) R := +⟨subring.carrier, λ p q h, by cases p; cases q; congr'⟩ -instance : has_mem R (subring R) := ⟨λ m S, m ∈ (S:set R)⟩ +@[simp] +lemma mem_carrier {s : subring R} {x : R} : x ∈ s.carrier ↔ x ∈ s := iff.rfl -instance : has_coe_to_sort (subring R) := ⟨Type*, λ S, {x : R // x ∈ S}⟩ +/-- Two subrings are equal if they have the same elements. -/ +@[ext] theorem ext {S T : subring R} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := set_like.ext h /-- Construct a `subring R` from a set `s`, a submonoid `sm`, and an additive subgroup `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`. -/ @@ -116,12 +119,12 @@ iff.rfl @[simp] lemma mk'_to_submonoid {s : set R} {sm : submonoid R} (hm : ↑sm = s) {sa : add_subgroup R} (ha : ↑sa = s) : (subring.mk' s sm sa hm ha).to_submonoid = sm := -submonoid.ext' hm.symm +set_like.coe_injective hm.symm @[simp] lemma mk'_to_add_subgroup {s : set R} {sm : submonoid R} (hm : ↑sm = s) {sa : add_subgroup R} (ha : ↑sa =s) : (subring.mk' s sm sa hm ha).to_add_subgroup = sa := -add_subgroup.ext' ha.symm +set_like.coe_injective ha.symm end subring @@ -134,14 +137,6 @@ def set.to_subring (S : set R) [is_subring S] : subring R := add_mem' := λ a b, is_add_submonoid.add_mem, neg_mem' := λ a, is_add_subgroup.neg_mem } -protected lemma subring.exists {s : subring R} {p : s → Prop} : - (∃ x : s, p x) ↔ ∃ x ∈ s, p ⟨x, ‹x ∈ s›⟩ := -set_coe.exists - -protected lemma subring.forall {s : subring R} {p : s → Prop} : - (∀ x : s, p x) ↔ ∀ x ∈ s, p ⟨x, ‹x ∈ s›⟩ := -set_coe.forall - /-- A `subsemiring` containing -1 is a `subring`. -/ def subsemiring.to_subring (s : subsemiring R) (hneg : (-1 : R) ∈ s) : subring R := { neg_mem' := by { rintros x, rw <-neg_one_mul, apply subsemiring.mul_mem, exact hneg, } @@ -151,17 +146,6 @@ namespace subring variables (s : subring R) -/-- Two subrings are equal if the underlying subsets are equal. -/ -theorem ext' ⦃s t : subring R⦄ (h : (s : set R) = t) : s = t := -by { cases s, cases t, congr' } - -/-- Two subrings are equal if and only if the underlying subsets are equal. -/ -protected theorem ext'_iff {s t : subring R} : s = t ↔ (s : set R) = t := -⟨λ h, h ▸ rfl, λ h, ext' h⟩ - -/-- Two subrings are equal if they have the same elements. -/ -@[ext] theorem ext {S T : subring R} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := ext' $ set.ext h - /-- A subring contains the ring's 1. -/ theorem one_mem : (1 : R) ∈ s := s.one_mem' @@ -290,22 +274,6 @@ s.subtype.map_int_cast n /-! # Partial order -/ -instance : partial_order (subring R) := -{ le := λ s t, ∀ ⦃x⦄, x ∈ s → x ∈ t, - .. partial_order.lift (coe : subring R → set R) ext' } - -lemma le_def {s t : subring R} : s ≤ t ↔ ∀ ⦃x : R⦄, x ∈ s → x ∈ t := iff.rfl - -@[simp, norm_cast] lemma coe_subset_coe {s t : subring R} : (s : set R) ⊆ t ↔ s ≤ t := iff.rfl - -@[simp, norm_cast] lemma coe_ssubset_coe {s t : subring R} : (s : set R) ⊂ t ↔ s < t := iff.rfl - -@[simp, norm_cast] -lemma mem_coe {S : subring R} {m : R} : m ∈ (S : set R) ↔ m ∈ S := iff.rfl - -@[simp, norm_cast] -lemma coe_coe (s : subring R) : ↥(s : set R) = s := rfl - @[simp] lemma mem_to_submonoid {s : subring R} {x : R} : x ∈ s.to_submonoid ↔ x ∈ s := iff.rfl @[simp] lemma coe_to_submonoid (s : subring R) : (s.to_submonoid : set R) = s := rfl @[simp] lemma mem_to_add_subgroup {s : subring R} {x : R} : @@ -356,7 +324,7 @@ def map {R : Type u} {S : Type v} [ring R] [ring S] set.mem_image_iff_bex lemma map_map (g : S →+* T) (f : R →+* S) : (s.map f).map g = s.map (g.comp f) := -ext' $ set.image_image _ _ _ +set_like.coe_injective $ set.image_image _ _ _ lemma map_le_iff_le_comap {f : R →+* S} {s : subring R} {t : subring S} : s.map f ≤ t ↔ s ≤ t.comap f := @@ -453,7 +421,8 @@ instance : complete_lattice (subring R) := inf_le_right := λ s t x, and.right, le_inf := λ s t₁ t₂ h₁ h₂ x hx, ⟨h₁ hx, h₂ hx⟩, .. complete_lattice_of_Inf (subring R) - (λ s, is_glb.of_image (λ s t, show (s : set R) ≤ t ↔ s ≤ t, from coe_subset_coe) is_glb_binfi)} + (λ s, is_glb.of_image (λ s t, + show (s : set R) ≤ t ↔ s ≤ t, from set_like.coe_subset_coe) is_glb_binfi)} lemma eq_top_iff' (A : subring R) : A = ⊤ ↔ ∀ x : R, x ∈ A := eq_top_iff.trans ⟨λ h m, h $ mem_top m, λ h m _, h m⟩ @@ -626,7 +595,7 @@ lemma mem_supr_of_directed {ι} [hι : nonempty ι] {S : ι → subring R} (hS : {x : R} : x ∈ (⨆ i, S i) ↔ ∃ i, x ∈ S i := begin - refine ⟨_, λ ⟨i, hi⟩, (le_def.1 $ le_supr S i) hi⟩, + refine ⟨_, λ ⟨i, hi⟩, (set_like.le_def.1 $ le_supr S i) hi⟩, let U : subring R := subring.mk' (⋃ i, (S i : set R)) (⨆ i, (S i).to_submonoid) (⨆ i, (S i).to_add_subgroup) (submonoid.coe_supr_of_directed $ hS.mono_comp _ (λ _ _, id)) @@ -677,7 +646,7 @@ lemma range_restrict_surjective (f : R →+* S) : function.surjective f.range_re lemma range_top_iff_surjective {f : R →+* S} : f.range = (⊤ : subring S) ↔ function.surjective f := -subring.ext'_iff.trans $ iff.trans (by rw [coe_range, coe_top]) set.range_iff_surjective +set_like.ext'_iff.trans $ iff.trans (by rw [coe_range, coe_top]) set.range_iff_surjective /-- The range of a surjective ring homomorphism is the whole of the codomain. -/ lemma range_top_of_surjective (f : R →+* S) (hf : function.surjective f) : @@ -704,7 +673,7 @@ eq_of_eq_on_set_top $ hs ▸ eq_on_set_closure h lemma closure_preimage_le (f : R →+* S) (s : set S) : closure (f ⁻¹' s) ≤ (closure s).comap f := -closure_le.2 $ λ x hx, mem_coe.2 $ mem_comap.2 $ subset_closure hx +closure_le.2 $ λ x hx, set_like.mem_coe.2 $ mem_comap.2 $ subset_closure hx /-- The image under a ring homomorphism of the subring generated by a set equals the subring generated by the image of the set. -/ @@ -726,7 +695,7 @@ def inclusion {S T : subring R} (h : S ≤ T) : S →* T := S.subtype.cod_restrict' _ (λ x, h x.2) @[simp] lemma range_subtype (s : subring R) : s.subtype.range = s := -ext' $ (coe_srange _).trans subtype.range_coe +set_like.coe_injective $ (coe_srange _).trans subtype.range_coe @[simp] lemma range_fst : (fst R S).srange = ⊤ := @@ -741,8 +710,8 @@ lemma prod_bot_sup_bot_prod (s : subring R) (t : subring S) : (s.prod ⊥) ⊔ (prod ⊥ t) = s.prod t := le_antisymm (sup_le (prod_mono_right s bot_le) (prod_mono_left t bot_le)) $ assume p hp, prod.fst_mul_snd p ▸ mul_mem _ - ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, mem_coe.2 $ one_mem ⊥⟩) - ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨mem_coe.2 $ one_mem ⊥, hp.2⟩) + ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, set_like.mem_coe.2 $ one_mem ⊥⟩) + ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨set_like.mem_coe.2 $ one_mem ⊥, hp.2⟩) end subring @@ -753,7 +722,7 @@ variables {s t : subring R} /-- Makes the identity isomorphism from a proof two subrings of a multiplicative monoid are equal. -/ def subring_congr (h : s = t) : s ≃+* t := -{ map_mul' := λ _ _, rfl, map_add' := λ _ _, rfl, ..equiv.set_congr $ subring.ext'_iff.1 h } +{ map_mul' := λ _ _, rfl, map_add' := λ _ _, rfl, ..equiv.set_congr $ congr_arg _ h } /-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its `ring_hom.range`. -/ @@ -820,7 +789,7 @@ end lemma closure_preimage_le (f : R →+* S) (s : set S) : closure (f ⁻¹' s) ≤ (closure s).comap f := -closure_le.2 $ λ x hx, mem_coe.2 $ mem_comap.2 $ subset_closure hx +closure_le.2 $ λ x hx, set_like.mem_coe.2 $ mem_comap.2 $ subset_closure hx end subring diff --git a/src/ring_theory/subsemiring.lean b/src/ring_theory/subsemiring.lean index 017719a4c83ce..8fe55de987fed 100644 --- a/src/ring_theory/subsemiring.lean +++ b/src/ring_theory/subsemiring.lean @@ -36,11 +36,14 @@ add_decl_doc subsemiring.to_add_submonoid namespace subsemiring -instance : has_coe (subsemiring R) (set R) := ⟨subsemiring.carrier⟩ +instance : set_like (subsemiring R) R := +⟨subsemiring.carrier, λ p q h, by cases p; cases q; congr'⟩ -instance : has_mem R (subsemiring R) := ⟨λ m S, m ∈ (S:set R)⟩ +@[simp] +lemma mem_carrier {s : subsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s := iff.rfl -instance : has_coe_to_sort (subsemiring R) := ⟨Type*, λ S, {x : R // x ∈ S}⟩ +/-- Two subsemirings are equal if they have the same elements. -/ +@[ext] theorem ext {S T : subsemiring R} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := set_like.ext h /-- Construct a `subsemiring R` from a set `s`, a submonoid `sm`, and an additive submonoid `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`. -/ @@ -65,38 +68,19 @@ iff.rfl @[simp] lemma mk'_to_submonoid {s : set R} {sm : submonoid R} (hm : ↑sm = s) {sa : add_submonoid R} (ha : ↑sa = s) : (subsemiring.mk' s sm hm sa ha).to_submonoid = sm := -submonoid.ext' hm.symm +set_like.coe_injective hm.symm @[simp] lemma mk'_to_add_submonoid {s : set R} {sm : submonoid R} (hm : ↑sm = s) {sa : add_submonoid R} (ha : ↑sa =s) : (subsemiring.mk' s sm hm sa ha).to_add_submonoid = sa := -add_submonoid.ext' ha.symm +set_like.coe_injective ha.symm end subsemiring -protected lemma subsemiring.exists {s : subsemiring R} {p : s → Prop} : - (∃ x : s, p x) ↔ ∃ x ∈ s, p ⟨x, ‹x ∈ s›⟩ := -set_coe.exists - -protected lemma subsemiring.forall {s : subsemiring R} {p : s → Prop} : - (∀ x : s, p x) ↔ ∀ x ∈ s, p ⟨x, ‹x ∈ s›⟩ := -set_coe.forall - namespace subsemiring variables (s : subsemiring R) -/-- Two subsemirings are equal if the underlying subsets are equal. -/ -theorem ext' ⦃s t : subsemiring R⦄ (h : (s : set R) = t) : s = t := -by cases s; cases t; congr' - -/-- Two subsemirings are equal if and only if the underlying subsets are equal. -/ -protected theorem ext'_iff {s t : subsemiring R} : s = t ↔ (s : set R) = t := -⟨λ h, h ▸ rfl, λ h, ext' h⟩ - -/-- Two subsemirings are equal if they have the same elements. -/ -@[ext] theorem ext {S T : subsemiring R} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := ext' $ set.ext h - /-- A subsemiring contains the semiring's 1. -/ theorem one_mem : (1 : R) ∈ s := s.one_mem' @@ -204,21 +188,6 @@ subtype.coe_injective.linear_ordered_semiring coe rfl rfl (λ _ _, rfl) (λ _ _, /-! Note: currently, there is no `linear_ordered_comm_semiring`. -/ -instance : partial_order (subsemiring R) := -{ le := λ s t, ∀ ⦃x⦄, x ∈ s → x ∈ t, - .. partial_order.lift (coe : subsemiring R → set R) ext' } - -lemma le_def {s t : subsemiring R} : s ≤ t ↔ ∀ ⦃x : R⦄, x ∈ s → x ∈ t := iff.rfl - -@[simp, norm_cast] lemma coe_subset_coe {s t : subsemiring R} : (s : set R) ⊆ t ↔ s ≤ t := iff.rfl - -@[simp, norm_cast] lemma coe_ssubset_coe {s t : subsemiring R} : (s : set R) ⊂ t ↔ s < t := iff.rfl - -@[simp, norm_cast] -lemma mem_coe {S : subsemiring R} {m : R} : m ∈ (S : set R) ↔ m ∈ S := iff.rfl - -@[simp, norm_cast] -lemma coe_coe (s : subsemiring R) : ↥(s : set R) = s := rfl @[simp] lemma mem_to_submonoid {s : subsemiring R} {x : R} : x ∈ s.to_submonoid ↔ x ∈ s := iff.rfl @[simp] lemma coe_to_submonoid (s : subsemiring R) : (s.to_submonoid : set R) = s := rfl @@ -260,7 +229,7 @@ def map (f : R →+* S) (s : subsemiring R) : subsemiring S := set.mem_image_iff_bex lemma map_map (g : S →+* T) (f : R →+* S) : (s.map f).map g = s.map (g.comp f) := -ext' $ set.image_image _ _ _ +set_like.coe_injective $ set.image_image _ _ _ lemma map_le_iff_le_comap {f : R →+* S} {s : subsemiring R} {t : subsemiring S} : s.map f ≤ t ↔ s ≤ t.comap f := @@ -341,7 +310,8 @@ instance : complete_lattice (subsemiring R) := inf_le_right := λ s t x, and.right, le_inf := λ s t₁ t₂ h₁ h₂ x hx, ⟨h₁ hx, h₂ hx⟩, .. complete_lattice_of_Inf (subsemiring R) - (λ s, is_glb.of_image (λ s t, show (s : set R) ≤ t ↔ s ≤ t, from coe_subset_coe) is_glb_binfi)} + (λ s, is_glb.of_image (λ s t, + show (s : set R) ≤ t ↔ s ≤ t, from set_like.coe_subset_coe) is_glb_binfi)} lemma eq_top_iff' (A : subsemiring R) : A = ⊤ ↔ ∀ x : R, x ∈ A := eq_top_iff.trans ⟨λ h m, h $ mem_top m, λ h m _, h m⟩ @@ -504,7 +474,7 @@ lemma mem_supr_of_directed {ι} [hι : nonempty ι] {S : ι → subsemiring R} ( {x : R} : x ∈ (⨆ i, S i) ↔ ∃ i, x ∈ S i := begin - refine ⟨_, λ ⟨i, hi⟩, (le_def.1 $ le_supr S i) hi⟩, + refine ⟨_, λ ⟨i, hi⟩, (set_like.le_def.1 $ le_supr S i) hi⟩, let U : subsemiring R := subsemiring.mk' (⋃ i, (S i : set R)) (⨆ i, (S i).to_submonoid) (submonoid.coe_supr_of_directed $ hS.mono_comp _ (λ _ _, id)) (⨆ i, (S i).to_add_submonoid) (add_submonoid.coe_supr_of_directed $ hS.mono_comp _ (λ _ _, id)), @@ -562,7 +532,7 @@ lemma srange_restrict_surjective (f : R →+* S) : function.surjective f.srange_ lemma srange_top_iff_surjective {f : R →+* S} : f.srange = (⊤ : subsemiring S) ↔ function.surjective f := -subsemiring.ext'_iff.trans $ iff.trans (by rw [coe_srange, coe_top]) set.range_iff_surjective +set_like.ext'_iff.trans $ iff.trans (by rw [coe_srange, coe_top]) set.range_iff_surjective /-- The range of a surjective ring homomorphism is the whole of the codomain. -/ lemma srange_top_of_surjective (f : R →+* S) (hf : function.surjective f) : @@ -588,7 +558,7 @@ eq_of_eq_on_stop $ hs ▸ eq_on_sclosure h lemma sclosure_preimage_le (f : R →+* S) (s : set S) : closure (f ⁻¹' s) ≤ (closure s).comap f := -closure_le.2 $ λ x hx, mem_coe.2 $ mem_comap.2 $ subset_closure hx +closure_le.2 $ λ x hx, set_like.mem_coe.2 $ mem_comap.2 $ subset_closure hx /-- The image under a ring homomorphism of the subsemiring generated by a set equals the subsemiring generated by the image of the set. -/ @@ -610,7 +580,7 @@ def inclusion {S T : subsemiring R} (h : S ≤ T) : S →* T := S.subtype.cod_srestrict _ (λ x, h x.2) @[simp] lemma srange_subtype (s : subsemiring R) : s.subtype.srange = s := -ext' $ (coe_srange _).trans subtype.range_coe +set_like.coe_injective $ (coe_srange _).trans subtype.range_coe @[simp] lemma range_fst : (fst R S).srange = ⊤ := @@ -625,8 +595,8 @@ lemma prod_bot_sup_bot_prod (s : subsemiring R) (t : subsemiring S) : (s.prod ⊥) ⊔ (prod ⊥ t) = s.prod t := le_antisymm (sup_le (prod_mono_right s bot_le) (prod_mono_left t bot_le)) $ assume p hp, prod.fst_mul_snd p ▸ mul_mem _ - ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, mem_coe.2 $ one_mem ⊥⟩) - ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨mem_coe.2 $ one_mem ⊥, hp.2⟩) + ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, set_like.mem_coe.2 $ one_mem ⊥⟩) + ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨set_like.mem_coe.2 $ one_mem ⊥, hp.2⟩) end subsemiring @@ -637,7 +607,7 @@ variables {s t : subsemiring R} /-- Makes the identity isomorphism from a proof two subsemirings of a multiplicative monoid are equal. -/ def subsemiring_congr (h : s = t) : s ≃+* t := -{ map_mul' := λ _ _, rfl, map_add' := λ _ _, rfl, ..equiv.set_congr $ subsemiring.ext'_iff.1 h } +{ map_mul' := λ _ _, rfl, map_add' := λ _ _, rfl, ..equiv.set_congr $ congr_arg _ h } /-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its `ring_hom.srange`. -/ diff --git a/src/topology/algebra/open_subgroup.lean b/src/topology/algebra/open_subgroup.lean index 153dcb5dc50aa..19238c39b6f0e 100644 --- a/src/topology/algebra/open_subgroup.lean +++ b/src/topology/algebra/open_subgroup.lean @@ -176,14 +176,14 @@ variables {G : Type*} [group G] [topological_space G] [has_continuous_mul G] (H lemma is_open_of_mem_nhds {g : G} (hg : (H : set G) ∈ 𝓝 g) : is_open (H : set G) := begin - simp only [is_open_iff_mem_nhds, subgroup.mem_coe] at hg ⊢, + simp only [is_open_iff_mem_nhds, set_like.mem_coe] at hg ⊢, intros x hx, have : filter.tendsto (λ y, y * (x⁻¹ * g)) (𝓝 x) (𝓝 $ x * (x⁻¹ * g)) := (continuous_id.mul continuous_const).tendsto _, rw [mul_inv_cancel_left] at this, have := filter.mem_map.1 (this hg), - replace hg : g ∈ H := subgroup.mem_coe.1 (mem_of_nhds hg), - simp only [subgroup.mem_coe, H.mul_mem_cancel_right (H.mul_mem (H.inv_mem hx) hg)] at this, + replace hg : g ∈ H := set_like.mem_coe.1 (mem_of_nhds hg), + simp only [set_like.mem_coe, H.mul_mem_cancel_right (H.mul_mem (H.inv_mem hx) hg)] at this, exact this end diff --git a/src/topology/continuous_function/algebra.lean b/src/topology/continuous_function/algebra.lean index c0db507cd6a20..af0b8857accc8 100644 --- a/src/topology/continuous_function/algebra.lean +++ b/src/topology/continuous_function/algebra.lean @@ -413,7 +413,7 @@ begin refine ⟨f', _, _, _⟩, { simp only [set.mem_image, coe_coe], refine ⟨f', _, rfl⟩, - simp only [f', submodule.mem_coe, subalgebra.mem_to_submodule], + simp only [f', set_like.mem_coe, subalgebra.mem_to_submodule], -- TODO should there be a tactic for this? -- We could add an attribute `@[subobject_mem]`, and a tactic -- ``def subobject_mem := `[solve_by_elim with subobject_mem { max_depth := 10 }]``