chore(order/filter, topology/algebra): golf (#18097)

src/order/filter/n_ary.lean

@@ -58,29 +58,15 @@ lemma map_prod_eq_map₂ (m : α → β → γ) (f : filter α) (g : filter β)
   filter.map (λ p : α × β, m p.1 p.2) (f ×ᶠ g) = map₂ m f g :=
 begin
   ext s,
-  split,
-  { intro hmem,
-    rw filter.mem_map_iff_exists_image at hmem,
-    obtain ⟨s', hs', hsub⟩ := hmem,
-    rw filter.mem_prod_iff at hs',
-    obtain ⟨t, ht, t', ht', hsub'⟩ := hs',
-    refine ⟨t, t', ht, ht', _⟩,
-    rw ← set.image_prod,
-    exact subset_trans (set.image_subset (λ (p : α × β), m p.fst p.snd) hsub') hsub },
-  { intro hmem,
-    rw mem_map₂_iff at hmem,
-    obtain ⟨t, t', ht, ht', hsub⟩ := hmem,
-    rw ← set.image_prod at hsub,
-    rw filter.mem_map_iff_exists_image,
-    exact ⟨t ×ˢ t', filter.prod_mem_prod ht ht', hsub⟩ },
+  simp [mem_prod_iff, prod_subset_iff]
 end
 
 lemma map_prod_eq_map₂' (m : α × β → γ) (f : filter α) (g : filter β) :
   filter.map m (f ×ᶠ g) = map₂ (λ a b, m (a, b)) f g :=
-by { refine eq.trans _ (map_prod_eq_map₂ (curry m) f g), ext, simp }
+(congr_arg2 _ (uncurry_curry m).symm rfl).trans (map_prod_eq_map₂ _ _ _)
 
 @[simp] lemma map₂_mk_eq_prod (f : filter α) (g : filter β) : map₂ prod.mk f g = f ×ᶠ g :=
-by ext; simp [mem_prod_iff]
+by simp only [← map_prod_eq_map₂, prod.mk.eta, map_id']
 
 -- lemma image2_mem_map₂_iff (hm : injective2 m) : image2 m s t ∈ map₂ m f g ↔ s ∈ f ∧ t ∈ g :=
 -- ⟨by { rintro ⟨u, v, hu, hv, h⟩, rw image2_subset_image2_iff hm at h,
@@ -230,19 +216,13 @@ begin
 end
 
 lemma map_map₂ (m : α → β → γ) (n : γ → δ) : (map₂ m f g).map n = map₂ (λ a b, n (m a b)) f g :=
-filter.ext $ λ u, exists₂_congr $ λ s t, by rw [←image_subset_iff, image_image2]
+by rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, map_map]
 
 lemma map₂_map_left (m : γ → β → δ) (n : α → γ) :
   map₂ m (f.map n) g = map₂ (λ a b, m (n a) b) f g :=
 begin
-  ext u,
-  split,
-  { rintro ⟨s, t, hs, ht, hu⟩,
-    refine ⟨_, t, hs, ht, _⟩,
-    rw ←image2_image_left,
-    exact (image2_subset_right $ image_preimage_subset _ _).trans hu },
-  { rintro ⟨s, t, hs, ht, hu⟩,
-    exact ⟨_, t, image_mem_map hs, ht, by rwa image2_image_left⟩ }
+  rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, ← @map_id _ g, prod_map_map_eq, map_map, map_id],
+  refl
 end
 
 lemma map₂_map_right (m : α → γ → δ) (n : β → γ) :
@@ -251,10 +231,11 @@ by rw [map₂_swap, map₂_map_left, map₂_swap]
 
 @[simp] lemma map₂_curry (m : α × β → γ) (f : filter α) (g : filter β) :
   map₂ (curry m) f g = (f ×ᶠ g).map m :=
-by { classical, rw [←map₂_mk_eq_prod, map_map₂, curry] }
+(map_prod_eq_map₂' _  _ _).symm
 
 @[simp] lemma map_uncurry_prod (m : α → β → γ) (f : filter α) (g : filter β) :
-  (f ×ᶠ g).map (uncurry m) = map₂ m f g := by rw [←map₂_curry, curry_uncurry]
+  (f ×ᶠ g).map (uncurry m) = map₂ m f g :=
+by rw [←map₂_curry, curry_uncurry]
 
 /-!
 ### Algebraic replacement rules

src/topology/algebra/group/basic.lean

@@ -670,24 +670,17 @@ lemma topological_group.ext_iff {G : Type*} [group G] {t t' : topological_space
 ⟨λ h, h ▸ rfl, tg.ext tg'⟩
 
 @[to_additive]
-lemma topological_group.of_nhds_aux {G : Type*} [group G] [topological_space G]
+lemma has_continuous_inv.of_nhds_one {G : Type*} [group G] [topological_space G]
   (hinv : tendsto (λ (x : G), x⁻¹) (𝓝 1) (𝓝 1))
   (hleft : ∀ (x₀ : G), 𝓝 x₀ = map (λ (x : G), x₀ * x) (𝓝 1))
-  (hconj : ∀ (x₀ : G), map (λ (x : G), x₀ * x * x₀⁻¹) (𝓝 1) ≤ 𝓝 1) : continuous (λ x : G, x⁻¹) :=
+  (hconj : ∀ (x₀ : G), tendsto (λ (x : G), x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)) :
+  has_continuous_inv G :=
 begin
-  rw continuous_iff_continuous_at,
-  rintros x₀,
-  have key : (λ x, (x₀*x)⁻¹) = (λ x, x₀⁻¹*x) ∘ (λ x, x₀*x*x₀⁻¹) ∘ (λ x, x⁻¹),
-    by {ext ; simp[mul_assoc] },
-  calc map (λ x, x⁻¹) (𝓝 x₀)
-      = map (λ x, x⁻¹) (map (λ x, x₀*x) $ 𝓝 1) : by rw hleft
-  ... = map (λ x, (x₀*x)⁻¹) (𝓝 1) : by rw filter.map_map
-  ... = map (((λ x, x₀⁻¹*x) ∘ (λ x, x₀*x*x₀⁻¹)) ∘ (λ x, x⁻¹)) (𝓝 1) : by rw key
-  ... = map ((λ x, x₀⁻¹*x) ∘ (λ x, x₀*x*x₀⁻¹)) _ : by rw ← filter.map_map
-  ... ≤ map ((λ x, x₀⁻¹ * x) ∘ λ x, x₀ * x * x₀⁻¹) (𝓝 1) : map_mono hinv
-  ... = map (λ x, x₀⁻¹ * x) (map (λ x, x₀ * x * x₀⁻¹) (𝓝 1)) : filter.map_map
-  ... ≤ map (λ x, x₀⁻¹ * x) (𝓝 1) : map_mono (hconj x₀)
-  ... = 𝓝 x₀⁻¹ : (hleft _).symm
+  refine ⟨continuous_iff_continuous_at.2 $ λ x₀, _⟩,
+  have : tendsto (λ x, x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map ((*) x₀⁻¹) (𝓝 1)),
+    from (tendsto_map.comp $ hconj x₀).comp hinv,
+  simpa only [continuous_at, hleft x₀, hleft x₀⁻¹, tendsto_map'_iff, (∘), mul_assoc,
+    mul_inv_rev, inv_mul_cancel_left] using this
 end
 
 @[to_additive]
@@ -696,47 +689,28 @@ lemma topological_group.of_nhds_one' {G : Type u} [group G] [topological_space G
   (hinv : tendsto (λ x : G, x⁻¹) (𝓝 1) (𝓝 1))
   (hleft : ∀ x₀ : G, 𝓝 x₀ = map (λ x, x₀*x) (𝓝 1))
   (hright : ∀ x₀ : G, 𝓝 x₀ = map (λ x, x*x₀) (𝓝 1)) : topological_group G :=
-begin
-  refine { continuous_mul := (has_continuous_mul.of_nhds_one hmul hleft hright).continuous_mul,
-           continuous_inv := topological_group.of_nhds_aux hinv hleft _ },
-  intros x₀,
-  suffices : map (λ (x : G), x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1, by simp [this, le_refl],
-  rw [show (λ x, x₀ * x * x₀⁻¹) = (λ x, x₀ * x) ∘ λ x, x*x₀⁻¹, by {ext, simp [mul_assoc] },
-      ← filter.map_map, ← hright, hleft x₀⁻¹, filter.map_map],
-  convert map_id,
-  ext,
-  simp
-end
+{ to_has_continuous_mul := has_continuous_mul.of_nhds_one hmul hleft hright,
+  to_has_continuous_inv := has_continuous_inv.of_nhds_one hinv hleft $ λ x₀, le_of_eq
+    begin
+      rw [show (λ x, x₀ * x * x₀⁻¹) = (λ x, x * x₀⁻¹) ∘ (λ x, x₀ * x), from rfl, ← map_map,
+        ← hleft, hright, map_map],
+      simp [(∘)]
+    end }
 
 @[to_additive]
 lemma topological_group.of_nhds_one {G : Type u} [group G] [topological_space G]
   (hmul : tendsto (uncurry ((*) : G → G → G)) ((𝓝 1) ×ᶠ 𝓝 1) (𝓝 1))
   (hinv : tendsto (λ x : G, x⁻¹) (𝓝 1) (𝓝 1))
   (hleft : ∀ x₀ : G, 𝓝 x₀ = map (λ x, x₀*x) (𝓝 1))
   (hconj : ∀ x₀ : G, tendsto (λ x, x₀*x*x₀⁻¹) (𝓝 1) (𝓝 1)) : topological_group G :=
- { continuous_mul := begin
-    rw continuous_iff_continuous_at,
-    rintros ⟨x₀, y₀⟩,
-    have key : (λ (p : G × G), x₀ * p.1 * (y₀ * p.2)) =
-      ((λ x, x₀*y₀*x) ∘ (uncurry (*)) ∘ (prod.map (λ x, y₀⁻¹*x*y₀) id)),
-      by { ext, simp [uncurry, prod.map, mul_assoc] },
-    specialize hconj y₀⁻¹, rw inv_inv at hconj,
-    calc map (λ (p : G × G), p.1 * p.2) (𝓝 (x₀, y₀))
-        = map (λ (p : G × G), p.1 * p.2) ((𝓝 x₀) ×ᶠ 𝓝 y₀)
-            : by rw nhds_prod_eq
-    ... = map (λ (p : G × G), x₀ * p.1 * (y₀ * p.2)) ((𝓝 1) ×ᶠ (𝓝 1))
-            : by rw [hleft x₀, hleft y₀, prod_map_map_eq, filter.map_map]
-    ... = map (((λ x, x₀*y₀*x) ∘ (uncurry (*))) ∘ (prod.map (λ x, y₀⁻¹*x*y₀) id))((𝓝 1) ×ᶠ (𝓝 1))
-            : by rw key
-    ... = map ((λ x, x₀*y₀*x) ∘ (uncurry (*))) ((map  (λ x, y₀⁻¹*x*y₀) $ 𝓝 1) ×ᶠ (𝓝 1))
-            : by rw [← filter.map_map, ← prod_map_map_eq', map_id]
-    ... ≤ map ((λ x, x₀*y₀*x) ∘ (uncurry (*))) ((𝓝 1) ×ᶠ (𝓝 1))
-            : map_mono (filter.prod_mono hconj $ le_rfl)
-    ... = map (λ x, x₀*y₀*x) (map (uncurry (*)) ((𝓝 1) ×ᶠ (𝓝 1)))   : by rw filter.map_map
-    ... ≤ map (λ x, x₀*y₀*x) (𝓝 1)   : map_mono hmul
-    ... = 𝓝 (x₀*y₀)   : (hleft _).symm
-  end,
-  continuous_inv := topological_group.of_nhds_aux hinv hleft hconj}
+begin
+  refine topological_group.of_nhds_one' hmul hinv hleft (λ x₀, _),
+  replace hconj : ∀ x₀ : G, map (λ x, x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1,
+    from λ x₀, map_eq_of_inverse (λ x, x₀⁻¹ * x * x₀⁻¹⁻¹) (by { ext, simp [mul_assoc] })
+      (hconj _) (hconj _),
+  rw [← hconj x₀],
+  simpa [(∘)] using hleft _
+end
 
 @[to_additive]
 lemma topological_group.of_comm_of_nhds_one {G : Type u} [comm_group G] [topological_space G]