refactor(topology/algebra/open_subgroup): use set_like (#18585)

urkud · urkud · commit 83f81aea3393 · 2023-03-15T14:32:21.000Z
diff --git a/src/field_theory/krull_topology.lean b/src/field_theory/krull_topology.lean
@@ -210,9 +210,7 @@ begin
   have h_basis : E.fixing_subgroup.carrier ∈ (gal_group_basis K L) :=
    ⟨E.fixing_subgroup, ⟨E, ‹_›, rfl⟩, rfl⟩,
   have h_nhd := group_filter_basis.mem_nhds_one (gal_group_basis K L) h_basis,
-  rw mem_nhds_iff at h_nhd,
-  rcases h_nhd with ⟨U, hU_le, hU_open, h1U⟩,
-  exact subgroup.is_open_of_one_mem_interior ⟨U, ⟨hU_open, hU_le⟩, h1U⟩,
+  exact subgroup.is_open_of_mem_nhds _ h_nhd
 end
 
 /-- Given a tower of fields `L/E/K`, with `E/K` finite, the subgroup `Gal(L/E) ≤ L ≃ₐ[K] L` is
diff --git a/src/topology/algebra/nonarchimedean/basic.lean b/src/topology/algebra/nonarchimedean/basic.lean
@@ -127,14 +127,13 @@ lemma mul_subset (U : open_add_subgroup R) :
   ∃ V : open_add_subgroup R, (V : set R) * V ⊆ U :=
 let ⟨V, H⟩ := prod_self_subset (is_open.mem_nhds (is_open.preimage continuous_mul U.is_open)
   begin
-    simpa only [set.mem_preimage, open_add_subgroup.mem_coe, prod.snd_zero, mul_zero]
-      using U.zero_mem,
+    simpa only [set.mem_preimage, set_like.mem_coe, prod.snd_zero, mul_zero] using U.zero_mem,
   end) in
 begin
   use V,
   rintros v ⟨a, b, ha, hb, hv⟩,
   have hy := H (set.mk_mem_prod ha hb),
-  simp only [set.mem_preimage, open_add_subgroup.mem_coe] at hy,
+  simp only [set.mem_preimage, set_like.mem_coe] at hy,
   rwa hv at hy
 end
 
diff --git a/src/topology/algebra/open_subgroup.lean b/src/topology/algebra/open_subgroup.lean
@@ -55,44 +55,39 @@ variables {G : Type*} [group G] [topological_space G]
 variables {U V : open_subgroup G} {g : G}
 
 @[to_additive]
-instance has_coe_set : has_coe_t (open_subgroup G) (set G) := ⟨λ U, U.1⟩
+instance has_coe_subgroup : has_coe_t (open_subgroup G) (subgroup G) := ⟨to_subgroup⟩
 
 @[to_additive]
-instance : has_mem G (open_subgroup G) := ⟨λ g U, g ∈ (U : set G)⟩
+lemma coe_subgroup_injective : injective (coe : open_subgroup G → subgroup G)
+| ⟨_, _⟩ ⟨_, _⟩ rfl := rfl
 
 @[to_additive]
-instance has_coe_subgroup : has_coe_t (open_subgroup G) (subgroup G) := ⟨to_subgroup⟩
+instance : set_like (open_subgroup G) G :=
+{ coe := λ U, U.1,
+  coe_injective' := λ _ _ h, coe_subgroup_injective $ set_like.ext' h }
+
+@[to_additive]
+instance : subgroup_class (open_subgroup G) G :=
+{ mul_mem := λ U _ _, U.mul_mem',
+  one_mem := λ U, U.one_mem',
+  inv_mem := λ U _, U.inv_mem' }
 
 @[to_additive]
 instance has_coe_opens : has_coe_t (open_subgroup G) (opens G) := ⟨λ U, ⟨U, U.is_open'⟩⟩
 
-@[simp, norm_cast, to_additive] lemma mem_coe : g ∈ (U : set G) ↔ g ∈ U := iff.rfl
+@[simp, norm_cast, to_additive] lemma coe_coe_opens : ((U : opens G) : set G) = U := rfl
+@[simp, norm_cast, to_additive] lemma coe_coe_subgroup : ((U : subgroup G) : set G) = U := rfl
 @[simp, norm_cast, to_additive] lemma mem_coe_opens : g ∈ (U : opens G) ↔ g ∈ U := iff.rfl
 @[simp, norm_cast, to_additive]
 lemma mem_coe_subgroup : g ∈ (U : subgroup G) ↔ g ∈ U := iff.rfl
 
-@[to_additive] lemma coe_injective : injective (coe : open_subgroup G → set G) :=
-by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨h⟩, congr, }
-
 @[ext, to_additive]
-lemma ext (h : ∀ x, x ∈ U ↔ x ∈ V) : (U = V) := coe_injective $ set.ext h
-
-@[to_additive]
-lemma ext_iff : (U = V) ↔ (∀ x, x ∈ U ↔ x ∈ V) := ⟨λ h x, h ▸ iff.rfl, ext⟩
+lemma ext (h : ∀ x, x ∈ U ↔ x ∈ V) : (U = V) := set_like.ext h
 
 variable (U)
 @[to_additive]
 protected lemma is_open : is_open (U : set G) := U.is_open'
 
-@[to_additive]
-protected lemma one_mem : (1 : G) ∈ U := U.one_mem'
-
-@[to_additive]
-protected lemma inv_mem {g : G} (h : g ∈ U) : g⁻¹ ∈ U := U.inv_mem' h
-
-@[to_additive]
-protected lemma mul_mem {g₁ g₂ : G} (h₁ : g₁ ∈ U) (h₂ : g₂ ∈ U) : g₁ * g₂ ∈ U := U.mul_mem' h₁ h₂
-
 @[to_additive]
 lemma mem_nhds_one : (U : set G) ∈ 𝓝 (1 : G) :=
 is_open.mem_nhds U.is_open U.one_mem
@@ -101,6 +96,15 @@ variable {U}
 @[to_additive]
 instance : has_top (open_subgroup G) := ⟨{ is_open' := is_open_univ, .. (⊤ : subgroup G) }⟩
 
+@[simp, to_additive] lemma mem_top (x : G) : x ∈ (⊤ : open_subgroup G) := trivial
+@[simp, norm_cast, to_additive] lemma coe_top : ((⊤ : open_subgroup G) : set G) = set.univ := rfl
+
+@[simp, norm_cast, to_additive]
+lemma coe_subgroup_top : ((⊤ : open_subgroup G) : subgroup G) = ⊤ := rfl
+
+@[simp, norm_cast, to_additive]
+lemma coe_opens_top : ((⊤ : open_subgroup G) : opens G) = ⊤ := rfl
+
 @[to_additive]
 instance : inhabited (open_subgroup G) := ⟨⊤⟩
 
@@ -109,67 +113,79 @@ lemma is_closed [has_continuous_mul G] (U : open_subgroup G) : is_closed (U : se
 begin
   apply is_open_compl_iff.1,
   refine is_open_iff_forall_mem_open.2 (λ x hx, ⟨(λ y, y * x⁻¹) ⁻¹' U, _, _, _⟩),
-  { intros u hux,
-    simp only [set.mem_preimage, set.mem_compl_iff, mem_coe] at hux hx ⊢,
-    refine mt (λ hu, _) hx,
+  { refine λ u hux hu, hx _,
+    simp only [set.mem_preimage, set_like.mem_coe] at hux hu ⊢,
     convert U.mul_mem (U.inv_mem hux) hu,
     simp },
   { exact U.is_open.preimage (continuous_mul_right _) },
-  { simp [U.one_mem] }
+  { simp [one_mem] }
 end
 
+@[to_additive]
+lemma is_clopen [has_continuous_mul G] (U : open_subgroup G) : is_clopen (U : set G) :=
+⟨U.is_open, U.is_closed⟩
+
 section
 variables {H : Type*} [group H] [topological_space H]
 
 /-- The product of two open subgroups as an open subgroup of the product group. -/
 @[to_additive "The product of two open subgroups as an open subgroup of the product group."]
 def prod (U : open_subgroup G) (V : open_subgroup H) : open_subgroup (G × H) :=
-{ carrier := U ×ˢ V,
-  is_open' := U.is_open.prod V.is_open,
+{ is_open' := U.is_open.prod V.is_open,
   .. (U : subgroup G).prod (V : subgroup H) }
 
+@[simp, norm_cast, to_additive] lemma coe_prod (U : open_subgroup G) (V : open_subgroup H) :
+  (U.prod V : set (G × H)) = U ×ˢ V :=
+rfl
+
+@[simp, norm_cast, to_additive]
+lemma coe_subgroup_prod (U : open_subgroup G) (V : open_subgroup H) :
+  (U.prod V : subgroup (G × H)) = (U : subgroup G).prod V :=
+rfl
+
 end
 
 @[to_additive]
-instance : partial_order (open_subgroup G) :=
-{ le := λ U V, ∀ ⦃x⦄, x ∈ U → x ∈ V,
-  .. partial_order.lift (coe : open_subgroup G → set G) coe_injective }
+instance : has_inf (open_subgroup G) :=
+⟨λ U V, ⟨U ⊓ V, U.is_open.inter V.is_open⟩⟩
+
+@[simp, norm_cast, to_additive] lemma coe_inf : (↑(U ⊓ V) : set G) = (U : set G) ∩ V := rfl
+@[simp, norm_cast, to_additive] lemma coe_subgroup_inf : (↑(U ⊓ V) : subgroup G) = ↑U ⊓ ↑V := rfl
+@[simp, norm_cast, to_additive] lemma coe_opens_inf : (↑(U ⊓ V) : opens G) = ↑U ⊓ ↑V := rfl
+@[simp, to_additive] lemma mem_inf {x} : x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V := iff.rfl
 
 @[to_additive]
 instance : semilattice_inf (open_subgroup G) :=
-{ inf := λ U V, { is_open' := is_open.inter U.is_open V.is_open, .. (U : subgroup G) ⊓ V },
-  inf_le_left := λ U V, set.inter_subset_left _ _,
-  inf_le_right := λ U V, set.inter_subset_right _ _,
-  le_inf := λ U V W hV hW, set.subset_inter hV hW,
-  ..open_subgroup.partial_order }
+{ .. set_like.partial_order,
+  .. set_like.coe_injective.semilattice_inf (coe : open_subgroup G → set G) (λ _ _, rfl) }
 
 @[to_additive]
 instance : order_top (open_subgroup G) :=
 { top := ⊤,
   le_top := λ U, set.subset_univ _ }
 
-@[simp, norm_cast, to_additive] lemma coe_inf : (↑(U ⊓ V) : set G) = (U : set G) ∩ V := rfl
-
-@[simp, norm_cast, to_additive] lemma coe_subset : (U : set G) ⊆ V ↔ U ≤ V := iff.rfl
-
 @[simp, norm_cast, to_additive] lemma coe_subgroup_le :
-(U : subgroup G) ≤ (V : subgroup G) ↔ U ≤ V := iff.rfl
+  (U : subgroup G) ≤ (V : subgroup G) ↔ U ≤ V :=
+iff.rfl
 
 variables {N : Type*} [group N] [topological_space N]
 
 /-- The preimage of an `open_subgroup` along a continuous `monoid` homomorphism
   is an `open_subgroup`. -/
 @[to_additive "The preimage of an `open_add_subgroup` along a continuous `add_monoid` homomorphism
 is an `open_add_subgroup`."]
-def comap (f : G →* N)
-  (hf : continuous f) (H : open_subgroup N) : open_subgroup G :=
+def comap (f : G →* N) (hf : continuous f) (H : open_subgroup N) : open_subgroup G :=
 { is_open' := H.is_open.preimage hf,
   .. (H : subgroup N).comap f }
 
-@[simp, to_additive]
+@[simp, norm_cast, to_additive]
 lemma coe_comap (H : open_subgroup N) (f : G →* N) (hf : continuous f) :
   (H.comap f hf : set G) = f ⁻¹' H := rfl
 
+@[simp, norm_cast, to_additive]
+lemma coe_subgroup_comap (H : open_subgroup N) (f : G →* N) (hf : continuous f) :
+  (H.comap f hf : subgroup G) = (H : subgroup N).comap f := rfl
+
 @[simp, to_additive]
 lemma mem_comap {H : open_subgroup N} {f : G →* N} {hf : continuous f} {x : G} :
   x ∈ H.comap f hf ↔ f x ∈ H := iff.rfl
@@ -190,45 +206,30 @@ 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, 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 := set_like.mem_coe.1 (mem_of_mem_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
+  refine is_open_iff_mem_nhds.2 (λ x hx, _),
+  have hg' : g ∈ H := set_like.mem_coe.1 (mem_of_mem_nhds hg),
+  have : filter.tendsto (λ y, y * (x⁻¹ * g)) (𝓝 x) (𝓝 g) :=
+    (continuous_id.mul continuous_const).tendsto' _ _ (mul_inv_cancel_left _ _),
+  simpa only [set_like.mem_coe, filter.mem_map',
+    H.mul_mem_cancel_right (H.mul_mem (H.inv_mem hx) hg')] using this hg,
 end
 
 @[to_additive]
-lemma is_open_of_open_subgroup {U : open_subgroup G} (h : U.1 ≤ H) :
+lemma is_open_mono {H₁ H₂ : subgroup G} (h : H₁ ≤ H₂) (h₁ : is_open (H₁ : set G)) :
+  is_open (H₂ : set G) :=
+is_open_of_mem_nhds _ $ filter.mem_of_superset (h₁.mem_nhds $ one_mem H₁) h
+
+@[to_additive]
+lemma is_open_of_open_subgroup {U : open_subgroup G} (h : ↑U ≤ H) :
   is_open (H : set G) :=
-H.is_open_of_mem_nhds (filter.mem_of_superset U.mem_nhds_one h)
+is_open_mono h U.is_open
 
 /-- If a subgroup of a topological group has `1` in its interior, then it is open. -/
 @[to_additive "If a subgroup of an additive topological group has `0` in its interior, then it is
 open."]
-lemma is_open_of_one_mem_interior {G : Type*} [group G] [topological_space G]
-  [topological_group G] {H : subgroup G} (h_1_int : (1 : G) ∈ interior (H : set G)) :
+lemma is_open_of_one_mem_interior (h_1_int : (1 : G) ∈ interior (H : set G)) :
   is_open (H : set G) :=
-begin
-  have h : 𝓝 1 ≤ filter.principal (H : set G) :=
-    nhds_le_of_le h_1_int (is_open_interior) (filter.principal_mono.2 interior_subset),
-  rw is_open_iff_nhds,
-  intros g hg,
-  rw (show 𝓝 g = filter.map ⇑(homeomorph.mul_left g) (𝓝 1), by simp),
-  convert filter.map_mono h,
-  simp only [homeomorph.coe_mul_left, filter.map_principal, set.image_mul_left,
-  filter.principal_eq_iff_eq],
-  ext,
-  simp [H.mul_mem_cancel_left (H.inv_mem hg)],
-end
-
-@[to_additive]
-lemma is_open_mono {H₁ H₂ : subgroup G} (h : H₁ ≤ H₂) (h₁ : is_open (H₁ : set G)) :
-  is_open (H₂ : set G) :=
-@is_open_of_open_subgroup _ _ _ _ H₂ { is_open' := h₁, .. H₁ } h
+is_open_of_mem_nhds H $ mem_interior_iff_mem_nhds.1 h_1_int
 
 end subgroup
 
@@ -237,20 +238,16 @@ namespace open_subgroup
 variables {G : Type*} [group G] [topological_space G] [has_continuous_mul G]
 
 @[to_additive]
-instance : semilattice_sup (open_subgroup G) :=
-{ sup := λ U V,
-  { is_open' := show is_open (((U : subgroup G) ⊔ V : subgroup G) : set G),
-    from subgroup.is_open_mono le_sup_left U.is_open,
-    .. ((U : subgroup G) ⊔ V) },
-  le_sup_left := λ U V, coe_subgroup_le.1 le_sup_left,
-  le_sup_right := λ U V, coe_subgroup_le.1 le_sup_right,
-  sup_le := λ U V W hU hV, coe_subgroup_le.1 (sup_le hU hV),
-  ..open_subgroup.semilattice_inf }
+instance : has_sup (open_subgroup G) :=
+⟨λ U V, ⟨U ⊔ V, subgroup.is_open_mono (le_sup_left : U.1 ≤ U ⊔ V) U.is_open⟩⟩
+
+@[simp, norm_cast, to_additive]
+lemma coe_subgroup_sup (U V : open_subgroup G) : (↑(U ⊔ V) : subgroup G) = ↑U ⊔ ↑V := rfl
 
 @[to_additive]
 instance : lattice (open_subgroup G) :=
-{ ..open_subgroup.semilattice_sup, ..open_subgroup.semilattice_inf }
-
+{ .. open_subgroup.semilattice_inf,
+  .. coe_subgroup_injective.semilattice_sup (coe : open_subgroup G → subgroup G) (λ _ _, rfl) }
 
 end open_subgroup
 
