refactor(topology): topological_space.induced resembles set.image; second_countable_topology on subtypes; simplify filter.map_comap

Author: johoelzl

src/order/filter.lean

@@ -756,15 +756,10 @@ le_antisymm
       union_subset hs₁ hs₂⟩)
   (sup_le (comap_mono le_sup_left) (comap_mono le_sup_right))
 
-lemma le_map_comap' {f : filter β} {m : α → β} {s : set β}
-  (hs : s ∈ f.sets) (hm : ∀b∈s, ∃a, m a = b) : f ≤ map m (comap m f) :=
-assume t' ⟨t, ht, (sub : m ⁻¹' t ⊆ m ⁻¹' t')⟩,
-by filter_upwards [ht, hs] assume x hxt hxs,
-  let ⟨y, hy⟩ := hm x hxs in
-  hy ▸ sub (show m y ∈ t, from hy.symm ▸ hxt)
-
-lemma le_map_comap {f : filter β} {m : α → β} (hm : ∀x, ∃y, m y = x) : f ≤ map m (comap m f) :=
-le_map_comap' univ_mem_sets (assume b _, hm b)
+lemma map_comap {f : filter β} {m : α → β} (hf : range m ∈ f.sets) : (f.comap m).map m = f :=
+le_antisymm
+  map_comap_le
+  (assume t' ⟨t, ht, sub⟩, by filter_upwards [ht, hf]; rintros x hxt ⟨y, rfl⟩; exact sub hxt)
 
 lemma comap_map {f : filter α} {m : α → β} (h : ∀ x y, m x = m y → x = y) :
   comap m (map m f) = f :=
@@ -1160,12 +1155,9 @@ lemma tendsto_comap_iff {f : α → β} {g : β → γ} {a : filter α} {c : fil
   tendsto f a (c.comap g) ↔ tendsto (g ∘ f) a c :=
 ⟨assume h, h.comp tendsto_comap, assume h, map_le_iff_le_comap.mp $ by rwa [map_map]⟩
 
-lemma tendsto_comap'' {m : α → β} {f : filter α} {g : filter β} (s : set α)
-  {i : γ → α} (hs : s ∈ f.sets) (hi : ∀a∈s, ∃c, i c = a)
-  (h : tendsto (m ∘ i) (comap i f) g) : tendsto m f g :=
-have tendsto m (map i $ comap i $ f) g,
-  by rwa [tendsto, ←map_compose] at h,
-le_trans (map_mono $ le_map_comap' hs hi) this
+lemma tendsto_comap'_iff {m : α → β} {f : filter α} {g : filter β} {i : γ → α}
+  (h : range i ∈ f.sets) : tendsto (m ∘ i) (comap i f) g ↔ tendsto m f g :=
+by rw [tendsto, ← map_compose]; simp only [(∘), map_comap h, tendsto]
 
 lemma comap_eq_of_inverse {f : filter α} {g : filter β} {φ : α → β} (ψ : β → α)
   (eq : ψ ∘ φ = id) (hφ : tendsto φ f g) (hψ : tendsto ψ g f) : comap φ g = f :=

src/topology/basic.lean

@@ -1314,27 +1314,28 @@ variables {α : Type*} {β : Type*} {γ : Type*}
   makes `f` continuous. -/
 def topological_space.induced {α : Type u} {β : Type v} (f : α → β) (t : topological_space β) :
   topological_space α :=
-{ is_open        := λs, ∃s', t.is_open s' ∧ s = f ⁻¹' s',
-  is_open_univ   := ⟨univ, t.is_open_univ, preimage_univ.symm⟩,
+{ is_open        := λs, ∃s', t.is_open s' ∧ f ⁻¹' s' = s,
+  is_open_univ   := ⟨univ, t.is_open_univ, preimage_univ⟩,
   is_open_inter  := by rintro s₁ s₂ ⟨s'₁, hs₁, rfl⟩ ⟨s'₂, hs₂, rfl⟩;
     exact ⟨s'₁ ∩ s'₂, t.is_open_inter _ _ hs₁ hs₂, preimage_inter⟩,
   is_open_sUnion := assume s h,
   begin
     simp only [classical.skolem] at h,
     cases h with f hf,
     apply exists.intro (⋃(x : set α) (h : x ∈ s), f x h),
-    simp only [sUnion_eq_bUnion, preimage_Union, (λx h, (hf x h).right.symm)], refine ⟨_, rfl⟩,
+    simp only [sUnion_eq_bUnion, preimage_Union, (λx h, (hf x h).right)], refine ⟨_, rfl⟩,
     exact (@is_open_Union β _ t _ $ assume i,
       show is_open (⋃h, f i h), from @is_open_Union β _ t _ $ assume h, (hf i h).left)
   end }
 
 lemma is_open_induced_iff [t : topological_space β] {s : set α} {f : α → β} :
-  @is_open α (t.induced f) s ↔ (∃t, is_open t ∧ s = f ⁻¹' t) :=
+  @is_open α (t.induced f) s ↔ (∃t, is_open t ∧ f ⁻¹' t = s) :=
 iff.refl _
 
 lemma is_closed_induced_iff [t : topological_space β] {s : set α} {f : α → β} :
   @is_closed α (t.induced f) s ↔ (∃t, is_closed t ∧ s = f ⁻¹' t) :=
-⟨assume ⟨t, ht, heq⟩, ⟨-t, is_closed_compl_iff.2 ht, by simp only [preimage_compl, heq.symm, lattice.neg_neg]⟩,
+⟨assume ⟨t, ht, heq⟩, ⟨-t, is_closed_compl_iff.2 ht,
+    by simp only [preimage_compl, heq, lattice.neg_neg]⟩,
   assume ⟨t, ht, heq⟩, ⟨-t, ht, by simp only [preimage_compl, heq.symm]⟩⟩
 
 /-- Given `f : α → β` and a topology on `α`, the coinduced topology on `β` is defined
@@ -1359,7 +1360,7 @@ lemma induced_le_iff_le_coinduced {f : α → β } {tα : topological_space α}
   tβ.induced f ≤ tα ↔ tβ ≤ tα.coinduced f :=
 iff.intro
   (assume h s hs, show tα.is_open (f ⁻¹' s), from h _ ⟨s, hs, rfl⟩)
-  (assume h s ⟨t, ht, hst⟩, hst.symm ▸ h _ ht)
+  (assume h s ⟨t, ht, hst⟩, hst ▸ h _ ht)
 
 lemma gc_induced_coinduced (f : α → β) :
   galois_connection (topological_space.induced f) (topological_space.coinduced f) :=
@@ -1393,12 +1394,12 @@ lemma coinduced_mono (h : t₁ ≤ t₂) : t₁.coinduced f ≤ t₂.coinduced f
 
 lemma induced_id [t : topological_space α] : t.induced id = t :=
 topological_space_eq $ funext $ assume s, propext $
-  ⟨assume ⟨s', hs, h⟩, h.symm ▸ hs, assume hs, ⟨s, hs, rfl⟩⟩
+  ⟨assume ⟨s', hs, h⟩, h ▸ hs, assume hs, ⟨s, hs, rfl⟩⟩
 
 lemma induced_compose [tβ : topological_space β] [tγ : topological_space γ]
   {f : α → β} {g : β → γ} : (tγ.induced g).induced f = tγ.induced (g ∘ f) :=
 topological_space_eq $ funext $ assume s, propext $
-  ⟨assume ⟨s', ⟨s, hs, h₂⟩, h₁⟩, h₁.symm ▸ h₂.symm ▸ ⟨s, hs, rfl⟩,
+  ⟨assume ⟨s', ⟨s, hs, h₂⟩, h₁⟩, h₁ ▸ h₂ ▸ ⟨s, hs, rfl⟩,
     assume ⟨s, hs, h⟩, ⟨preimage g s, ⟨s, hs, rfl⟩, h ▸ rfl⟩⟩
 
 lemma coinduced_id [t : topological_space α] : t.coinduced id = t :=
@@ -1516,6 +1517,13 @@ lemma generate_from_le {t : topological_space α} { g : set (set α) } (h : ∀s
   generate_from g ≤ t :=
 generate_from_le_iff_subset_is_open.2 h
 
+lemma induced_generate_from_eq {α β} {b : set (set β)} {f : α → β} :
+  (generate_from b).induced f = topological_space.generate_from (preimage f '' b) :=
+le_antisymm
+  (induced_le_iff_le_coinduced.2 $ generate_from_le $ assume s hs,
+    generate_open.basic _ $ mem_image_of_mem _ hs)
+  (generate_from_le $ ball_image_iff.2 $ assume s hs, ⟨s, generate_open.basic _ hs, rfl⟩)
+
 protected def topological_space.nhds_adjoint (a : α) (f : filter α) : topological_space α :=
 { is_open        := λs, a ∈ s → s ∈ f.sets,
   is_open_univ   := assume s, univ_mem_sets,
@@ -1570,7 +1578,7 @@ instance Pi.t2_space {β : α → Type v} [t₂ : Πa, topological_space (β a)]
 instance {p : α → Prop} [topological_space α] [discrete_topology α] :
   discrete_topology (subtype p) :=
 ⟨top_unique $ assume s hs,
-  ⟨subtype.val '' s, is_open_discrete _, (set.preimage_image_eq _ subtype.val_injective).symm⟩⟩
+  ⟨subtype.val '' s, is_open_discrete _, (set.preimage_image_eq _ subtype.val_injective)⟩⟩
 
 instance sum.discrete_topology [topological_space α] [topological_space β]
   [hα : discrete_topology α] [hβ : discrete_topology β] : discrete_topology (α ⊕ β) :=
@@ -1696,6 +1704,19 @@ let ⟨b, hb, eq⟩ := second_countable_topology.is_open_generated_countable α
 ⟨assume a, ⟨{s | a ∈ s ∧ s ∈ b},
   countable_subset (assume x ⟨_, hx⟩, hx) hb, by rw [eq, nhds_generate_from]⟩⟩
 
+lemma second_countable_topology_induced (β)
+  [t : topological_space β] [second_countable_topology β] (f : α → β) :
+  @second_countable_topology α (t.induced f) :=
+begin
+  rcases second_countable_topology.is_open_generated_countable β with ⟨b, hb, eq⟩,
+  refine { is_open_generated_countable := ⟨preimage f '' b, countable_image _ hb, _⟩ },
+  rw [eq, induced_generate_from_eq]
+end
+
+instance subtype.second_countable_topology
+  (s : set α) [topological_space α] [second_countable_topology α] : second_countable_topology s :=
+second_countable_topology_induced s α coe
+
 lemma is_open_generated_countable_inter [second_countable_topology α] :
   ∃b:set (set α), countable b ∧ ∅ ∉ b ∧ is_topological_basis b :=
 let ⟨b, hb₁, hb₂⟩ := second_countable_topology.is_open_generated_countable α in

src/topology/continuity.lean

@@ -154,7 +154,7 @@ assume s h, ⟨_, h, rfl⟩
 
 lemma continuous_induced_rng {g : γ → α} {t₂ : tspace β} {t₁ : tspace γ}
   (h : cont t₁ t₂ (f ∘ g)) : cont t₁ (induced f t₂) g :=
-assume s ⟨t, ht, s_eq⟩, s_eq.symm ▸ h t ht
+assume s ⟨t, ht, s_eq⟩, s_eq ▸ h t ht
 
 lemma continuous_coinduced_rng {t : tspace α} : cont t (coinduced f t) f :=
 assume s h, h
@@ -241,39 +241,23 @@ section induced
 open topological_space
 variables [t : topological_space β] {f : α → β}
 
+theorem is_open_induced_eq {s : set α} :
+  @_root_.is_open _ (induced f t) s ↔ s ∈ preimage f '' {s | is_open s} :=
+iff.refl _
+
 theorem is_open_induced {s : set β} (h : is_open s) : (induced f t).is_open (f ⁻¹' s) :=
 ⟨s, h, rfl⟩
 
 lemma nhds_induced_eq_comap {a : α} : @nhds α (induced f t) a = comap f (nhds (f a)) :=
-le_antisymm
-  (assume s ⟨s', hs', (h_s : f ⁻¹' s' ⊆ s)⟩,
-    let ⟨t', hsub, ht', hin⟩ := mem_nhds_sets_iff.1 hs' in
-    (@nhds α (induced f t) a).sets_of_superset
-      begin
-        simp [mem_nhds_sets_iff],
-        exact ⟨preimage f t', preimage_mono hsub, is_open_induced ht', hin⟩
-      end
-      h_s)
-  (le_infi $ assume s, le_infi $ assume ⟨as, s', is_open_s', s_eq⟩,
-    begin
-      simp [comap, mem_nhds_sets_iff, s_eq],
-      exact ⟨s', ⟨s', subset.refl _, is_open_s', by rwa [s_eq] at as⟩, subset.refl _⟩
-    end)
+calc @nhds α (induced f t) a = (⨅ s (x : s ∈ preimage f '' set_of is_open ∧ a ∈ s), principal s) :
+    by simp [nhds, is_open_induced_eq, -mem_image, and_comm]
+  ... = (⨅ s (x : is_open s ∧ f a ∈ s), principal (f ⁻¹' s)) :
+    by simp only [infi_and, infi_image]; refl
+  ... = _ : by simp [nhds, comap_infi, and_comm]
 
-lemma map_nhds_induced_eq {a : α} (h : image f univ ∈ (nhds (f a)).sets) :
+lemma map_nhds_induced_eq {a : α} (h : range f ∈ (nhds (f a)).sets) :
   map f (@nhds α (induced f t) a) = nhds (f a) :=
-le_antisymm
-  (@continuous.tendsto α β (induced f t) _ _ continuous_induced_dom a)
-  (assume s, assume hs : f ⁻¹' s ∈ (@nhds α (induced f t) a).sets,
-    let ⟨t', t_subset, is_open_t, a_in_t⟩ := mem_nhds_sets_iff.mp h in
-    let ⟨s', s'_subset, ⟨s'', is_open_s'', s'_eq⟩, a_in_s'⟩ := (@mem_nhds_sets_iff _ (induced f t) _ _).mp hs in
-    by subst s'_eq; exact (mem_nhds_sets_iff.mpr $
-      ⟨t' ∩ s'',
-        assume x ⟨h₁, h₂⟩, match x, h₂, t_subset h₁ with
-        | x, h₂, ⟨y, _, y_eq⟩ := begin subst y_eq, exact s'_subset h₂ end
-        end,
-        is_open_inter is_open_t is_open_s'',
-        ⟨a_in_t, a_in_s'⟩⟩))
+by rw [nhds_induced_eq_comap, filter.map_comap h]
 
 lemma closure_induced [t : topological_space β] {f : α → β} {a : α} {s : set α}
   (hf : ∀x y, f x = f y → x = y) :
@@ -331,16 +315,16 @@ lemma embedding_open {f : α → β} {s : set α}
   (hf : embedding f) (h : is_open (range f)) (hs : is_open s) : is_open (f '' s) :=
 let ⟨t, ht, h_eq⟩ := by rw [hf.right] at hs; exact hs in
 have is_open (t ∩ range f), from is_open_inter ht h,
-h_eq.symm ▸ by rwa [image_preimage_eq_inter_range]
+h_eq ▸ by rwa [image_preimage_eq_inter_range]
 
 lemma embedding_is_closed {f : α → β} {s : set α}
   (hf : embedding f) (h : is_closed (range f)) (hs : is_closed s) : is_closed (f '' s) :=
 let ⟨t, ht, h_eq⟩ := by rw [hf.right, is_closed_induced_iff] at hs; exact hs in
 have is_closed (t ∩ range f), from is_closed_inter ht h,
 h_eq.symm ▸ by rwa [image_preimage_eq_inter_range]
 
-lemma embedding.map_nhds_eq [topological_space α] [topological_space β] {f : α → β} (hf : embedding f) (a : α)
-  (h : f '' univ ∈ (nhds (f a)).sets) : (nhds a).map f = nhds (f a) :=
+lemma embedding.map_nhds_eq [topological_space α] [topological_space β] {f : α → β}
+  (hf : embedding f) (a : α) (h : range f ∈ (nhds (f a)).sets) : (nhds a).map f = nhds (f a) :=
 by rw [hf.2]; exact map_nhds_induced_eq h
 
 lemma embedding.tendsto_nhds_iff {ι : Type*}
@@ -552,12 +536,8 @@ lemma prod_eq_generate_from [tα : topological_space α] [tβ : topological_spac
   generate_from {g | ∃(s:set α) (t:set β), is_open s ∧ is_open t ∧ g = set.prod s t} :=
 le_antisymm
   (sup_le
-    (assume s ⟨t, ht, s_eq⟩,
-      have set.prod t univ = s, by simp [s_eq, preimage, set.prod],
-      this ▸ (generate_open.basic _ ⟨t, univ, ht, is_open_univ, rfl⟩))
-    (assume s ⟨t, ht, s_eq⟩,
-      have set.prod univ t = s, by simp [s_eq, preimage, set.prod],
-      this ▸ (generate_open.basic _ ⟨univ, t, is_open_univ, ht, rfl⟩)))
+    (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨t, univ, by simpa [set.prod_eq] using ht⟩)
+    (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨univ, t, by simpa [set.prod_eq] using ht⟩))
   (generate_from_le $ assume g ⟨s, t, hs, ht, g_eq⟩, g_eq.symm ▸ is_open_prod hs ht)
 
 lemma is_open_prod_iff {s : set (α×β)} : is_open s ↔
@@ -801,7 +781,7 @@ lemma embedding_inl : embedding (@sum.inl α β) :=
       change
         (is_open (sum.inl ⁻¹' (@sum.inl α β '' u)) ∧
          is_open (sum.inr ⁻¹' (@sum.inl α β '' u))) ∧
-        u = sum.inl ⁻¹' (sum.inl '' u),
+        sum.inl ⁻¹' (sum.inl '' u) = u,
       have : sum.inl ⁻¹' (@sum.inl α β '' u) = u :=
         preimage_image_eq u (λ _ _, sum.inl.inj_iff.mp), rw this,
       have : sum.inr ⁻¹' (@sum.inl α β '' u) = ∅ :=
@@ -819,7 +799,7 @@ lemma embedding_inr : embedding (@sum.inr α β) :=
       change
         (is_open (sum.inl ⁻¹' (@sum.inr α β '' u)) ∧
          is_open (sum.inr ⁻¹' (@sum.inr α β '' u))) ∧
-        u = sum.inr ⁻¹' (sum.inr '' u),
+        sum.inr ⁻¹' (sum.inr '' u) = u,
       have : sum.inl ⁻¹' (@sum.inr α β '' u) = ∅ :=
         eq_empty_iff_forall_not_mem.mpr (assume b ⟨a, _, h⟩, sum.inr_ne_inl h), rw this,
       have : sum.inr ⁻¹' (@sum.inr α β '' u) = u :=
@@ -1007,7 +987,7 @@ lemma pi_eq_generate_from [∀a, topological_space (π a)] :
   generate_from {g | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, is_open (s a)) ∧ g = pi ↑i s} :=
 le_antisymm
   (supr_le $ assume a s ⟨t, ht, s_eq⟩, generate_open.basic _ $
-    ⟨function.update (λa, univ) a t, {a}, by simpa using ht, by ext f; simp [s_eq, pi]⟩)
+    ⟨function.update (λa, univ) a t, {a}, by simpa using ht, by ext f; simp [s_eq.symm, pi]⟩)
   (generate_from_le $ assume g ⟨s, i, hi, eq⟩, eq.symm ▸ is_open_set_pi (finset.finite_to_set _) hi)
 
 lemma pi_generate_from_eq {g : Πa, set (set (π a))} :
@@ -1091,7 +1071,8 @@ lemma tendsto_cons_iff [topological_space β]
   tendsto f (nhds (a :: l)) b ↔ tendsto (λp:α×list α, f (p.1 :: p.2)) ((nhds a).prod (nhds l)) b :=
 have nhds (a :: l) = ((nhds a).prod (nhds l)).map (λp:α×list α, (p.1 :: p.2)),
 begin
-  simp only [nhds_cons, prod_eq, (filter.map_def _ _).symm, (filter.seq_eq_filter_seq _ _).symm],
+  simp only
+    [nhds_cons, filter.prod_eq, (filter.map_def _ _).symm, (filter.seq_eq_filter_seq _ _).symm],
   simp [-filter.seq_eq_filter_seq, -filter.map_def, (∘)] with functor_norm,
 end,
 by rw [this, filter.tendsto_map'_iff]
@@ -1127,7 +1108,8 @@ lemma tendsto_insert_nth' {a : α} : ∀{n : ℕ} {l : list α},
   have (nhds a).prod (nhds (a' :: l)) =
     ((nhds a).prod ((nhds a').prod (nhds l))).map (λp:α×α×list α, (p.1, p.2.1 :: p.2.2)),
   begin
-    simp only [nhds_cons, prod_eq, (filter.map_def _ _).symm, (filter.seq_eq_filter_seq _ _).symm],
+    simp only
+      [nhds_cons, filter.prod_eq, (filter.map_def _ _).symm, (filter.seq_eq_filter_seq _ _).symm],
     simp [-filter.seq_eq_filter_seq, -filter.map_def, (∘)] with functor_norm
   end,
   begin

src/topology/instances/ennreal.lean

@@ -64,8 +64,8 @@ end
 lemma is_open_ne_top : is_open {a : ennreal | a ≠ ⊤} :=
 is_open_neg (is_closed_eq continuous_id continuous_const)
 
-lemma coe_image_univ_mem_nhds : (coe : nnreal → ennreal) '' univ ∈ (nhds (r : ennreal)).sets :=
-have {a : ennreal | a ≠ ⊤} = (coe : nnreal → ennreal) '' univ,
+lemma coe_range_mem_nhds : range (coe : nnreal → ennreal) ∈ (nhds (r : ennreal)).sets :=
+have {a : ennreal | a ≠ ⊤} = range (coe : nnreal → ennreal),
   from set.ext $ assume a, by cases a; simp [none_eq_top, some_eq_coe],
 this ▸ mem_nhds_sets is_open_ne_top coe_ne_top
 
@@ -78,14 +78,14 @@ continuous (λa, (f a : ennreal)) ↔ continuous f :=
 embedding_coe.continuous_iff.symm
 
 lemma nhds_coe {r : nnreal} : nhds (r : ennreal) = (nhds r).map coe :=
-by rw [embedding_coe.2, map_nhds_induced_eq coe_image_univ_mem_nhds]
+by rw [embedding_coe.2, map_nhds_induced_eq coe_range_mem_nhds]
 
 lemma nhds_coe_coe {r p : nnreal} : nhds ((r : ennreal), (p : ennreal)) =
   (nhds (r, p)).map (λp:nnreal×nnreal, (p.1, p.2)) :=
 begin
   rw [(embedding_prod_mk embedding_coe embedding_coe).map_nhds_eq],
-  rw [← univ_prod_univ, ← prod_image_image_eq],
-  exact prod_mem_nhds_sets coe_image_univ_mem_nhds coe_image_univ_mem_nhds
+  rw [← prod_range_range_eq],
+  exact prod_mem_nhds_sets coe_range_mem_nhds coe_range_mem_nhds
 end
 
 lemma tendsto_to_nnreal {a : ennreal} : a ≠ ⊤ →

src/topology/instances/nnreal.lean

@@ -25,6 +25,9 @@ instance : topological_semiring ℝ≥0 :=
           (continuous_add (continuous.comp continuous_fst continuous_subtype_val)
                           (continuous.comp continuous_snd continuous_subtype_val)) }
 
+instance : second_countable_topology nnreal :=
+topological_space.subtype.second_countable_topology _ _
+
 instance : orderable_topology ℝ≥0 :=
 ⟨ le_antisymm
     begin

src/topology/uniform_space/basic.lean

@@ -659,7 +659,7 @@ begin
     rcases c f' cf' this with ⟨x, xs, hx⟩,
     existsi [m x, mem_image_of_mem m xs],
     rw [(uniform_embedding.embedding hm).2, nhds_induced_eq_comap] at hx,
-    calc f ≤ map m f' : le_map_comap' fs (λb ⟨x, hx⟩, ⟨x, hx.2⟩)
+    calc f = map m f' : (map_comap $ filter.mem_sets_of_superset fs $ image_subset_range _ _).symm
       ... ≤ map m (comap m (nhds (m x))) : map_mono hx
       ... ≤ nhds (m x) : map_comap_le }
 end
@@ -1342,21 +1342,17 @@ begin
   rw [nhds_subtype_eq_comap] at hc,
   simp [comap_comap_comp] at hc,
   change (tendsto (f ∘ @subtype.val α p) (comap (e ∘ @subtype.val α p) (nhds b)) (nhds c)) at hc,
-  rw [←comap_comap_comp] at hc,
-  existsi c,
-  apply tendsto_comap'' s _ _ hc,
+  rw [←comap_comap_comp, tendsto_comap'_iff] at hc,
+  exact ⟨c, hc⟩,
   exact ⟨_, hb, assume x,
     begin
-      change e x ∈ (closure (e '' s)) → x ∈ s,
-      rw [←closure_induced, closure_eq_nhds],
-      dsimp,
-      rw [nhds_induced_eq_comap, de.induced],
-      change x ∈ {x | nhds x ⊓ principal s ≠ ⊥} → x ∈ s,
+      change e x ∈ (closure (e '' s)) → x ∈ range subtype.val,
+      rw [←closure_induced, closure_eq_nhds, mem_set_of_eq, (≠), nhds_induced_eq_comap, de.induced],
+      change x ∈ {x | nhds x ⊓ principal s ≠ ⊥} → x ∈ range subtype.val,
       rw [←closure_eq_nhds, closure_eq_of_is_closed hs],
-      exact id,
+      exact assume hxs, ⟨⟨x, hp x hxs⟩, rfl⟩,
       exact de.inj
-    end⟩,
-  exact (assume x hx, ⟨⟨x, hp x hx⟩, rfl⟩)
+    end⟩
 end
 
 section prod

src/topology/uniform_space/completion.lean

@@ -156,7 +156,8 @@ instance complete_space_separation [h : complete_space α] :
     cauchy_comap comap_quotient_le_uniformity hf $
       comap_neq_bot_of_surj hf.left $ assume b, quotient.exists_rep _,
   let ⟨x, (hx : f.comap (λx, ⟦x⟧) ≤ nhds x)⟩ := complete_space.complete this in
-  ⟨⟦x⟧, calc f ≤ map (λx, ⟦x⟧) (f.comap (λx, ⟦x⟧)) : le_map_comap $ assume b, quotient.exists_rep _
+  ⟨⟦x⟧, calc f = map (λx, ⟦x⟧) (f.comap (λx, ⟦x⟧)) :
+      (map_comap $ univ_mem_sets' $ assume b, quotient.exists_rep _).symm
     ... ≤ map (λx, ⟦x⟧) (nhds x) : map_mono hx
     ... ≤ _ : continuous_iff_tendsto.mp uniform_continuous_quotient_mk.continuous _⟩⟩