refactor(topology/*): use dot notation with compact, prove `compact…

….image` with `continuous_on` (#1809)

* refactor(topology/*): use dot notation, prove `compact.image` with `continuous_on`

* Apply suggestions from code review

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Fix compile, update some proofs

* Make `range_quot_mk` a `simp` lemma

* Fix lint errors

src/analysis/complex/polynomial.lean

@@ -13,10 +13,9 @@ lemma exists_forall_abs_polynomial_eval_le (p : polynomial ℂ) :
   ∃ x, ∀ y, (p.eval x).abs ≤ (p.eval y).abs :=
 if hp0 : 0 < degree p
 then let ⟨r, hr0, hr⟩ := polynomial.tendsto_infinity complex.abs hp0 ((p.eval 0).abs) in
-  let ⟨x, hx₁, hx₂⟩ := exists_forall_le_of_compact_of_continuous (λ y, (p.eval y).abs)
-    (continuous_abs.comp p.continuous_eval)
-    (closed_ball 0 r) (proper_space.compact_ball _ _)
-    (set.ne_empty_iff_exists_mem.2 ⟨0, by simp [le_of_lt hr0]⟩) in
+  let ⟨x, hx₁, hx₂⟩ := (proper_space.compact_ball (0:ℂ) r).exists_forall_le
+    (set.ne_empty_iff_exists_mem.2 ⟨0, by simp [le_of_lt hr0]⟩)
+    (λ z, abs (p.eval z)) (continuous_abs.comp p.continuous_eval).continuous_on in
   ⟨x, λ y, if hy : y.abs ≤ r then hx₂ y $ by simpa [complex.dist_eq] using hy
     else le_trans (hx₂ _ (by simp [le_of_lt hr0])) (le_of_lt (hr y (lt_of_not_ge hy)))⟩
 else ⟨p.coeff 0, by rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]; simp⟩

src/data/set/basic.lean

@@ -1159,6 +1159,12 @@ eq_univ_iff_forall
 
 @[simp] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id
 
+theorem range_inl_union_range_inr : range (@sum.inl α β) ∪ range sum.inr = univ :=
+ext $ λ x, by cases x; simp
+
+@[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
+range_iff_surjective.2 quot.exists_rep
+
 @[simp] theorem image_univ {ι : Type*} {f : ι → β} : f '' univ = range f :=
 ext $ by simp [image, range]
 

src/measure_theory/lebesgue_measure.lean

@@ -97,9 +97,8 @@ begin
   suffices : ∀ (s:finset ℕ) b
     (cv : Icc a b ⊆ ⋃ i ∈ (↑s:set ℕ), Ioo (c i) (d i)),
     (of_real (b - a) : ennreal) ≤ s.sum (λ i, of_real (d i - c i)),
-  { rcases @compact_elim_finite_subcover_image _ _
-      _ (Icc a b) univ (λ i, Ioo (c i) (d i)) compact_Icc
-      (λ i _, is_open_Ioo) (by simpa using ss) with ⟨s, su, hf, hs⟩,
+  { rcases compact_Icc.elim_finite_subcover_image (λ (i : ℕ) (_ : i ∈ univ),
+      @is_open_Ioo _ _ _ _ (c i) (d i)) (by simpa using ss) with ⟨s, su, hf, hs⟩,
     have e : (⋃ i ∈ (↑hf.to_finset:set ℕ),
       Ioo (c i) (d i)) = (⋃ i ∈ s, Ioo (c i) (d i)), {simp [set.ext_iff]},
     rw ennreal.tsum_eq_supr_sum,

src/order/filter/basic.lean

@@ -727,10 +727,8 @@ lemma map_le_iff_le_comap : map m f ≤ g ↔ f ≤ comap m g :=
 lemma gc_map_comap (m : α → β) : galois_connection (map m) (comap m) :=
 assume f g, map_le_iff_le_comap
 
-lemma map_mono (h : f₁ ≤ f₂) : map m f₁ ≤ map m f₂ := (gc_map_comap m).monotone_l h
-lemma monotone_map : monotone (map m) | a b := map_mono
-lemma comap_mono (h : g₁ ≤ g₂) : comap m g₁ ≤ comap m g₂ := (gc_map_comap m).monotone_u h
-lemma monotone_comap : monotone (comap m) | a b := comap_mono
+lemma map_mono : monotone (map m) := (gc_map_comap m).monotone_l
+lemma comap_mono : monotone (comap m) := (gc_map_comap m).monotone_u
 
 @[simp] lemma map_bot : map m ⊥ = ⊥ := (gc_map_comap m).l_bot
 @[simp] lemma map_sup : map m (f₁ ⊔ f₂) = map m f₁ ⊔ map m f₂ := (gc_map_comap m).l_sup
@@ -763,7 +761,7 @@ le_antisymm
         assume i,
         exact (ht i).2
       end⟩)
-  (supr_le $ assume i, monotone_comap $ le_supr _ _)
+  (supr_le $ assume i, comap_mono $ le_supr _ _)
 
 lemma comap_Sup {s : set (filter β)} {m : α → β} : comap m (Sup s) = (⨆f∈s, comap m f) :=
 by simp only [Sup_eq_supr, comap_supr, eq_self_iff_true]
@@ -774,7 +772,7 @@ le_antisymm
     ⟨t₁ ∪ t₂,
       ⟨g₁.sets_of_superset ht₁ (subset_union_left _ _), g₂.sets_of_superset ht₂ (subset_union_right _ _)⟩,
       union_subset hs₁ hs₂⟩)
-  (sup_le (comap_mono le_sup_left) (comap_mono le_sup_right))
+  ((@comap_mono _ _ m).le_map_sup _ _)
 
 lemma map_comap {f : filter β} {m : α → β} (hf : range m ∈ f) : (f.comap m).map m = f :=
 le_antisymm
@@ -803,7 +801,7 @@ this ▸ hb
 lemma le_of_map_le_map_inj_iff {f g : filter α} {m : α → β} {s : set α}
   (hsf : s ∈ f) (hsg : s ∈ g) (hm : ∀x∈s, ∀y∈s, m x = m y → x = y) :
   map m f ≤ map m g ↔ f ≤ g :=
-iff.intro (le_of_map_le_map_inj' hsf hsg hm) map_mono
+iff.intro (le_of_map_le_map_inj' hsf hsg hm) (λ h, map_mono h)
 
 lemma eq_of_map_eq_map_inj' {f g : filter α} {m : α → β} {s : set α}
   (hsf : s ∈ f) (hsg : s ∈ g) (hm : ∀x∈s, ∀y∈s, m x = m y → x = y)
@@ -846,13 +844,24 @@ forall_sets_neq_empty_iff_neq_bot.mp $ assume s ⟨t, ht, t_s⟩,
   let ⟨a, (ha : a ∈ preimage m t)⟩ := hm t ht in
   neq_bot_of_le_neq_bot (ne_empty_of_mem ha) t_s
 
-lemma comap_neq_bot_of_surj {f : filter β} {m : α → β}
-  (hf : f ≠ ⊥) (hm : ∀b, ∃a, m a = b) : comap m f ≠ ⊥ :=
+lemma comap_ne_bot_of_range_mem {f : filter β} {m : α → β}
+  (hf : f ≠ ⊥) (hm : range m ∈ f) : comap m f ≠ ⊥ :=
 comap_neq_bot $ assume t ht,
-  let
-    ⟨b, (hx : b ∈ t)⟩ := inhabited_of_mem_sets hf ht,
-    ⟨a, (ha : m a = b)⟩ := hm b
-  in ⟨a, ha.symm ▸ hx⟩
+  let ⟨_, ha, a, rfl⟩ := inhabited_of_mem_sets hf (inter_mem_sets ht hm)
+  in ⟨a, ha⟩
+
+lemma comap_inf_principal_ne_bot_of_image_mem {f : filter β} {m : α → β}
+  (hf : f ≠ ⊥) {s : set α} (hs : m '' s ∈ f) : (comap m f ⊓ principal s) ≠ ⊥ :=
+begin
+  refine compl_compl s ▸ mt mem_sets_of_neq_bot _,
+  rintros ⟨t, ht, hts⟩,
+  rcases inhabited_of_mem_sets hf (inter_mem_sets hs ht) with ⟨_, ⟨x, hxs, rfl⟩, hxt⟩,
+  exact absurd hxs (hts hxt)
+end
+
+lemma comap_neq_bot_of_surj {f : filter β} {m : α → β}
+  (hf : f ≠ ⊥) (hm : function.surjective m) : comap m f ≠ ⊥ :=
+comap_ne_bot_of_range_mem hf $ univ_mem_sets' hm
 
 @[simp] lemma map_eq_bot_iff : map m f = ⊥ ↔ f = ⊥ :=
 ⟨by rw [←empty_in_sets_eq_bot, ←empty_in_sets_eq_bot]; exact id,
@@ -915,12 +924,13 @@ calc map m (⨅i (h : p i), f i) = map m (⨅i:subtype p, f i.val) : by simp onl
     ⟨⟨i, hi⟩⟩
   ... = (⨅i (h : p i), map m (f i)) : by simp only [infi_subtype, eq_self_iff_true]
 
+lemma map_inf_le {f g : filter α} {m : α → β} : map m (f ⊓ g) ≤ map m f ⊓ map m g :=
+(@map_mono _ _ m).map_inf_le f g
+
 lemma map_inf' {f g : filter α} {m : α → β} {t : set α} (htf : t ∈ f) (htg : t ∈ g)
   (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
-    (le_inf (map_mono inf_le_left) (map_mono inf_le_right))
-    (assume s hs, _),
+  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 ⊢,
   rcases hs with ⟨t₁, h₁, t₂, h₂, hs⟩,
   refine ⟨m '' (t₁ ∩ t), _, m '' (t₂ ∩ t), _, _⟩,
@@ -932,9 +942,9 @@ begin
     { exact λ x ⟨_, hx⟩ y ⟨_, hy⟩, h x hx y hy } }
 end
 
-lemma map_inf {f g : filter α} {m : α → β} (h : ∀ x y, m x = m y → x = y) :
+lemma map_inf {f g : filter α} {m : α → β} (h : function.injective m) :
   map m (f ⊓ g) = map m f ⊓ map m g :=
-map_inf' univ_mem_sets univ_mem_sets (assume x _ y _, h x y)
+map_inf' univ_mem_sets univ_mem_sets (assume x _ y _ hxy, h hxy)
 
 lemma map_eq_comap_of_inverse {f : filter α} {m : α → β} {n : β → α}
   (h₁ : m ∘ n = id) (h₂ : n ∘ m = id) : map m f = comap n f :=
@@ -1185,6 +1195,10 @@ lemma tendsto_le_right {f : α → β} {x : filter α} {y z : filter β}
   (h₁ : y ≤ z) (h₂ : tendsto f x y) : tendsto f x z :=
 le_trans h₂ h₁
 
+lemma tendsto.ne_bot {f : α → β} {x : filter α} {y : filter β} (h : tendsto f x y) (hx : x ≠ ⊥) :
+  y ≠ ⊥ :=
+neq_bot_of_le_neq_bot (map_ne_bot hx) h
+
 lemma tendsto_map {f : α → β} {x : filter α} : tendsto f x (map f x) := le_refl (map f x)
 
 lemma tendsto_map' {f : β → γ} {g : α → β} {x : filter α} {y : filter γ}
@@ -1234,6 +1248,10 @@ lemma tendsto_inf_right {f : α → β} {x₁ x₂ : filter α} {y : filter β}
   (h : tendsto f x₂ y) : tendsto f (x₁ ⊓ x₂) y  :=
 le_trans (map_mono inf_le_right) h
 
+lemma tendsto.inf {f : α → β} {x₁ x₂ : filter α} {y₁ y₂ : filter β}
+  (h₁ : tendsto f x₁ y₁) (h₂ : tendsto f x₂ y₂) : tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂) :=
+tendsto_inf.2 ⟨tendsto_inf_left h₁, tendsto_inf_right h₂⟩
+
 lemma tendsto_infi {f : α → β} {x : filter α} {y : ι → filter β} :
   tendsto f x (⨅i, y i) ↔ ∀i, tendsto f x (y i) :=
 by simp only [tendsto, iff_self, lattice.le_infi_iff]

src/order/filter/lift.lean

@@ -57,13 +57,13 @@ 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 monotone_map.comp hg,
+  from map_mono.comp hg,
 filter_eq $ set.ext $
   by simp only [mem_lift_sets, hg, @mem_lift_sets _ _ f _ this, exists_prop, forall_const, mem_map, iff_self, 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 monotone_comap.comp hg,
+  from comap_mono.comp hg,
 filter_eq $ set.ext begin
   simp only [hg, @mem_lift_sets _ _ f _ this, comap, mem_lift_sets, mem_set_of_eq, exists_prop,
     function.comp_apply],

src/topology/algebra/ordered.lean

@@ -805,8 +805,8 @@ lemma bdd_below_of_compact {α : Type u} [topological_space α] [linear_order α
 begin
   by_contra H,
   letI := classical.DLO α,
-  rcases @compact_elim_finite_subcover_image α _ _ _ s (λ x, {b | x < b}) hs
-    (λ x _, is_open_lt continuous_const continuous_id) _ with ⟨t, st, ft, ht⟩,
+  rcases hs.elim_finite_subcover_image (λ x (_ : x ∈ s), @is_open_Ioi _ _ _ _ x) _
+    with ⟨t, st, ft, ht⟩,
   { refine H ((bdd_below_finite ft).imp $ λ C hC y hy, _),
     rcases mem_bUnion_iff.1 (ht hy) with ⟨x, hx, xy⟩,
     exact le_trans (hC hx) (le_of_lt xy) },
@@ -1111,11 +1111,11 @@ is_connected_Icc.intermediate_value (right_mem_Icc.2 hab) (left_mem_Icc.2 hab) h
 end densely_ordered
 
 /-- The extreme value theorem: a continuous function realizes its minimum on a compact set -/
-lemma exists_forall_le_of_compact_of_continuous {α : Type u} [topological_space α]
-  (f : α → β) (hf : continuous f) (s : set α) (hs : compact s) (ne_s : s ≠ ∅) :
+lemma compact.exists_forall_le {α : Type u} [topological_space α]
+  {s : set α} (hs : compact s) (ne_s : s ≠ ∅) (f : α → β) (hf : continuous_on f s) :
   ∃x∈s, ∀y∈s, f x ≤ f y :=
 begin
-  have C : compact (f '' s) := compact_image hs hf,
+  have C : compact (f '' s) := hs.image_of_continuous_on hf,
   haveI := has_Inf_to_nonempty β,
   have B : bdd_below (f '' s) := bdd_below_of_compact C,
   have : Inf (f '' s) ∈ f '' s :=
@@ -1125,10 +1125,10 @@ begin
 end
 
 /-- The extreme value theorem: a continuous function realizes its maximum on a compact set -/
-lemma exists_forall_ge_of_compact_of_continuous {α : Type u} [topological_space α] :
-  ∀ f : α → β, continuous f → ∀ s : set α, compact s → s ≠ ∅ →
+lemma compact.exists_forall_ge {α : Type u} [topological_space α]:
+  ∀ {s : set α}, compact s → s ≠ ∅ → ∀ {f : α → β}, continuous_on f s →
   ∃x∈s, ∀y∈s, f y ≤ f x :=
-@exists_forall_le_of_compact_of_continuous (order_dual β) _ _ _ _ _
+@compact.exists_forall_le (order_dual β) _ _ _ _ _
 
 end conditionally_complete_linear_order
 

src/topology/bounded_continuous_function.lean

@@ -63,8 +63,7 @@ bounded_range_iff.2 f.2.2
 /-- If a function is continuous on a compact space, it is automatically bounded,
 and therefore gives rise to an element of the type of bounded continuous functions -/
 def mk_of_compact [compact_space α] (f : α → β) (hf : continuous f) : α →ᵇ β :=
-⟨f, hf, bounded_range_iff.1 $ by rw ← image_univ; exact
-  bounded_of_compact (compact_image compact_univ hf)⟩
+⟨f, hf, bounded_range_iff.1 $ bounded_of_compact $ compact_range hf⟩
 
 /-- If a function is bounded on a discrete space, it is automatically continuous,
 and therefore gives rise to an element of the type of bounded continuous functions -/
@@ -255,7 +254,7 @@ begin
   /- For all x, the set hU x is an open set containing x on which the elements of A
   fluctuate by at most ε₂.
   We extract finitely many of these sets that cover the whole space, by compactness -/
-  rcases compact_elim_finite_subcover_image compact_univ
+  rcases compact_univ.elim_finite_subcover_image
     (λx _, (hU x).2.1) (λx hx, mem_bUnion (mem_univ _) (hU x).1)
     with ⟨tα, _, ⟨_⟩, htα⟩,
   /- tα : set α, htα : univ ⊆ ⋃x ∈ tα, U x -/
@@ -304,7 +303,7 @@ begin
   have M : lipschitz_with 1 coe := lipschitz_with.subtype_coe s,
   let F : (α →ᵇ s) → α →ᵇ β := comp coe M,
   refine compact_of_is_closed_subset
-    (compact_image (_ : compact (F ⁻¹' A)) (continuous_comp M)) closed (λ f hf, _),
+    ((_ : compact (F ⁻¹' A)).image (continuous_comp M)) closed (λ f hf, _),
   { haveI : compact_space s := compact_iff_compact_space.1 hs,
     refine arzela_ascoli₁ _ (continuous_iff_is_closed.1 (continuous_comp M) _ closed)
       (λ x ε ε0, bex.imp_right (λ U U_nhds hU y z hy hz f hf, _) (H x ε ε0)),

src/topology/continuous_on.lean

@@ -186,6 +186,14 @@ begin
     exact forall_sets_neq_empty_iff_neq_bot.2 h (u ∩ s) this }
 end
 
+lemma nhds_within_ne_bot_of_mem {s : set α} {x : α} (hx : x ∈ s) :
+  nhds_within x s ≠ ⊥ :=
+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
+
 /-
 nhds_within and subtypes
 -/

src/topology/homeomorph.lean

@@ -72,17 +72,15 @@ le_antisymm
     rwa [coinduced_compose, self_comp_symm, coinduced_id] at this,
   end
 
+protected lemma embedding (h : α ≃ₜ β) : embedding h :=
+⟨⟨h.induced_eq.symm⟩, h.to_equiv.injective⟩
+
 lemma compact_image {s : set α} (h : α ≃ₜ β) : compact (h '' s) ↔ compact s :=
-⟨λ hs, by have := compact_image hs h.symm.continuous;
-  rwa [← image_comp, symm_comp_self, image_id] at this,
-λ hs, compact_image hs h.continuous⟩
+h.embedding.compact_iff_compact_image.symm
 
 lemma compact_preimage {s : set β} (h : α ≃ₜ β) : compact (h ⁻¹' s) ↔ compact s :=
 by rw ← image_symm; exact h.symm.compact_image
 
-protected lemma embedding (h : α ≃ₜ β) : embedding h :=
-⟨⟨h.induced_eq.symm⟩, h.to_equiv.injective⟩
-
 protected lemma dense_embedding (h : α ≃ₜ β) : dense_embedding h :=
 { dense   := assume a, by rw [h.range_coe, closure_univ]; trivial,
   inj     := h.to_equiv.injective,

src/topology/instances/complex.lean

@@ -119,7 +119,8 @@ instance : topological_ring ℂ :=
 
 instance : topological_semiring ℂ := by apply_instance -- short-circuit type class inference
 
-def real_prod_homeo : homeomorph ℂ (ℝ × ℝ) :=
+/-- `ℂ` is homeomorphic to the real plane with `max` norm. -/
+def real_prod_homeo : ℂ ≃ₜ (ℝ × ℝ) :=
 { to_equiv := real_prod_equiv,
   continuous_to_fun := continuous_re.prod_mk continuous_im,
   continuous_inv_fun := show continuous (λ p : ℝ × ℝ, complex.mk p.1 p.2),
@@ -131,7 +132,7 @@ instance : proper_space ℂ :=
 ⟨λx r, begin
   refine real_prod_homeo.symm.compact_preimage.1
     (compact_of_is_closed_subset
-      (compact_prod _ _ (proper_space.compact_ball x.re r) (proper_space.compact_ball x.im r))
+      ((proper_space.compact_ball x.re r).prod (proper_space.compact_ball x.im r))
       (continuous_iff_is_closed.1 real_prod_homeo.symm.continuous _ is_closed_ball) _),
   exact λ p h, ⟨
     le_trans (abs_re_le_abs (⟨p.1, p.2⟩ - x)) h,

src/topology/metric_space/basic.lean

@@ -1035,16 +1035,18 @@ section compact
 /-- Any compact set in a metric space can be covered by finitely many balls of a given positive
 radius -/
 lemma finite_cover_balls_of_compact {α : Type u} [metric_space α] {s : set α}
-  (hs : compact s) {e : ℝ} (he : e > 0) :
+  (hs : compact s) {e : ℝ} (he : 0 < e) :
   ∃t ⊆ s, finite t ∧ s ⊆ ⋃x∈t, ball x e :=
 begin
-  apply compact_elim_finite_subcover_image hs,
+  apply hs.elim_finite_subcover_image,
   { simp [is_open_ball] },
   { intros x xs,
     simp,
     exact ⟨x, ⟨xs, by simpa⟩⟩ }
 end
 
+alias finite_cover_balls_of_compact ← compact.finite_cover_balls
+
 end compact
 
 section proper_space
@@ -1068,7 +1070,7 @@ lemma proper_space_of_compact_closed_ball_of_le
       apply inter_eq_self_of_subset_right,
       exact closed_ball_subset_closed_ball (le_of_lt (not_le.1 hr)) },
     rw this,
-    exact compact_inter (h x R (le_refl _)) is_closed_ball }
+    exact (h x R (le_refl _)).inter_right is_closed_ball }
 end⟩
 
 /- A compact metric space is proper -/
@@ -1195,7 +1197,7 @@ lemma second_countable_of_countable_discretization {α : Type u} [metric_space 
   second_countable_topology α :=
 begin
   classical, by_cases hs : (univ : set α) = ∅,
-  { haveI : compact_space α := ⟨by rw hs; exact compact_of_finite (set.finite_empty)⟩, by apply_instance },
+  { haveI : compact_space α := ⟨by rw hs; exact compact_empty⟩, by apply_instance },
   rcases exists_mem_of_ne_empty hs with ⟨x0, hx0⟩,
   letI : inhabited α := ⟨x0⟩,
   refine second_countable_of_almost_dense_set (λε ε0, _),
@@ -1303,9 +1305,11 @@ lemma bounded_of_compact {s : set α} (h : compact s) : bounded s :=
 let ⟨t, ht, fint, subs⟩ := finite_cover_balls_of_compact h zero_lt_one in
 bounded.subset subs $ (bounded_bUnion fint).2 $ λ i hi, bounded_ball
 
+alias bounded_of_compact ← compact.bounded
+
 /-- A finite set is bounded -/
 lemma bounded_of_finite {s : set α} (h : finite s) : bounded s :=
-bounded_of_compact $ compact_of_finite h
+h.compact.bounded
 
 /-- A singleton is bounded -/
 lemma bounded_singleton {x : α} : bounded ({x} : set α) :=
@@ -1319,12 +1323,12 @@ exists_congr $ λ C, ⟨
 
 /-- In a compact space, all sets are bounded -/
 lemma bounded_of_compact_space [compact_space α] : bounded s :=
-(bounded_of_compact compact_univ).subset (subset_univ _)
+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, bounded_of_compact h⟩, begin
+⟨λ h, ⟨closed_of_compact _ h, h.bounded⟩, begin
   rintro ⟨hc, hb⟩,
   classical, by_cases s = ∅, {simp [h, compact_empty]},
   rcases exists_mem_of_ne_empty h with ⟨x, hx⟩,
@@ -1351,7 +1355,7 @@ begin
       exact mul_le_mul_of_nonneg_left (add_le_add hx hy) (le_max_right _ _)
     end⟩,
   have : compact K := compact_iff_closed_bounded.2 ⟨A, B⟩,
-  have C : compact (f '' K) := compact_image this f_cont,
+  have C : compact (f '' K) := this.image f_cont,
   have : f '' K = closed_ball x₀ r,
     by { rw image_preimage_eq_of_subset, rw hf, exact subset_univ _ },
   rwa this at C