chore(topology/*): use dot syntax for some lemmas (#3251)

Rename:

* `closure_eq_of_is_closed` to `is_closed.closure_eq`;
* `closed_of_compact` to `compact.is_closed`;
* `bdd_above_of_compact` to `compact.bdd_above`;
* `bdd_below_of_compact` to `compact.bdd_below`.
* `is_complete_of_is_closed` to `is_closed.is_complete`
* `is_closed_of_is_complete` to `is_complete.is_closed`
* `is_closed_iff_nhds` to `is_closed_iff_cluster_pt`
* `closure_subset_iff_subset_of_is_closed` to `is_closed.closure_subset_iff`

Add:

* `closure_closed_ball` (`@[simp]` lemma)
* `is_closed.closure_subset : is_closed s → closure s ⊆ s`

src/algebraic_geometry/prime_spectrum.lean

@@ -354,7 +354,7 @@ begin
     rw [subset_zero_locus_iff_subset_vanishing_ideal] at ht,
     calc fs ⊆ vanishing_ideal t : ht
         ... ⊆ x.as_ideal        : hx },
-  { rw closure_subset_iff_subset_of_is_closed (is_closed_zero_locus _),
+  { rw (is_closed_zero_locus _).closure_subset_iff,
     exact subset_zero_locus_vanishing_ideal t }
 end
 
@@ -366,7 +366,7 @@ begin
   let I : ι → ideal R := λ i, vanishing_ideal (Z i),
   have hI : ∀ i, Z i = zero_locus (I i),
   { intro i,
-    rw [zero_locus_vanishing_ideal_eq_closure, closure_eq_of_is_closed],
+    rw [zero_locus_vanishing_ideal_eq_closure, is_closed.closure_eq],
     exact hZc i },
   have one_mem : (1:R) ∈ ⨆ (i : ι), I i,
   { rw [← ideal.eq_top_iff_one, ← zero_locus_empty_iff_eq_top, zero_locus_supr],

src/analysis/calculus/fderiv.lean

@@ -260,7 +260,7 @@ begin
     have : closure (submodule.span 𝕜 (tangent_cone_at 𝕜 s x) : set E) ⊆ closure K :=
       closure_mono this,
     have : y ∈ closure K := this hy,
-    rwa closure_eq_of_is_closed (is_closed_eq f'.continuous f₁'.continuous) at this },
+    rwa (is_closed_eq f'.continuous f₁'.continuous).closure_eq at this },
   rw H.1 at C,
   ext y,
   exact C y (mem_univ _)

src/analysis/calculus/inverse.lean

@@ -289,7 +289,7 @@ begin
     { exact lipschitz_with.of_dist_le_mul (λ x x', hf.inverse_approx_map_contracts_on
         y (hε x.mem) (hε x'.mem)) } },
   refine ⟨this.efixed_point' _ _ _ b (mem_closed_ball_self ε0) (edist_lt_top _ _), _, _⟩,
-  { exact is_complete_of_is_closed is_closed_ball },
+  { exact is_closed_ball.is_complete },
   { apply contracting_with.efixed_point_mem' },
   { exact (inverse_approx_map_fixed_iff y).1 (this.efixed_point_is_fixed_pt' _ _ _ _) }
 end

src/analysis/convex/topology.lean

@@ -116,7 +116,7 @@ end
 /-- Convex hull of a finite set is closed. -/
 lemma set.finite.is_closed_convex_hull [t2_space E] {s : set E} (hs : finite s) :
   is_closed (convex_hull s) :=
-closed_of_compact _ hs.compact_convex_hull
+hs.compact_convex_hull.is_closed
 
 end topological_vector_space
 

src/analysis/normed_space/basic.lean

@@ -825,12 +825,12 @@ end
 
 theorem frontier_closed_ball [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :
   frontier (closed_ball x r) = sphere x r :=
-by rw [frontier, closure_eq_of_is_closed is_closed_ball, interior_closed_ball x hr,
+by rw [frontier, closure_closed_ball, interior_closed_ball x hr,
   closed_ball_diff_ball]
 
 theorem frontier_closed_ball' [normed_space ℝ E] (x : E) (r : ℝ) (hE : ∃ z : E, z ≠ 0) :
   frontier (closed_ball x r) = sphere x r :=
-by rw [frontier, closure_eq_of_is_closed is_closed_ball, interior_closed_ball' x r hE,
+by rw [frontier, closure_closed_ball, interior_closed_ball' x r hE,
   closed_ball_diff_ball]
 
 open normed_field

src/analysis/normed_space/finite_dimension.lean

@@ -97,7 +97,7 @@ begin
         exact (equiv_fun_basis b_basis).symm.uniform_embedding (linear_map.continuous_on_pi _) this },
       have : is_complete (s : set E),
         from complete_space_coe_iff_is_complete.1 ((complete_space_congr U).1 (by apply_instance)),
-      exact is_closed_of_is_complete this },
+      exact this.is_closed },
     -- second step: any linear form is continuous, as its kernel is closed by the first step
     have H₂ : ∀f : E →ₗ[𝕜] 𝕜, continuous f,
     { assume f,
@@ -199,7 +199,7 @@ complete_space_coe_iff_is_complete.1 (finite_dimensional.complete 𝕜 s)
 /-- A finite-dimensional subspace is closed. -/
 lemma submodule.closed_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
   is_closed (s : set E) :=
-is_closed_of_is_complete s.complete_of_finite_dimensional
+s.complete_of_finite_dimensional.is_closed
 
 lemma continuous_linear_map.exists_right_inverse_of_surjective [finite_dimensional 𝕜 F]
   (f : E →L[𝕜] F) (hf : f.range = ⊤) :

src/topology/algebra/module.lean

@@ -344,7 +344,7 @@ continuous_iff_is_closed.1 f.cont _ is_closed_singleton
 lemma is_complete_ker {M' : Type*} [uniform_space M'] [complete_space M'] [add_comm_monoid M']
   [semimodule R M'] [t1_space M₂] (f : M' →L[R] M₂) :
   is_complete (f.ker : set M') :=
-is_complete_of_is_closed f.is_closed_ker
+f.is_closed_ker.is_complete
 
 instance complete_space_ker {M' : Type*} [uniform_space M'] [complete_space M'] [add_comm_monoid M']
   [semimodule R M'] [t1_space M₂] (f : M' →L[R] M₂) :

src/topology/algebra/ordered.lean

@@ -166,7 +166,7 @@ ge_of_tendsto nt lim (eventually_of_forall _ h)
 @[simp]
 lemma closure_le_eq [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
   closure {b | f b ≤ g b} = {b | f b ≤ g b} :=
-closure_eq_iff_is_closed.mpr $ is_closed_le hf hg
+(is_closed_le hf hg).closure_eq
 
 lemma closure_lt_subset_le [topological_space β] {f g : β → α} (hf : continuous f)
   (hg : continuous g) :
@@ -178,15 +178,8 @@ lemma continuous_within_at.closure_le [topological_space β]
  (hf : continuous_within_at f s x)
  (hg : continuous_within_at g s x)
  (h : ∀ y ∈ s, f y ≤ g y) : f x ≤ g x :=
-begin
-  show (f x, g x) ∈ {p : α × α | p.1 ≤ p.2},
-  suffices : (f x, g x) ∈ closure {p : α × α | p.1 ≤ p.2},
-    begin
-      rwa closure_eq_of_is_closed at this,
-      exact order_closed_topology.is_closed_le'
-    end,
-  exact (continuous_within_at.prod hf hg).mem_closure hx h
-end
+show (f x, g x) ∈ {p : α × α | p.1 ≤ p.2},
+from order_closed_topology.is_closed_le'.closure_subset ((hf.prod hg).mem_closure hx h)
 
 /-- If `s` is a closed set and two functions `f` and `g` are continuous on `s`,
 then the set `{x ∈ s | f x ≤ g x}` is a closed set. -/
@@ -202,7 +195,7 @@ variables [topological_space α] [partial_order α] [t : order_closed_topology 
 include t
 
 private lemma is_closed_eq : is_closed {p : α × α | p.1 = p.2} :=
-by simp [le_antisymm_iff];
+by simp only [le_antisymm_iff];
    exact is_closed_inter t.is_closed_le' (is_closed_le continuous_snd continuous_fst)
 
 @[priority 90] -- see Note [lower instance priority]
@@ -1085,18 +1078,18 @@ by rw closure_eq_cluster_pts; exact ha.nhds_within_ne_bot hs
 
 lemma mem_of_is_lub_of_is_closed {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty)
   (sc : is_closed s) : a ∈ s :=
-by rw ←closure_eq_of_is_closed sc; exact mem_closure_of_is_lub ha hs
+by rw ←sc.closure_eq; exact mem_closure_of_is_lub ha hs
 
 lemma mem_closure_of_is_glb {a : α} {s : set α} (ha : is_glb s a) (hs : s.nonempty) :
   a ∈ closure s :=
 by rw closure_eq_cluster_pts; exact ha.nhds_within_ne_bot hs
 
 lemma mem_of_is_glb_of_is_closed {a : α} {s : set α} (ha : is_glb s a) (hs : s.nonempty)
   (sc : is_closed s) : a ∈ s :=
-by rw ←closure_eq_of_is_closed sc; exact mem_closure_of_is_glb ha hs
+by rw ←sc.closure_eq; exact mem_closure_of_is_glb ha hs
 
 /-- A compact set is bounded below -/
-lemma bdd_below_of_compact {α : Type u} [topological_space α] [linear_order α]
+lemma compact.bdd_below {α : Type u} [topological_space α] [linear_order α]
   [order_closed_topology α] [nonempty α] {s : set α} (hs : compact s) : bdd_below s :=
 begin
   by_contra H,
@@ -1111,9 +1104,9 @@ begin
 end
 
 /-- A compact set is bounded above -/
-lemma bdd_above_of_compact {α : Type u} [topological_space α] [linear_order α]
+lemma compact.bdd_above {α : Type u} [topological_space α] [linear_order α]
   [order_topology α] : Π [nonempty α] {s : set α}, compact s → bdd_above s :=
-@bdd_below_of_compact (order_dual α) _ _ _
+@compact.bdd_below (order_dual α) _ _ _
 
 end order_topology
 
@@ -1618,15 +1611,15 @@ end densely_ordered
 
 lemma compact.Inf_mem {s : set α} (hs : compact s) (ne_s : s.nonempty) :
   Inf s ∈ s :=
-(closed_of_compact s hs).cInf_mem ne_s (bdd_below_of_compact hs)
+hs.is_closed.cInf_mem ne_s hs.bdd_below
 
 lemma compact.Sup_mem {s : set α} (hs : compact s) (ne_s : s.nonempty) :
   Sup s ∈ s :=
 @compact.Inf_mem (order_dual α) _ _ _ _ hs ne_s
 
 lemma compact.is_glb_Inf {s : set α} (hs : compact s) (ne_s : s.nonempty) :
   is_glb s (Inf s) :=
-is_glb_cInf ne_s (bdd_below_of_compact hs)
+is_glb_cInf ne_s hs.bdd_below
 
 lemma compact.is_lub_Sup {s : set α} (hs : compact s) (ne_s : s.nonempty) :
   is_lub s (Sup s) :=
@@ -1686,8 +1679,8 @@ lemma compact.exists_Sup_image_eq {α : Type u} [topological_space α]:
 
 lemma eq_Icc_of_connected_compact {s : set α} (h₁ : is_connected s) (h₂ : compact s) :
   s = Icc (Inf s) (Sup s) :=
-eq_Icc_cInf_cSup_of_connected_bdd_closed h₁ (bdd_below_of_compact h₂) (bdd_above_of_compact h₂)
-  (closed_of_compact s h₂)
+eq_Icc_cInf_cSup_of_connected_bdd_closed h₁ h₂.bdd_below h₂.bdd_above
+  h₂.is_closed
 
 end conditionally_complete_linear_order
 

src/topology/basic.lean

@@ -281,13 +281,13 @@ subset_sInter $ assume t ⟨h₁, h₂⟩, h₂
 lemma closure_minimal {s t : set α} (h₁ : s ⊆ t) (h₂ : is_closed t) : closure s ⊆ t :=
 sInter_subset_of_mem ⟨h₂, h₁⟩
 
-lemma closure_eq_of_is_closed {s : set α} (h : is_closed s) : closure s = s :=
+lemma is_closed.closure_eq {s : set α} (h : is_closed s) : closure s = s :=
 subset.antisymm (closure_minimal (subset.refl s) h) subset_closure
 
-lemma closure_eq_iff_is_closed {s : set α} : closure s = s ↔ is_closed s :=
-⟨assume h, h ▸ is_closed_closure, closure_eq_of_is_closed⟩
+lemma is_closed.closure_subset {s : set α} (hs : is_closed s) : closure s ⊆ s :=
+closure_minimal (subset.refl _) hs
 
-lemma closure_subset_iff_subset_of_is_closed {s t : set α} (h₁ : is_closed t) :
+lemma is_closed.closure_subset_iff {s t : set α} (h₁ : is_closed t) :
   closure s ⊆ t ↔ s ⊆ t :=
 ⟨subset.trans subset_closure, assume h, closure_minimal h h₁⟩
 
@@ -304,21 +304,27 @@ lemma closure_inter_subset_inter_closure (s t : set α) :
 lemma is_closed_of_closure_subset {s : set α} (h : closure s ⊆ s) : is_closed s :=
 by rw subset.antisymm subset_closure h; exact is_closed_closure
 
+lemma closure_eq_iff_is_closed {s : set α} : closure s = s ↔ is_closed s :=
+⟨assume h, h ▸ is_closed_closure, is_closed.closure_eq⟩
+
+lemma closure_subset_iff_is_closed {s : set α} : closure s ⊆ s ↔ is_closed s :=
+⟨is_closed_of_closure_subset, is_closed.closure_subset⟩
+
 @[simp] lemma closure_empty : closure (∅ : set α) = ∅ :=
-closure_eq_of_is_closed is_closed_empty
+is_closed_empty.closure_eq
 
-lemma closure_empty_iff (s : set α) : closure s = ∅ ↔ s = ∅ :=
+@[simp] lemma closure_empty_iff (s : set α) : closure s = ∅ ↔ s = ∅ :=
 ⟨subset_eq_empty subset_closure, λ h, h.symm ▸ closure_empty⟩
 
 lemma set.nonempty.closure {s : set α} (h : s.nonempty) :
   set.nonempty (closure s) :=
 let ⟨x, hx⟩ := h in ⟨x, subset_closure hx⟩
 
 @[simp] lemma closure_univ : closure (univ : set α) = univ :=
-closure_eq_of_is_closed is_closed_univ
+is_closed_univ.closure_eq
 
 @[simp] lemma closure_closure {s : set α} : closure (closure s) = closure s :=
-closure_eq_of_is_closed is_closed_closure
+is_closed_closure.closure_eq
 
 @[simp] lemma closure_union {s t : set α} : closure (s ∪ t) = closure s ∪ closure t :=
 subset.antisymm
@@ -396,7 +402,7 @@ by simpa only [frontier_compl, ← compl_union]
   using frontier_inter_subset sᶜ tᶜ
 
 lemma is_closed.frontier_eq {s : set α} (hs : is_closed s) : frontier s = s \ interior s :=
-by rw [frontier, closure_eq_of_is_closed hs]
+by rw [frontier, hs.closure_eq]
 
 lemma is_open.frontier_eq {s : set α} (hs : is_open s) : frontier s = closure s \ s :=
 by rw [frontier, interior_eq_of_open hs]
@@ -625,10 +631,9 @@ begin
   rw [←le_principal_iff, inf_comm, le_inf_iff]
 end
 
-lemma is_closed_iff_nhds {s : set α} : is_closed s ↔ ∀a, cluster_pt a (𝓟 s) → a ∈ s :=
-calc is_closed s ↔ closure s = s : by rw [closure_eq_iff_is_closed]
-  ... ↔ closure s ⊆ s : ⟨assume h, by rw h, assume h, subset.antisymm h subset_closure⟩
-  ... ↔ (∀a, cluster_pt a (𝓟 s) → a ∈ s) : by rw [closure_eq_cluster_pts]; refl
+lemma is_closed_iff_cluster_pt {s : set α} : is_closed s ↔ ∀a, cluster_pt a (𝓟 s) → a ∈ s :=
+calc is_closed s ↔ closure s ⊆ s : closure_subset_iff_is_closed.symm
+  ... ↔ (∀a, cluster_pt a (𝓟 s) → a ∈ s) : by simp only [subset_def, mem_closure_iff_cluster_pt]
 
 lemma closure_inter_open {s t : set α} (h : is_open s) : s ∩ closure t ⊆ closure (s ∩ t) :=
 assume a ⟨hs, ht⟩,
@@ -661,11 +666,11 @@ lemma mem_of_closed_of_tendsto {f : β → α} {b : filter β} {a : α} {s : set
   (hb : b ≠ ⊥) (hf : tendsto f b (𝓝 a)) (hs : is_closed s) (h : f ⁻¹' s ∈ b) : a ∈ s :=
 have b.map f ≤ 𝓝 a ⊓ 𝓟 s,
   from le_trans (le_inf (le_refl _) (le_principal_iff.mpr h)) (inf_le_inf_right _ hf),
-is_closed_iff_nhds.mp hs a $ ne_bot_of_le_ne_bot (map_ne_bot hb) this
+is_closed_iff_cluster_pt.mp hs a $ ne_bot_of_le_ne_bot (map_ne_bot hb) this
 
 lemma mem_of_closed_of_tendsto' {f : β → α} {x : filter β} {a : α} {s : set α}
   (hf : tendsto f x (𝓝 a)) (hs : is_closed s) (h : x ⊓ 𝓟 (f ⁻¹' s) ≠ ⊥) : a ∈ s :=
-is_closed_iff_nhds.mp hs _ $ ne_bot_of_le_ne_bot (@map_ne_bot _ _ _ f h) $
+is_closed_iff_cluster_pt.mp hs _ $ ne_bot_of_le_ne_bot (@map_ne_bot _ _ _ f h) $
   le_inf (le_trans (map_mono $ inf_le_left) hf) $
     le_trans (map_mono $ inf_le_right_of_le $
       by simp only [comap_principal, le_principal_iff]; exact subset.refl _) (@map_comap_le _ _ _ f)

src/topology/bounded_continuous_function.lean

@@ -313,7 +313,7 @@ theorem arzela_ascoli
 /- This version is deduced from the previous one by checking that the closure of A, in
 addition to being closed, still satisfies the properties of compact range and equicontinuity -/
 arzela_ascoli₂ s hs (closure A) is_closed_closure
-  (λ f x hf, (mem_of_closed' (closed_of_compact _ hs)).2 $ λ ε ε0,
+  (λ f x hf, (mem_of_closed' hs.is_closed).2 $ λ ε ε0,
     let ⟨g, gA, dist_fg⟩ := metric.mem_closure_iff.1 hf ε ε0 in
     ⟨g x, in_s g x gA, lt_of_le_of_lt (dist_coe_le_dist _) dist_fg⟩)
   (λ x ε ε0, show ∃ U ∈ 𝓝 x,

src/topology/constructions.lean

@@ -319,7 +319,7 @@ show (λp:α×β, f p.1 p.2) (a, b) ∈ closure u, from
 
 lemma is_closed_prod {s₁ : set α} {s₂ : set β} (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
   is_closed (set.prod s₁ s₂) :=
-closure_eq_iff_is_closed.mp $ by simp [h₁, h₂, closure_prod_eq, closure_eq_of_is_closed]
+closure_eq_iff_is_closed.mp $ by simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]
 
 lemma inducing.prod_mk {f : α → β} {g : γ → δ} (hf : inducing f) (hg : inducing g) :
   inducing (λx:α×γ, (f x.1, g x.2)) :=
@@ -778,12 +778,11 @@ end ulift
 
 lemma mem_closure_of_continuous [topological_space α] [topological_space β]
   {f : α → β} {a : α} {s : set α} {t : set β}
-  (hf : continuous f) (ha : a ∈ closure s) (h : ∀a∈s, f a ∈ closure t) :
+  (hf : continuous f) (ha : a ∈ closure s) (h : maps_to f s (closure t)) :
   f a ∈ closure t :=
 calc f a ∈ f '' closure s : mem_image_of_mem _ ha
   ... ⊆ closure (f '' s) : image_closure_subset_closure_image hf
-  ... ⊆ closure (closure t) : closure_mono $ image_subset_iff.mpr $ h
-  ... ⊆ closure t : begin rw [closure_eq_of_is_closed], exact subset.refl _, exact is_closed_closure end
+  ... ⊆ closure t : closure_minimal h.image_subset is_closed_closure
 
 lemma mem_closure_of_continuous2 [topological_space α] [topological_space β] [topological_space γ]
   {f : α → β → γ} {a : α} {b : β} {s : set α} {t : set β} {u : set γ}

src/topology/continuous_on.lean

@@ -182,7 +182,7 @@ mem_closure_iff_nhds_within_ne_bot.1 $ subset_closure hx
 
 lemma is_closed.mem_of_nhds_within_ne_bot {s : set α} (hs : is_closed s)
   {x : α} (hx : nhds_within x s ≠ ⊥) : x ∈ s :=
-by simpa only [closure_eq_of_is_closed hs] using mem_closure_iff_nhds_within_ne_bot.2 hx
+by simpa only [hs.closure_eq] using mem_closure_iff_nhds_within_ne_bot.2 hx
 
 /-
 nhds_within and subtypes

src/topology/dense_embedding.lean

@@ -185,7 +185,7 @@ let ⟨s'', hs''₁, hs''₂, hs''₃⟩ := nhds_is_closed hs in
 let ⟨s', hs'₁, (hs'₂ : i ⁻¹' s' ⊆ f ⁻¹' s'')⟩ := mem_of_nhds hφ hs''₁ in
 let ⟨t, (ht₁ : t ⊆ φ ∩ s'), ht₂, ht₃⟩ := mem_nhds_sets_iff.mp $ inter_mem_sets hφ hs'₁ in
 have h₁ : closure (f '' (i ⁻¹' s')) ⊆ s'',
-  by rw [closure_subset_iff_subset_of_is_closed hs''₃, image_subset_iff]; exact hs'₂,
+  by rw [hs''₃.closure_subset_iff, image_subset_iff]; exact hs'₂,
 have h₂ : t ⊆ di.extend f ⁻¹' closure (f '' (i ⁻¹' t)), from
   assume b' hb',
   have 𝓝 b' ≤ 𝓟 t, by simp; exact mem_nhds_sets ht₂ hb',
@@ -287,7 +287,7 @@ lemma is_closed_property [topological_space β] {e : α → β} {p : β → Prop
 have univ ⊆ {b | p b},
   from calc univ = closure (range e) : he.closure_range.symm
     ... ⊆ closure {b | p b} : closure_mono $ range_subset_iff.mpr h
-    ... = _ : closure_eq_of_is_closed hp,
+    ... = _ : hp.closure_eq,
 assume b, this trivial
 
 lemma is_closed_property2 [topological_space β] {e : α → β} {p : β → β → Prop}

src/topology/instances/real.lean

@@ -284,7 +284,7 @@ section
 
 lemma closure_of_rat_image_lt {q : ℚ} : closure ((coe:ℚ → ℝ) '' {x | q < x}) = {r | ↑q ≤ r} :=
 subset.antisymm
-  ((closure_subset_iff_subset_of_is_closed (is_closed_ge' _)).2
+  ((is_closed_ge' _).closure_subset_iff.2
     (image_subset_iff.2 $ λ p h, le_of_lt $ (@rat.cast_lt ℝ _ _ _).2 h)) $
 λ x hx, mem_closure_iff_nhds.2 $ λ t ht,
 let ⟨ε, ε0, hε⟩ := metric.mem_nhds_iff.1 ht in

src/topology/metric_space/baire.lean

@@ -330,7 +330,7 @@ begin
     have : x ∈ g s := mem_bInter_iff.1 hx s hs,
     have : x ∈ interior (f s),
     { have : x ∈ f s \ (frontier (f s)) := mem_inter xs this,
-      simpa [frontier, xs, closure_eq_of_is_closed (hc s hs)] using this },
+      simpa [frontier, xs, (hc s hs).closure_eq] using this },
     exact mem_bUnion_iff.2 ⟨s, ⟨hs, this⟩⟩ },
   have := closure_mono this,
   rw clos_g at this,

src/topology/metric_space/basic.lean

@@ -1101,6 +1101,9 @@ variables {x y z : α} {ε ε₁ ε₂ : ℝ} {s : set α}
 theorem is_closed_ball : is_closed (closed_ball x ε) :=
 is_closed_le (continuous_id.dist continuous_const) continuous_const
 
+@[simp] theorem closure_closed_ball : closure (closed_ball x ε) = closed_ball x ε :=
+is_closed_ball.closure_eq
+
 theorem closure_ball_subset_closed_ball : closure (ball x ε) ⊆ closed_ball x ε :=
 closure_minimal ball_subset_closed_ball is_closed_ball
 
@@ -1133,7 +1136,7 @@ lemma mem_closure_range_iff_nat {α : Type u} [metric_space α] {e : β → α}
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem mem_of_closed' {α : Type u} [metric_space α] {s : set α} (hs : is_closed s)
   {a : α} : a ∈ s ↔ ∀ε>0, ∃b ∈ s, dist a b < ε :=
-by simpa only [closure_eq_of_is_closed hs] using @mem_closure_iff _ _ s a
+by simpa only [hs.closure_eq] using @mem_closure_iff _ _ s a
 
 end metric
 
@@ -1466,7 +1469,7 @@ begin
     exact this (x, y) (mk_mem_prod x_in y_in) },
   intros p p_in,
   have := mem_closure continuous_dist p_in h,
-  rwa closure_eq_of_is_closed (is_closed_le' C) at this
+  rwa (is_closed_le' C).closure_eq at this
 end
 
 alias bounded_closure_of_bounded ← bounded.closure
@@ -1522,7 +1525,7 @@ compact_univ.bounded.subset (subset_univ _)
 In a proper space, a set is compact if and only if it is closed and bounded -/
 lemma compact_iff_closed_bounded [proper_space α] :
   compact s ↔ is_closed s ∧ bounded s :=
-⟨λ h, ⟨closed_of_compact _ h, h.bounded⟩, begin
+⟨λ h, ⟨h.is_closed, h.bounded⟩, begin
   rintro ⟨hc, hb⟩,
   cases s.eq_empty_or_nonempty with h h, {simp [h, compact_empty]},
   rcases h with ⟨x, hx⟩,
@@ -1538,7 +1541,7 @@ begin
   apply proper_space_of_compact_closed_ball_of_le 0 (λx₀ r hr, _),
   let K := f ⁻¹' (closed_ball x₀ r),
   have A : is_closed K :=
-    continuous_iff_is_closed.1 f_cont (closed_ball x₀ r) (is_closed_ball),
+    continuous_iff_is_closed.1 f_cont (closed_ball x₀ r) is_closed_ball,
   have B : bounded K := ⟨max C 0 * (r + r), λx y hx hy, calc
     dist x y ≤ C * dist (f x) (f y) : hC x y
     ... ≤ max C 0 * dist (f x) (f y) : mul_le_mul_of_nonneg_right (le_max_left _ _) (dist_nonneg)