refactor(order/filter): make `filter.has_mem semireducible (#4807)

This way `simp only []` does not simplify `s ∈ f` to `s ∈ f.sets`.

* Add protected simp lemmas `filter.mem_mk` and `filter.mem_sets`.
* Use implicit argument in `filter.mem_generate_iff`.
* Use `∃ t, s ∈ ...` instead of `s ∈ ⋃ t, ...` in
  `filter.mem_infi_finite` and `filter.mem_infi_finite'`.
* Use an implicit argument in `(non/ne_)empty_of_mem_ultrafilter`.

Author: urkud

src/analysis/calculus/fderiv.lean

@@ -2165,7 +2165,7 @@ lemma fderiv_const_mul (hc : differentiable_at 𝕜 c x) (d : 𝕜) :
 end mul
 
 section algebra_inverse
-variables {R :Type*} [normed_ring R] [normed_algebra 𝕜 R] [complete_space R]
+variables {R : Type*} [normed_ring R] [normed_algebra 𝕜 R] [complete_space R]
 open normed_ring continuous_linear_map ring
 
 /-- At an invertible element `x` of a normed algebra `R`, the Fréchet derivative of the inversion

src/data/analysis/topology.lean

@@ -107,11 +107,9 @@ is_open_iff_nhds.2 $ λ a m, by simpa using F.mem_nhds.2 ⟨s, m, subset.refl _
 theorem ext' [T : topological_space α] {σ : Type*} {F : ctop α σ}
   (H : ∀ a s, s ∈ 𝓝 a ↔ ∃ b, a ∈ F b ∧ F b ⊆ s) :
   F.to_topsp = T :=
-topological_space_eq $ funext $ λ s, begin
-  have : ∀ T s, @topological_space.is_open _ T s ↔ _ := @is_open_iff_mem_nhds α,
-  rw [this, this],
-  apply congr_arg (λ f : α → filter α, ∀ a ∈ s, s ∈ f a),
-  funext a, apply filter_eq, apply set.ext, intro x,
+begin
+  refine eq_of_nhds_eq_nhds (λ x, _),
+  ext s,
   rw [mem_nhds_to_topsp, H]
 end
 

src/order/filter/basic.lean

@@ -95,12 +95,15 @@ structure filter (α : Type*) :=
 (inter_sets {x y}       : x ∈ sets → y ∈ sets → x ∩ y ∈ sets)
 
 /-- If `F` is a filter on `α`, and `U` a subset of `α` then we can write `U ∈ F` as on paper. -/
-@[reducible]
 instance {α : Type*}: has_mem (set α) (filter α) := ⟨λ U F, U ∈ F.sets⟩
 
 namespace filter
 variables {α : Type u} {f g : filter α} {s t : set α}
 
+@[simp] protected lemma mem_mk {t : set (set α)} {h₁ h₂ h₃} : s ∈ mk t h₁ h₂ h₃ ↔ s ∈ t := iff.rfl
+
+@[simp] protected lemma mem_sets : s ∈ f.sets ↔ s ∈ f := iff.rfl
+
 instance inhabited_mem : inhabited {s : set α // s ∈ f} := ⟨⟨univ, f.univ_sets⟩⟩
 
 lemma filter_eq : ∀{f g : filter α}, f.sets = g.sets → f = g
@@ -110,7 +113,7 @@ lemma filter_eq_iff : f = g ↔ f.sets = g.sets :=
 ⟨congr_arg _, filter_eq⟩
 
 protected lemma ext_iff : f = g ↔ ∀ s, s ∈ f ↔ s ∈ g :=
-by rw [filter_eq_iff, ext_iff]
+by simp only [filter_eq_iff, ext_iff, filter.mem_sets]
 
 @[ext]
 protected lemma ext : (∀ s, s ∈ f ↔ s ∈ g) → f = g :=
@@ -218,7 +221,7 @@ section join
 /-- The join of a filter of filters is defined by the relation `s ∈ join f ↔ {t | s ∈ t} ∈ f`. -/
 def join (f : filter (filter α)) : filter α :=
 { sets             := {s | {t : filter α | s ∈ t} ∈ f},
-  univ_sets        := by simp only [univ_mem_sets, mem_set_of_eq]; exact univ_mem_sets,
+  univ_sets        := by simp only [mem_set_of_eq, univ_sets, ← filter.mem_sets, set_of_true],
   sets_of_superset := assume x y hx xy,
     mem_sets_of_superset hx $ assume f h, mem_sets_of_superset h xy,
   inter_sets       := assume x y hx hy,
@@ -260,7 +263,8 @@ iff.intro
     (assume x y _ hxy hx, mem_sets_of_superset hx hxy)
     (assume x y _ _ hx hy, inter_mem_sets hx hy))
 
-lemma mem_generate_iff (s : set $ set α) {U : set α} : U ∈ generate s ↔ ∃ t ⊆ s, finite t ∧ ⋂₀ t ⊆ U :=
+lemma mem_generate_iff {s : set $ set α} {U : set α} :
+  U ∈ generate s ↔ ∃ t ⊆ s, finite t ∧ ⋂₀ t ⊆ U :=
 begin
   split ; intro h,
   { induction h with V V_in V W V_in hVW hV V W V_in W_in hV hW,
@@ -295,8 +299,9 @@ end
 protected def mk_of_closure (s : set (set α)) (hs : (generate s).sets = s) : filter α :=
 { sets             := s,
   univ_sets        := hs ▸ (univ_mem_sets : univ ∈ generate s),
-  sets_of_superset := assume x y, hs ▸ (mem_sets_of_superset : x ∈ generate s → x ⊆ y → y ∈ generate s),
-  inter_sets       := assume x y, hs ▸ (inter_mem_sets : x ∈ generate s → y ∈ generate s → x ∩ y ∈ generate s) }
+  sets_of_superset := λ x y, hs ▸ (mem_sets_of_superset : x ∈ generate s → x ⊆ y → y ∈ generate s),
+  inter_sets       := λ x y, hs ▸ (inter_mem_sets : x ∈ generate s → y ∈ generate s →
+                        x ∩ y ∈ generate s) }
 
 lemma mk_of_closure_sets {s : set (set α)} {hs : (generate s).sets = s} :
   filter.mk_of_closure s hs = generate s :=
@@ -438,7 +443,7 @@ iff.rfl
 
 @[simp] lemma mem_supr_sets {x : set α} {f : ι → filter α} :
   x ∈ supr f ↔ (∀i, x ∈ f i) :=
-by simp only [supr_sets_eq, iff_self, mem_Inter]
+by simp only [← filter.mem_sets, supr_sets_eq, iff_self, mem_Inter]
 
 lemma infi_eq_generate (s : ι → filter α) : infi s = generate (⋃ i, (s i).sets) :=
 show generate _ = generate _, from congr_arg _ supr_range
@@ -590,25 +595,24 @@ let ⟨i⟩ := ne, u := { filter .
       rcases h a b with ⟨c, ha, hb⟩,
       exact ⟨c, inter_mem_sets (ha hx) (hb hy)⟩
     end } in
-have u = infi f, from eq_infi_of_mem_sets_iff_exists_mem (λ s, by simp only [mem_Union]),
+have u = infi f, from eq_infi_of_mem_sets_iff_exists_mem
+  (λ s, by simp only [filter.mem_mk, mem_Union, filter.mem_sets]),
 congr_arg filter.sets this.symm
 
 lemma mem_infi {f : ι → filter α} (h : directed (≥) f) [nonempty ι] (s) :
   s ∈ infi f ↔ ∃ i, s ∈ f i :=
-by simp only [infi_sets_eq h, mem_Union]
-
-lemma binfi_sets_eq {f : β → filter α} {s : set β}
-  (h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) :
-  (⨅ i∈s, f i).sets = (⋃ i ∈ s, (f i).sets) :=
-by haveI := ne.to_subtype;
-calc (⨅ i ∈ s, f i).sets  = (⨅ t : {t // t ∈ s}, (f t.val)).sets : by rw [infi_subtype]; refl
-  ... = (⨆ t : {t // t ∈ s}, (f t.val).sets) : infi_sets_eq h.directed_coe
-  ... = (⨆ t ∈ s, (f t).sets) : by rw [supr_subtype]; refl
+by simp only [← filter.mem_sets, infi_sets_eq h, mem_Union]
 
 lemma mem_binfi {f : β → filter α} {s : set β}
   (h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) {t : set α} :
   t ∈ (⨅ i∈s, f i) ↔ ∃ i ∈ s, t ∈ f i :=
-by simp only [binfi_sets_eq h ne, mem_bUnion_iff]
+by haveI : nonempty {x // x  ∈ s} := ne.to_subtype;
+  erw [infi_subtype', mem_infi h.directed_coe, subtype.exists]; refl
+
+lemma binfi_sets_eq {f : β → filter α} {s : set β}
+  (h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) :
+  (⨅ i∈s, f i).sets = (⋃ i ∈ s, (f i).sets) :=
+ext $ λ t, by simp [mem_binfi h ne]
 
 lemma infi_sets_eq_finite {ι : Type*} (f : ι → filter α) :
   (⨅i, f i).sets = (⋃t:finset ι, (⨅i∈t, f i).sets) :=
@@ -622,21 +626,19 @@ lemma infi_sets_eq_finite' (f : ι → filter α) :
 by rw [← infi_sets_eq_finite, ← equiv.plift.surjective.infi_comp]; refl
 
 lemma mem_infi_finite {ι : Type*} {f : ι → filter α} (s) :
-  s ∈ infi f ↔ s ∈ ⋃t:finset ι, (⨅i∈t, f i).sets :=
-set.ext_iff.1 (infi_sets_eq_finite f) s
+  s ∈ infi f ↔ ∃ t:finset ι, s ∈ ⨅i∈t, f i :=
+(set.ext_iff.1 (infi_sets_eq_finite f) s).trans mem_Union
 
 lemma mem_infi_finite' {f : ι → filter α} (s) :
-  s ∈ infi f ↔ s ∈ ⋃t:finset (plift ι), (⨅i∈t, f (plift.down i)).sets :=
-set.ext_iff.1 (infi_sets_eq_finite' f) s
+  s ∈ infi f ↔ ∃ t:finset (plift ι), s ∈ ⨅i∈t, f (plift.down i) :=
+(set.ext_iff.1 (infi_sets_eq_finite' f) s).trans mem_Union
 
 @[simp] lemma sup_join {f₁ f₂ : filter (filter α)} : (join f₁ ⊔ join f₂) = join (f₁ ⊔ f₂) :=
-filter_eq $ set.ext $ assume x,
-  by simp only [supr_sets_eq, join, mem_sup_sets, iff_self, mem_set_of_eq]
+filter.ext $ λ x, by simp only [mem_sup_sets, mem_join_sets]
 
 @[simp] lemma supr_join {ι : Sort w} {f : ι → filter (filter α)} :
   (⨆x, join (f x)) = join (⨆x, f x) :=
-filter_eq $ set.ext $ assume x,
-  by simp only [supr_sets_eq, join, iff_self, mem_Inter, mem_set_of_eq]
+filter.ext $ assume x, by simp only [mem_supr_sets, mem_join_sets]
 
 instance : bounded_distrib_lattice (filter α) :=
 { le_sup_inf :=
@@ -751,7 +753,7 @@ lemma infi_sets_induct {f : ι → filter α} {s : set α} (hs : s ∈ infi f) {
   (upw : ∀{s₁ s₂}, s₁ ⊆ s₂ → p s₁ → p s₂) : p s :=
 begin
   rw [mem_infi_finite'] at hs,
-  simp only [mem_Union, (finset.inf_eq_infi _ _).symm] at hs,
+  simp only [← finset.inf_eq_infi] at hs,
   rcases hs with ⟨is, his⟩,
   revert s,
   refine finset.induction_on is _ _,
@@ -770,12 +772,10 @@ le_antisymm
   (by simp [le_inf_iff, inter_subset_left, inter_subset_right])
 
 @[simp] lemma sup_principal {s t : set α} : 𝓟 s ⊔ 𝓟 t = 𝓟 (s ∪ t) :=
-filter_eq $ set.ext $
-  by simp only [union_subset_iff, union_subset_iff, mem_sup_sets, forall_const, iff_self, mem_principal_sets]
+filter.ext $ λ u, by simp only [union_subset_iff, mem_sup_sets, mem_principal_sets]
 
 @[simp] lemma supr_principal {ι : Sort w} {s : ι → set α} : (⨆x, 𝓟 (s x)) = 𝓟 (⋃i, s i) :=
-filter_eq $ set.ext $ assume x, by simp only [supr_sets_eq, mem_principal_sets, mem_Inter];
-exact (@supr_le_iff (set α) _ _ _ _).symm
+filter.ext $ assume x, by simp only [mem_supr_sets, mem_principal_sets, Union_subset_iff]
 
 @[simp] lemma principal_eq_bot_iff {s : set α} : 𝓟 s = ⊥ ↔ s = ∅ :=
 empty_in_sets_eq_bot.symm.trans $ mem_principal_sets.trans subset_empty_iff
@@ -1722,13 +1722,13 @@ lemma ne_bot.map (hf : ne_bot f) (m : α → β) : ne_bot (map m f) :=
 instance map_ne_bot [hf : ne_bot f] : ne_bot (f.map m) := hf.map m
 
 lemma sInter_comap_sets (f : α → β) (F : filter β) :
-  ⋂₀(comap f F).sets = ⋂ U ∈ F, f ⁻¹' U :=
+  ⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U :=
 begin
   ext x,
   suffices : (∀ (A : set α) (B : set β), B ∈ F → f ⁻¹' B ⊆ A → x ∈ A) ↔
     ∀ (B : set β), B ∈ F → f x ∈ B,
-  by simp only [mem_sInter, mem_Inter, mem_comap_sets, this, and_imp, mem_comap_sets, exists_prop, mem_sInter,
-    iff_self, mem_Inter, mem_preimage, exists_imp_distrib],
+  by simp only [mem_sInter, mem_Inter, filter.mem_sets, mem_comap_sets, this, and_imp,
+    mem_comap_sets, exists_prop, mem_sInter, mem_Inter, mem_preimage, exists_imp_distrib],
   split,
   { intros h U U_in,
     simpa only [set.subset.refl, forall_prop_of_true, mem_preimage] using h (f ⁻¹' U) U U_in },
@@ -1748,7 +1748,7 @@ le_antisymm
   map_infi_le
   (assume s (hs : preimage m s ∈ infi f),
     have ∃i, preimage m s ∈ f i,
-      by simp only [infi_sets_eq hf, mem_Union] at hs; assumption,
+      by simp only [mem_infi hf, mem_Union] at hs; assumption,
     let ⟨i, hi⟩ := this in
     have (⨅ i, map m (f i)) ≤ 𝓟 s, from
       infi_le_of_le i $ by simp only [le_principal_iff, mem_map]; assumption,
@@ -1770,7 +1770,7 @@ lemma map_inf' {f g : filter α} {m : α → β} {t : set α} (htf : t ∈ f) (h
   (h : ∀x∈t, ∀y∈t, m x = m y → x = y) : map m (f ⊓ g) = map m f ⊓ map m g :=
 begin
   refine le_antisymm map_inf_le (assume s hs, _),
-  simp only [map, mem_inf_sets, exists_prop, mem_map, mem_preimage, mem_inf_sets] at hs ⊢,
+  simp only [mem_inf_sets, exists_prop, mem_map, mem_preimage, mem_inf_sets] at hs ⊢,
   rcases hs with ⟨t₁, h₁, t₂, h₂, hs⟩,
   refine ⟨m '' (t₁ ∩ t), _, m '' (t₂ ∩ t), _, _⟩,
   { filter_upwards [h₁, htf] assume a h₁ h₂, mem_image_of_mem _ ⟨h₁, h₂⟩ },

src/order/filter/lift.lean

@@ -91,19 +91,16 @@ infi_le_infi $ assume s, infi_le_infi $ assume hs, hg s hs
 lemma map_lift_eq {m : β → γ} (hg : monotone g) : map m (f.lift g) = f.lift (map m ∘ g) :=
 have monotone (map m ∘ g),
   from map_mono.comp hg,
-filter_eq $ set.ext $
-  by simp only [mem_lift_sets hg, mem_lift_sets this, exists_prop, forall_const, mem_map, iff_self,
-    function.comp_app]
+filter.ext $ λ s,
+  by simp only [mem_lift_sets hg, mem_lift_sets this, exists_prop, mem_map, function.comp_app]
 
 lemma comap_lift_eq {m : γ → β} (hg : monotone g) : comap m (f.lift g) = f.lift (comap m ∘ g) :=
 have monotone (comap m ∘ g),
   from comap_mono.comp hg,
-filter_eq $ set.ext begin
-  simp only [mem_lift_sets hg, mem_lift_sets this, comap, mem_lift_sets, mem_set_of_eq, exists_prop,
-    function.comp_apply],
-  exact λ s,
-   ⟨λ ⟨b, ⟨a, ha, hb⟩, hs⟩, ⟨a, ha, b, hb, hs⟩,
-    λ ⟨a, ha, b, hb, hs⟩, ⟨b, ⟨a, ha, hb⟩, hs⟩⟩
+begin
+  ext,
+  simp only [mem_lift_sets hg, mem_lift_sets this, mem_comap_sets, exists_prop, mem_lift_sets],
+  exact ⟨λ ⟨b, ⟨a, ha, hb⟩, hs⟩, ⟨a, ha, b, hb, hs⟩, λ ⟨a, ha, b, hb, hs⟩, ⟨b, ⟨a, ha, hb⟩, hs⟩⟩
 end
 
 theorem comap_lift_eq2 {m : β → α} {g : set β → filter γ} (hg : monotone g) :

src/order/filter/partial.lean

@@ -18,7 +18,7 @@ Relations.
 -/
 
 def rmap (r : rel α β) (f : filter α) : filter β :=
-{ sets             := r.core ⁻¹' f.sets,
+{ sets             := {s | r.core s ∈  f},
   univ_sets        := by { simp [rel.core], apply univ_mem_sets },
   sets_of_superset := assume s t hs st, mem_sets_of_superset hs $ rel.core_mono _ st,
   inter_sets       := by { simp [set.preimage, rel.core_inter], exact λ s t, inter_mem_sets } }

src/order/filter/pointwise.lean

@@ -130,8 +130,8 @@ variables [monoid α] [monoid β] {f : filter α} (m : α → β)
 
 @[to_additive]
 protected lemma map_mul [is_mul_hom m] {f₁ f₂ : filter α} : map m (f₁ * f₂) = map m f₁ * map m f₂ :=
-filter_eq $ set.ext $ assume s,
 begin
+  ext s,
   simp only [mem_mul], split,
   { rintro ⟨t₁, t₂, ht₁, ht₂, t₁t₂⟩,
     have : m '' (t₁ * t₂) ⊆ s := subset.trans (image_subset m t₁t₂) (image_preimage_subset _ _),

src/order/filter/ultrafilter.lean

@@ -69,15 +69,11 @@ begin
   { intros h s, conv_rhs {rw (show s = sᶜᶜ, by simp)}, exact h _, }
 end
 
-lemma ne_empty_of_mem_ultrafilter (s : set α) : is_ultrafilter f → s ∈ f → s ≠ ∅ :=
-begin
-  rintros h hs rfl,
-  replace h := ((ultrafilter_iff_compl_mem_iff_not_mem'.mp h) ∅).mp hs,
-  finish [f.univ_sets],
-end
+lemma nonempty_of_mem_ultrafilter {s : set α} (hf : is_ultrafilter f) (hs : s ∈ f) : s.nonempty :=
+hf.1.nonempty_of_mem hs
 
-lemma nonempty_of_mem_ultrafilter (s : set α) : is_ultrafilter f → s ∈ f → s.nonempty :=
-λ hf hs, ne_empty_iff_nonempty.mp (ne_empty_of_mem_ultrafilter _ hf hs)
+lemma ne_empty_of_mem_ultrafilter {s : set α} (hf : is_ultrafilter f) (hs : s ∈ f) : s ≠ ∅ :=
+(nonempty_of_mem_ultrafilter hf hs).ne_empty
 
 lemma mem_or_compl_mem_of_ultrafilter (hf : is_ultrafilter f) (s : set α) :
   s ∈ f ∨ sᶜ ∈ f :=
@@ -126,17 +122,13 @@ lemma ultrafilter_map {f : filter α} {m : α → β} (h : is_ultrafilter f) :
 by rw ultrafilter_iff_compl_mem_iff_not_mem at ⊢ h; exact assume s, h (m ⁻¹' s)
 
 lemma ultrafilter_pure {a : α} : is_ultrafilter (pure a) :=
-begin
-  rw ultrafilter_iff_compl_mem_iff_not_mem, intro s,
-  rw [mem_pure_sets, mem_pure_sets], exact iff.rfl
-end
+by simp [ultrafilter_iff_compl_mem_iff_not_mem]
 
 lemma ultrafilter_bind {f : filter α} (hf : is_ultrafilter f) {m : α → filter β}
   (hm : ∀ a, is_ultrafilter (m a)) : is_ultrafilter (f.bind m) :=
 begin
   simp only [ultrafilter_iff_compl_mem_iff_not_mem] at ⊢ hf hm, intro s,
-  dsimp [bind, join, map, preimage],
-  simp only [hm], apply hf
+  simp only [mem_bind_sets', hm, ← compl_set_of, hf]
 end
 
 /-- The ultrafilter lemma: Any proper filter is contained in an ultrafilter. -/
@@ -175,7 +167,7 @@ begin
   refine ⟨_, λ T hT, filter.generate_sets.basic hT⟩,
   rw ← forall_sets_nonempty_iff_ne_bot,
   intros T hT,
-  rcases (mem_generate_iff _).mp hT with ⟨A, h1, h2, h3⟩,
+  rcases mem_generate_iff.mp hT with ⟨A, h1, h2, h3⟩,
   let B := set.finite.to_finset h2,
   rw (show A = ↑B, by simp) at *,
   rcases cond B h1 with ⟨x, hx⟩,
@@ -224,7 +216,7 @@ begin
     simpa [subset_def, and_comm] using this },
   resetI,
   rcases exists_ultrafilter f' with ⟨g', g'f', u'⟩,
-  simp only [supr_sets_eq, mem_Inter] at hs,
+  simp only [mem_supr_sets, mem_Inter] at hs,
   have := hs (g'.map coe) (ultrafilter_map u') (map_le_iff_le_comap.mpr g'f'),
   rw [←le_principal_iff, map_le_iff_le_comap, comap_principal, j_inv_s, principal_empty,
     le_bot_iff] at this,

src/topology/category/Compactum.lean

@@ -204,14 +204,14 @@ begin
   -- All sets in C0 are nonempty.
   have claim2 : ∀ B ∈ C0, set.nonempty B,
   { rintros B ⟨Q,hQ,rfl⟩,
-    obtain ⟨q⟩ := nonempty_of_mem_ultrafilter _ F.2 hQ,
+    obtain ⟨q⟩ := nonempty_of_mem_ultrafilter F.2 hQ,
     use X.incl q,
     simpa, },
   -- The intersection of AA with every set in C0 is nonempty.
   have claim3 : ∀ B ∈ C0, (AA ∩ B).nonempty,
   { rintros B ⟨Q,hQ,rfl⟩,
     have : (Q ∩ cl A).nonempty,
-    { apply nonempty_of_mem_ultrafilter _ F.2,
+    { apply nonempty_of_mem_ultrafilter F.2,
       exact F.1.inter_sets hQ hF },
     rcases this with ⟨q,hq1,P,hq2,hq3⟩,
     refine ⟨P,hq2,_⟩,

src/topology/metric_space/gluing.lean

@@ -53,6 +53,7 @@ universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
 open function set premetric
+open_locale uniformity
 
 namespace metric
 section approx_gluing
@@ -285,7 +286,7 @@ lemma sum.one_dist_le' {x : α} {y : β} : 1 ≤ sum.dist (inr y) (inl x) :=
 by rw sum.dist_comm; exact sum.one_dist_le
 
 private lemma sum.mem_uniformity (s : set ((α ⊕ β) × (α ⊕ β))) :
-  s ∈ (@uniformity (α ⊕ β) _).sets ↔ ∃ ε > 0, ∀ a b, sum.dist a b < ε → (a, b) ∈ s :=
+  s ∈ 𝓤 (α ⊕ β) ↔ ∃ ε > 0, ∀ a b, sum.dist a b < ε → (a, b) ∈ s :=
 begin
   split,
   { rintro ⟨hsα, hsβ⟩,
@@ -298,13 +299,13 @@ begin
     { cases not_le_of_lt (lt_of_lt_of_le h (min_le_right _ _)) sum.one_dist_le' },
     { exact hβ (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_right _ _))) } },
   { rintro ⟨ε, ε0, H⟩,
-    split; rw [filter.mem_map, mem_uniformity_dist];
+    split; rw [filter.mem_sets, filter.mem_map, mem_uniformity_dist];
       exact ⟨ε, ε0, λ x y h, H _ _ (by exact h)⟩ }
 end
 
-/-- The distance on the disjoint union indeed defines a metric space. All the distance properties follow from our
-choice of the distance. The harder work is to show that the uniform structure defined by the distance coincides
-with the disjoint union uniform structure. -/
+/-- The distance on the disjoint union indeed defines a metric space. All the distance properties
+follow from our choice of the distance. The harder work is to show that the uniform structure
+defined by the distance coincides with the disjoint union uniform structure. -/
 def metric_space_sum : metric_space (α ⊕ β) :=
 { dist               := sum.dist,
   dist_self          := λx, by cases x; simp only [sum.dist, dist_self],

src/topology/order.lean

@@ -533,7 +533,7 @@ end
 
 theorem nhds_induced [T : topological_space α] (f : β → α) (a : β) :
   @nhds β (topological_space.induced f T) a = comap f (𝓝 (f a)) :=
-filter_eq $ by ext s; rw mem_nhds_induced; rw mem_comap_sets
+by { ext s, rw [mem_nhds_induced, mem_comap_sets] }
 
 lemma induced_iff_nhds_eq [tα : topological_space α] [tβ : topological_space β] (f : β → α) :
 tβ = tα.induced f ↔ ∀ b, 𝓝 b = comap f (𝓝 $ f b) :=