chore(topology/*): golf some proofs (#4528)

* move `exists_nhds_split` to `topology/algebra/monoid`, rename to `exists_nhds_one_split`;
* add a version `exists_open_nhds_one_split`;
* move `exists_nhds_split4` to `topology/algebra/monoid`, rename to `exists_nhds_one_split4`;
* move `one_open_separated_mul` to `topology/algebra/monoid`, rename to `exists_open_nhds_one_mul_subset`;
* add `mem_prod_nhds_iff`;
* golf some proofs.

src/topology/algebra/group.lean

@@ -126,39 +126,12 @@ protected def homeomorph.inv (G : Type*) [topological_space G] [group G] [topolo
   continuous_inv_fun := continuous_inv,
   .. equiv.inv G }
 
-@[to_additive exists_nhds_half]
-lemma exists_nhds_split [topological_group G] {s : set G} (hs : s ∈ 𝓝 (1 : G)) :
-  ∃ V ∈ 𝓝 (1 : G), ∀ v w ∈ V, v * w ∈ s :=
-begin
-  have : ((λa:G×G, a.1 * a.2) ⁻¹' s) ∈ 𝓝 ((1, 1) : G × G) :=
-    tendsto_mul (by simpa using hs),
-  rw nhds_prod_eq at this,
-  rcases mem_prod_iff.1 this with ⟨V₁, H₁, V₂, H₂, H⟩,
-  exact ⟨V₁ ∩ V₂, inter_mem_sets H₁ H₂, assume v w ⟨hv, _⟩ ⟨_, hw⟩, @H (v, w) ⟨hv, hw⟩⟩
-end
-
 @[to_additive exists_nhds_half_neg]
 lemma exists_nhds_split_inv [topological_group G] {s : set G} (hs : s ∈ 𝓝 (1 : G)) :
   ∃ V ∈ 𝓝 (1 : G), ∀ (v ∈ V) (w ∈ V), v * w⁻¹ ∈ s :=
-begin
-  have : tendsto (λa:G×G, a.1 * (a.2)⁻¹) (𝓝 (1:G) ×ᶠ 𝓝 (1:G)) (𝓝 1),
-  { simpa using (@tendsto_fst G G (𝓝 1) (𝓝 1)).mul tendsto_snd.inv },
-  have : ((λa:G×G, a.1 * (a.2)⁻¹) ⁻¹' s) ∈ 𝓝 (1:G) ×ᶠ 𝓝 (1:G) :=
-    this (by simpa using hs),
-  rcases mem_prod_self_iff.1 this with ⟨V, H, H'⟩,
-  exact ⟨V, H, prod_subset_iff.1 H'⟩
-end
-
-@[to_additive exists_nhds_quarter]
-lemma exists_nhds_split4 [topological_group G] {u : set G} (hu : u ∈ 𝓝 (1 : G)) :
-  ∃ V ∈ 𝓝 (1 : G), ∀ {v w s t}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u :=
-begin
-  rcases exists_nhds_split hu with ⟨W, W_nhd, h⟩,
-  rcases exists_nhds_split W_nhd with ⟨V, V_nhd, h'⟩,
-  existsi [V, V_nhd],
-  intros v w s t v_in w_in s_in t_in,
-  simpa [mul_assoc] using h _ _ (h' v w v_in w_in) (h' s t s_in t_in)
-end
+have ((λp : G × G, p.1 * p.2⁻¹) ⁻¹' s) ∈ 𝓝 ((1, 1) : G × G),
+  from continuous_at_fst.mul continuous_at_snd.inv (by simpa),
+by simpa only [nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage]
 
 section
 variable (G)
@@ -371,16 +344,13 @@ lemma topological_group.t1_space (h : @is_closed G _ {1}) : t1_space G :=
 lemma topological_group.regular_space [t1_space G] : regular_space G :=
 ⟨assume s a hs ha,
  let f := λ p : G × G, p.1 * (p.2)⁻¹ in
- have hf : continuous f :=
-   continuous_mul.comp (continuous_fst.prod_mk (continuous_inv.comp continuous_snd)),
+ have hf : continuous f := continuous_fst.mul continuous_snd.inv,
  -- a ∈ -s implies f (a, 1) ∈ -s, and so (a, 1) ∈ f⁻¹' (-s);
  -- and so can find t₁ t₂ open such that a ∈ t₁ × t₂ ⊆ f⁻¹' (-s)
  let ⟨t₁, t₂, ht₁, ht₂, a_mem_t₁, one_mem_t₂, t_subset⟩ :=
    is_open_prod_iff.1 (hf _ (is_open_compl_iff.2 hs)) a (1:G) (by simpa [f]) in
  begin
-   use s * t₂,
-   use is_open_mul_left ht₂,
-   use λ x hx, ⟨x, 1, hx, one_mem_t₂, mul_one _⟩,
+   use [s * t₂, is_open_mul_left ht₂, λ x hx, ⟨x, 1, hx, one_mem_t₂, mul_one _⟩],
    apply inf_principal_eq_bot,
    rw mem_nhds_sets_iff,
    refine ⟨t₁, _, ht₁, a_mem_t₁⟩,
@@ -401,18 +371,6 @@ section
 /-! Some results about an open set containing the product of two sets in a topological group. -/
 
 variables [topological_space G] [group G] [topological_group G]
-/-- Given a open neighborhood `U` of `1` there is a open neighborhood `V` of `1`
-  such that `VV ⊆ U`. -/
-@[to_additive "Given a open neighborhood `U` of `0` there is a open neighborhood `V` of `0`
-  such that `V + V ⊆ U`."]
-lemma one_open_separated_mul {U : set G} (h1U : is_open U) (h2U : (1 : G) ∈ U) :
-  ∃ V : set G, is_open V ∧ (1 : G) ∈ V ∧ V * V ⊆ U :=
-begin
-  rcases exists_nhds_square (continuous_mul U h1U) (by simp only [mem_preimage, one_mul, h2U] :
-    ((1 : G), (1 : G)) ∈ (λ p : G × G, p.1 * p.2) ⁻¹' U) with ⟨V, h1V, h2V, h3V⟩,
-  refine ⟨V, h1V, h2V, _⟩,
-  rwa [← image_subset_iff, image_mul_prod] at h3V
-end
 
 /-- Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `1`
   such that `KV ⊆ U`. -/
@@ -424,7 +382,7 @@ begin
   let W : G → set G := λ x, (λ y, x * y) ⁻¹' U,
   have h1W : ∀ x, is_open (W x) := λ x, continuous_mul_left x U hU,
   have h2W : ∀ x ∈ K, (1 : G) ∈ W x := λ x hx, by simp only [mem_preimage, mul_one, hKU hx],
-  choose V hV using λ x : K, one_open_separated_mul (h1W x) (h2W x.1 x.2),
+  choose V hV using λ x : K, exists_open_nhds_one_mul_subset (mem_nhds_sets (h1W x) (h2W x.1 x.2)),
   let X : K → set G := λ x, (λ y, (x : G)⁻¹ * y) ⁻¹' (V x),
   cases hK.elim_finite_subcover X (λ x, continuous_mul_left x⁻¹ (V x) (hV x).1) _ with t ht, swap,
   { intros x hx, rw [mem_Union], use ⟨x, hx⟩, rw [mem_preimage], convert (hV _).2.1,
@@ -466,12 +424,12 @@ begin
   rw [← nhds_translation_mul_inv x, ← nhds_translation_mul_inv y, ← nhds_translation_mul_inv (x*y)],
   split,
   { rintros ⟨t, ht, ts⟩,
-    rcases exists_nhds_split ht with ⟨V, V_mem, h⟩,
+    rcases exists_nhds_one_split ht with ⟨V, V1, h⟩,
     refine ⟨(λa, a * x⁻¹) ⁻¹' V, (λa, a * y⁻¹) ⁻¹' V,
-            ⟨V, V_mem, subset.refl _⟩, ⟨V, V_mem, subset.refl _⟩, _⟩,
+            ⟨V, V1, subset.refl _⟩, ⟨V, V1, subset.refl _⟩, _⟩,
     rintros a ⟨v, w, v_mem, w_mem, rfl⟩,
     apply ts,
-    simpa [mul_comm, mul_assoc, mul_left_comm] using h (v * x⁻¹) (w * y⁻¹) v_mem w_mem },
+    simpa [mul_comm, mul_assoc, mul_left_comm] using h (v * x⁻¹) v_mem (w * y⁻¹) w_mem },
   { rintros ⟨a, c, ⟨b, hb, ba⟩, ⟨d, hd, dc⟩, ac⟩,
     refine ⟨b ∩ d, inter_mem_sets hb hd, assume v, _⟩,
     simp only [preimage_subset_iff, mul_inv_rev, mem_preimage] at *,

src/topology/algebra/monoid.lean

@@ -2,12 +2,19 @@
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
-
-Theory of topological monoids.
 -/
 import topology.continuous_on
 import group_theory.submonoid.basic
 import algebra.group.prod
+import algebra.pointwise
+
+/-!
+# Theory of topological monoids
+
+In this file we define mixin classes `has_continuous_mul` and `has_continuous_add`. While in many
+applications the underlying type is a monoid (multiplicative or additive), we do not require this in
+the definitions.
+-/
 
 open classical set filter topological_space
 open_locale classical topological_space big_operators
@@ -90,6 +97,44 @@ section has_continuous_mul
 
 variables [topological_space M] [monoid M] [has_continuous_mul M]
 
+@[to_additive exists_open_nhds_zero_half]
+lemma exists_open_nhds_one_split {s : set M} (hs : s ∈ 𝓝 (1 : M)) :
+  ∃ V : set M, is_open V ∧ (1 : M) ∈ V ∧ ∀ (v ∈ V) (w ∈ V), v * w ∈ s :=
+have ((λa:M×M, a.1 * a.2) ⁻¹' s) ∈ 𝓝 ((1, 1) : M × M),
+  from tendsto_mul (by simpa only [one_mul] using hs),
+by simpa only [prod_subset_iff] using exists_nhds_square this
+
+@[to_additive exists_nhds_zero_half]
+lemma exists_nhds_one_split {s : set M} (hs : s ∈ 𝓝 (1 : M)) :
+  ∃ V ∈ 𝓝 (1 : M), ∀ (v ∈ V) (w ∈ V), v * w ∈ s :=
+let ⟨V, Vo, V1, hV⟩ := exists_open_nhds_one_split hs
+in ⟨V, mem_nhds_sets Vo V1, hV⟩
+
+@[to_additive exists_nhds_zero_quarter]
+lemma exists_nhds_one_split4 {u : set M} (hu : u ∈ 𝓝 (1 : M)) :
+  ∃ V ∈ 𝓝 (1 : M),
+    ∀ {v w s t}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u :=
+begin
+  rcases exists_nhds_one_split hu with ⟨W, W1, h⟩,
+  rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩,
+  use [V, V1],
+  intros v w s t v_in w_in s_in t_in,
+  simpa only [mul_assoc] using h _ (h' v v_in w w_in) _ (h' s s_in t t_in)
+end
+
+/-- Given a neighborhood `U` of `1` there is an open neighborhood `V` of `1`
+such that `VV ⊆ U`. -/
+@[to_additive "Given a open neighborhood `U` of `0` there is a open neighborhood `V` of `0`
+  such that `V + V ⊆ U`."]
+lemma exists_open_nhds_one_mul_subset {U : set M} (hU : U ∈ 𝓝 (1 : M)) :
+  ∃ V : set M, is_open V ∧ (1 : M) ∈ V ∧ V * V ⊆ U :=
+begin
+  rcases exists_open_nhds_one_split hU with ⟨V, Vo, V1, hV⟩,
+  use [V, Vo, V1],
+  rintros _ ⟨x, y, hx, hy, rfl⟩,
+  exact hV _ hx _ hy
+end
+
 @[to_additive]
 lemma tendsto_list_prod {f : β → α → M} {x : filter α} {a : β → M} :
   ∀l:list β, (∀c∈l, tendsto (f c) x (𝓝 (a c))) →

src/topology/algebra/uniform_group.lean

@@ -162,7 +162,7 @@ def topological_add_group.to_uniform_space : uniform_space G :=
     intros D H,
     rw mem_lift'_sets,
     { rcases H with ⟨U, U_nhds, U_sub⟩,
-      rcases exists_nhds_half U_nhds with ⟨V, ⟨V_nhds, V_sum⟩⟩,
+      rcases exists_nhds_zero_half U_nhds with ⟨V, ⟨V_nhds, V_sum⟩⟩,
       existsi ((λp:G×G, p.2 - p.1) ⁻¹' V),
       have H : (λp:G×G, p.2 - p.1) ⁻¹' V ∈ comap (λp:G×G, p.2 - p.1) (𝓝 (0 : G)),
         by existsi [V, V_nhds] ; refl,
@@ -171,7 +171,7 @@ def topological_add_group.to_uniform_space : uniform_space G :=
       begin
         intros p p_comp_rel,
         rcases p_comp_rel with ⟨z, ⟨Hz1, Hz2⟩⟩,
-        simpa [sub_eq_add_neg, add_comm, add_left_comm] using V_sum _ _ Hz1 Hz2
+        simpa [sub_eq_add_neg, add_comm, add_left_comm] using V_sum _ Hz1 _ Hz2
       end,
       exact set.subset.trans comp_rel_sub U_sub },
     { exact monotone_comp_rel monotone_id monotone_id }
@@ -390,7 +390,7 @@ begin
     rw ← nhds_prod_eq at lim_sub_sub,
     exact tendsto.comp lim_φ lim_sub_sub },
 
-  rcases exists_nhds_quarter W'_nhd with ⟨W, W_nhd, W4⟩,
+  rcases exists_nhds_zero_quarter W'_nhd with ⟨W, W_nhd, W4⟩,
 
   have : ∃ U₁ ∈ comap e (𝓝 x₀), ∃ V₁ ∈ comap f (𝓝 y₀),
     ∀ x x' ∈ U₁, ∀ y y' ∈ V₁,  φ (x'-x, y'-y) ∈ W,

src/topology/constructions.lean

@@ -157,6 +157,16 @@ is_open_inter (continuous_fst s hs) (continuous_snd t ht)
 lemma nhds_prod_eq {a : α} {b : β} : 𝓝 (a, b) = 𝓝 a ×ᶠ 𝓝 b :=
 by rw [filter.prod, prod.topological_space, nhds_inf, nhds_induced, nhds_induced]
 
+lemma mem_nhds_prod_iff {a : α} {b : β} {s : set (α × β)} :
+  s ∈ 𝓝 (a, b) ↔ ∃ (u ∈ 𝓝 a) (v ∈ 𝓝 b), set.prod u v ⊆ s :=
+by rw [nhds_prod_eq, mem_prod_iff]
+
+lemma filter.has_basis.prod_nhds {ιa ιb : Type*} {pa : ιa → Prop} {pb : ιb → Prop}
+  {sa : ιa → set α} {sb : ιb → set β} {a : α} {b : β} (ha : (𝓝 a).has_basis pa sa)
+  (hb : (𝓝 b).has_basis pb sb) :
+  (𝓝 (a, b)).has_basis (λ i : ιa × ιb, pa i.1 ∧ pb i.2) (λ i, (sa i.1).prod (sb i.2)) :=
+by { rw nhds_prod_eq, exact ha.prod hb }
+
 instance [discrete_topology α] [discrete_topology β] : discrete_topology (α × β) :=
 ⟨eq_of_nhds_eq_nhds $ assume ⟨a, b⟩,
   by rw [nhds_prod_eq, nhds_discrete α, nhds_discrete β, nhds_bot, filter.prod_pure_pure]⟩
@@ -233,40 +243,25 @@ lemma is_open_prod_iff {s : set (α×β)} : is_open s ↔
   (∀a b, (a, b) ∈ s → ∃u v, is_open u ∧ is_open v ∧ a ∈ u ∧ b ∈ v ∧ set.prod u v ⊆ s) :=
 begin
   rw [is_open_iff_nhds],
-  simp [nhds_prod_eq, mem_prod_iff],
-  simp [mem_nhds_sets_iff],
-  exact forall_congr (assume a, ball_congr $ assume b h,
-    ⟨assume ⟨u', ⟨u, us, uo, au⟩, v', ⟨v, vs, vo, bv⟩, h⟩,
-      ⟨u, uo, v, vo, au, bv, subset.trans (set.prod_mono us vs) h⟩,
-      assume ⟨u, uo, v, vo, au, bv, h⟩,
-      ⟨u, ⟨u, subset.refl u, uo, au⟩, v, ⟨v, subset.refl v, vo, bv⟩, h⟩⟩)
+  simp_rw [le_principal_iff, prod.forall,
+    ((nhds_basis_opens _).prod_nhds (nhds_basis_opens _)).mem_iff, prod.exists, exists_prop],
+  simp only [and_assoc, and.left_comm]
 end
 
-/-- Given an open neighborhood `s` of `(x, x)`, then `(x, x)` has a square open neighborhood
+/-- Given a neighborhood `s` of `(x, x)`, then `(x, x)` has a square open neighborhood
   that is a subset of `s`. -/
-lemma exists_nhds_square {s : set (α × α)} (hs : is_open s) {x : α} (hx : (x, x) ∈ s) :
+lemma exists_nhds_square {s : set (α × α)} {x : α} (hx : s ∈ 𝓝 (x, x)) :
   ∃U, is_open U ∧ x ∈ U ∧ set.prod U U ⊆ s :=
-begin
-  rcases is_open_prod_iff.mp hs x x hx with ⟨u, v, hu, hv, h1x, h2x, h2s⟩,
-  refine ⟨u ∩ v, is_open_inter hu hv, ⟨h1x, h2x⟩, subset.trans _ h2s⟩,
-  simp only [prod_subset_prod_iff, inter_subset_left, true_or, inter_subset_right, and_self],
-end
+by simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and.assoc, and.left_comm] using hx
 
 /-- The first projection in a product of topological spaces sends open sets to open sets. -/
 lemma is_open_map_fst : is_open_map (@prod.fst α β) :=
 begin
-  assume s hs,
-  rw is_open_iff_forall_mem_open,
-  assume x xs,
-  rw mem_image_eq at xs,
-  rcases xs with ⟨⟨y₁, y₂⟩, ys, yx⟩,
-  rcases is_open_prod_iff.1 hs _ _ ys with ⟨o₁, o₂, o₁_open, o₂_open, yo₁, yo₂, ho⟩,
-  simp at yx,
-  rw yx at yo₁,
-  refine ⟨o₁, _, o₁_open, yo₁⟩,
-  assume z zs,
-  rw mem_image_eq,
-  exact ⟨(z, y₂), ho (by simp [zs, yo₂]), rfl⟩
+  rw is_open_map_iff_nhds_le,
+  rintro ⟨x, y⟩ s hs,
+  rcases mem_nhds_prod_iff.1 hs with ⟨tx, htx, ty, hty, ht⟩,
+  simp only [subset_def, prod.forall, mem_prod] at ht,
+  exact mem_sets_of_superset htx (λ x hx, ht x y ⟨hx, mem_of_nhds hty⟩)
 end
 
 /-- The second projection in a product of topological spaces sends open sets to open sets. -/
@@ -275,18 +270,11 @@ begin
   /- This lemma could be proved by composing the fact that the first projection is open, and
   exchanging coordinates is a homeomorphism, hence open. As the `prod_comm` homeomorphism is defined
   later, we rather go for the direct proof, copy-pasting the proof for the first projection. -/
-  assume s hs,
-  rw is_open_iff_forall_mem_open,
-  assume x xs,
-  rw mem_image_eq at xs,
-  rcases xs with ⟨⟨y₁, y₂⟩, ys, yx⟩,
-  rcases is_open_prod_iff.1 hs _ _ ys with ⟨o₁, o₂, o₁_open, o₂_open, yo₁, yo₂, ho⟩,
-  simp at yx,
-  rw yx at yo₂,
-  refine ⟨o₂, _, o₂_open, yo₂⟩,
-  assume z zs,
-  rw mem_image_eq,
-  exact ⟨(y₁, z), ho (by simp [zs, yo₁]), rfl⟩
+  rw is_open_map_iff_nhds_le,
+  rintro ⟨x, y⟩ s hs,
+  rcases mem_nhds_prod_iff.1 hs with ⟨tx, htx, ty, hty, ht⟩,
+  simp only [subset_def, prod.forall, mem_prod] at ht,
+  exact mem_sets_of_superset hty (λ y hy, ht x y ⟨mem_of_nhds htx, hy⟩)
 end
 
 /-- A product set is open in a product space if and only if each factor is open, or one of them is
@@ -307,7 +295,7 @@ begin
       { rw ← snd_image_prod st.1 t,
         exact is_open_map_snd _ H } },
     { assume H,
-      simp [st.1.ne_empty, st.2.ne_empty] at H,
+      simp only [st.1.ne_empty, st.2.ne_empty, not_false_iff, or_false] at H,
       exact H.1.prod H.2 } }
 end