diff --git a/archive/wiedijk_100_theorems/ascending_descending_sequences.lean b/archive/wiedijk_100_theorems/ascending_descending_sequences.lean
index 2c2d3931d8d69..a0d947a8089a5 100644
--- a/archive/wiedijk_100_theorems/ascending_descending_sequences.lean
+++ b/archive/wiedijk_100_theorems/ascending_descending_sequences.lean
@@ -24,7 +24,6 @@ sequences, increasing, decreasing, Ramsey, Erdos-Szekeres, Erdős–Szekeres, Er
 variables {α : Type*} [linear_order α] {β : Type*}
 
 open function finset
-open_locale classical
 
 namespace theorems_100
 
diff --git a/src/analysis/normed_space/continuous_linear_map.lean b/src/analysis/normed_space/continuous_linear_map.lean
index 693adffcd123e..87ad5e2c41002 100644
--- a/src/analysis/normed_space/continuous_linear_map.lean
+++ b/src/analysis/normed_space/continuous_linear_map.lean
@@ -192,27 +192,6 @@ lemma to_span_singleton_homothety (x : E) (c : 𝕜) :
   ‖linear_map.to_span_singleton 𝕜 E x c‖ = ‖x‖ * ‖c‖ :=
 by {rw mul_comm, exact norm_smul _ _}
 
-/-- Given an element `x` of a normed space `E` over a field `𝕜`, the natural continuous
-    linear map from `𝕜` to `E` by taking multiples of `x`.-/
-def to_span_singleton (x : E) : 𝕜 →L[𝕜] E :=
-of_homothety (linear_map.to_span_singleton 𝕜 E x) ‖x‖ (to_span_singleton_homothety 𝕜 x)
-
-lemma to_span_singleton_apply (x : E) (r : 𝕜) : to_span_singleton 𝕜 x r = r • x :=
-by simp [to_span_singleton, of_homothety, linear_map.to_span_singleton]
-
-lemma to_span_singleton_add (x y : E) :
-  to_span_singleton 𝕜 (x + y) = to_span_singleton 𝕜 x + to_span_singleton 𝕜 y :=
-by { ext1, simp [to_span_singleton_apply], }
-
-lemma to_span_singleton_smul' (𝕜') [normed_field 𝕜'] [normed_space 𝕜' E]
-  [smul_comm_class 𝕜 𝕜' E] (c : 𝕜') (x : E) :
-  to_span_singleton 𝕜 (c • x) = c • to_span_singleton 𝕜 x :=
-by { ext1, rw [to_span_singleton_apply, smul_apply, to_span_singleton_apply, smul_comm], }
-
-lemma to_span_singleton_smul (c : 𝕜) (x : E) :
-  to_span_singleton 𝕜 (c • x) = c • to_span_singleton 𝕜 x :=
-to_span_singleton_smul' 𝕜 𝕜 c x
-
 end continuous_linear_map
 
 section
diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
index 30687beee91e0..43bca0b7aca26 100644
--- a/src/data/finset/basic.lean
+++ b/src/data/finset/basic.lean
@@ -570,6 +570,10 @@ lemma forall_mem_cons (h : a ∉ s) (p : α → Prop) :
   (∀ x, x ∈ cons a s h → p x) ↔ p a ∧ ∀ x, x ∈ s → p x :=
 by simp only [mem_cons, or_imp_distrib, forall_and_distrib, forall_eq]
 
+/-- Useful in proofs by induction. -/
+lemma forall_of_forall_cons {p : α → Prop} {h : a ∉ s} (H : ∀ x, x ∈ cons a s h → p x) (x)
+  (h : x ∈ s) : p x := H _ $ mem_cons.2 $ or.inr h
+
 @[simp] lemma mk_cons {s : multiset α} (h : (a ::ₘ s).nodup) :
   (⟨a ::ₘ s, h⟩ : finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 := rfl
 
@@ -2084,6 +2088,10 @@ lemma forall_mem_insert [decidable_eq α] (a : α) (s : finset α) (p : α → P
   (∀ x, x ∈ insert a s → p x) ↔ p a ∧ ∀ x, x ∈ s → p x :=
 by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq]
 
+/-- Useful in proofs by induction. -/
+lemma forall_of_forall_insert [decidable_eq α] {p : α → Prop} {a : α} {s : finset α}
+  (H : ∀ x, x ∈ insert a s → p x) (x) (h : x ∈ s) : p x := H _ $ mem_insert_of_mem h
+
 end finset
 
 /-- Equivalence between the set of natural numbers which are `≥ k` and `ℕ`, given by `n → n - k`. -/
diff --git a/src/data/finset/n_ary.lean b/src/data/finset/n_ary.lean
index 3a0db131eab7b..dd7d4df71f086 100644
--- a/src/data/finset/n_ary.lean
+++ b/src/data/finset/n_ary.lean
@@ -358,6 +358,37 @@ lemma image₂_right_identity {f : γ → β → γ} {b : β} (h : ∀ a, f a b
   image₂ f s {b} = s :=
 by rw [image₂_singleton_right, funext h, image_id']
 
+/-- If each partial application of `f` is injective, and images of `s` under those partial
+applications are disjoint (but not necessarily distinct!), then the size of `t` divides the size of
+`finset.image₂ f s t`. -/
+lemma card_dvd_card_image₂_right (hf : ∀ a ∈ s, injective (f a))
+  (hs : ((λ a, t.image $ f a) '' s).pairwise_disjoint id) :
+  t.card ∣ (image₂ f s t).card :=
+begin
+  classical,
+  induction s using finset.induction with a s ha ih,
+  { simp },
+  specialize ih (forall_of_forall_insert hf)
+    (hs.subset $ set.image_subset _ $ coe_subset.2 $ subset_insert _ _),
+  rw image₂_insert_left,
+  by_cases h : disjoint (image (f a) t) (image₂ f s t),
+  { rw card_union_eq h,
+    exact (card_image_of_injective _ $ hf _ $ mem_insert_self _ _).symm.dvd.add ih },
+  simp_rw [←bUnion_image_left, disjoint_bUnion_right, not_forall] at h,
+  obtain ⟨b, hb, h⟩ := h,
+  rwa union_eq_right_iff_subset.2,
+  exact (hs.eq (set.mem_image_of_mem _ $ mem_insert_self _ _)
+    (set.mem_image_of_mem _ $ mem_insert_of_mem hb) h).trans_subset (image_subset_image₂_right hb),
+end
+
+/-- If each partial application of `f` is injective, and images of `t` under those partial
+applications are disjoint (but not necessarily distinct!), then the size of `s` divides the size of
+`finset.image₂ f s t`. -/
+lemma card_dvd_card_image₂_left (hf : ∀ b ∈ t, injective (λ a, f a b))
+  (ht : ((λ b, s.image $ λ a, f a b) '' t).pairwise_disjoint id) :
+  s.card ∣ (image₂ f s t).card :=
+by { rw ←image₂_swap, exact card_dvd_card_image₂_right hf ht }
+
 variables [decidable_eq α] [decidable_eq β]
 
 lemma image₂_inter_union_subset_union :
diff --git a/src/data/finset/pointwise.lean b/src/data/finset/pointwise.lean
index 03063a1ed2bc6..0f441be5a12ec 100644
--- a/src/data/finset/pointwise.lean
+++ b/src/data/finset/pointwise.lean
@@ -1078,6 +1078,24 @@ coe_injective $ by { push_cast, exact set.smul_univ hs }
 @[simp, to_additive] lemma card_smul_finset (a : α) (s : finset β) : (a • s).card = s.card :=
 card_image_of_injective _ $ mul_action.injective _
 
+/-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily distinct!), then
+the size of `t` divides the size of `s * t`. -/
+@[to_additive "If the left cosets of `t` by elements of `s` are disjoint (but not necessarily
+distinct!), then the size of `t` divides the size of `s + t`."]
+lemma card_dvd_card_smul_right {s : finset α} :
+  ((• t) '' (s : set α)).pairwise_disjoint id → t.card ∣ (s • t).card :=
+card_dvd_card_image₂_right (λ _ _, mul_action.injective _)
+
+variables [decidable_eq α]
+
+/-- If the right cosets of `s` by elements of `t` are disjoint (but not necessarily distinct!), then
+the size of `s` divides the size of `s * t`. -/
+@[to_additive "If the right cosets of `s` by elements of `t` are disjoint (but not necessarily
+distinct!), then the size of `s` divides the size of `s + t`."]
+lemma card_dvd_card_mul_left {s t : finset α} :
+  ((λ b, s.image $ λ a, a * b) '' (t : set α)).pairwise_disjoint id → s.card ∣ (s * t).card :=
+card_dvd_card_image₂_left (λ _ _, mul_left_injective _)
+
 end group
 
 section group_with_zero
diff --git a/src/order/directed.lean b/src/order/directed.lean
index b5c5f44c6f8fc..83c44b4bf2b62 100644
--- a/src/order/directed.lean
+++ b/src/order/directed.lean
@@ -131,6 +131,10 @@ lemma directed_on_of_inf_mem [semilattice_inf α] {S : set α}
   (H : ∀ ⦃i j⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S) : directed_on (≥) S :=
 λ a ha b hb, ⟨a ⊓ b, H ha hb, inf_le_left, inf_le_right⟩
 
+lemma is_total.directed [is_total α r] (f : ι → α) :
+  directed r f :=
+λ i j, or.cases_on (total_of r (f i) (f j)) (λ h, ⟨j, h, refl _⟩) (λ h, ⟨i, refl _, h⟩)
+
 /-- `is_directed α r` states that for any elements `a`, `b` there exists an element `c` such that
 `r a c` and `r b c`. -/
 class is_directed (α : Type*) (r : α → α → Prop) : Prop :=
@@ -150,7 +154,7 @@ lemma directed_on_univ_iff : directed_on r set.univ ↔ is_directed α r :=
 
 @[priority 100]  -- see Note [lower instance priority]
 instance is_total.to_is_directed [is_total α r] : is_directed α r :=
-⟨λ a b, or.cases_on (total_of r a b) (λ h, ⟨b, h, refl _⟩) (λ h, ⟨a, refl _, h⟩)⟩
+by rw ← directed_id_iff; exact is_total.directed _
 
 lemma is_directed_mono [is_directed α r] (h : ∀ ⦃a b⦄, r a b → s a b) : is_directed α s :=
 ⟨λ a b, let ⟨c, ha, hb⟩ := is_directed.directed a b in ⟨c, h ha, h hb⟩⟩
diff --git a/src/order/monotone/basic.lean b/src/order/monotone/basic.lean
index 84433c7deff17..9ca070071a7ca 100644
--- a/src/order/monotone/basic.lean
+++ b/src/order/monotone/basic.lean
@@ -102,6 +102,21 @@ def strict_anti_on (f : α → β) (s : set α) : Prop :=
 
 end monotone_def
 
+section decidable
+
+variables [preorder α] [preorder β] {f : α → β} {s : set α}
+
+instance [i : decidable (∀ a b, a ≤ b → f a ≤ f b)] : decidable (monotone f) := i
+instance [i : decidable (∀ a b, a ≤ b → f b ≤ f a)] : decidable (antitone f) := i
+instance [i : decidable (∀ a b ∈ s, a ≤ b → f a ≤ f b)] : decidable (monotone_on f s) := i
+instance [i : decidable (∀ a b ∈ s, a ≤ b → f b ≤ f a)] : decidable (antitone_on f s) := i
+instance [i : decidable (∀ a b, a < b → f a < f b)] : decidable (strict_mono f) := i
+instance [i : decidable (∀ a b, a < b → f b < f a)] : decidable (strict_anti f) := i
+instance [i : decidable (∀ a b ∈ s, a < b → f a < f b)] : decidable (strict_mono_on f s) := i
+instance [i : decidable (∀ a b ∈ s, a < b → f b < f a)] : decidable (strict_anti_on f s) := i
+
+end decidable
+
 /-! ### Monotonicity on the dual order
 
 Strictly, many of the `*_on.dual` lemmas in this section should use `of_dual ⁻¹' s` instead of `s`,
diff --git a/src/topology/algebra/module/basic.lean b/src/topology/algebra/module/basic.lean
index 5379fd79c140b..f7d3e1befccef 100644
--- a/src/topology/algebra/module/basic.lean
+++ b/src/topology/algebra/module/basic.lean
@@ -1003,6 +1003,37 @@ lemma smul_right_comp [has_continuous_mul R₁] {x : M₂} {c : R₁} :
     smul_right (1 : R₁ →L[R₁] R₁) (c • x) :=
 by { ext, simp [mul_smul] }
 
+section to_span_singleton
+variables (R₁)
+variables [has_continuous_smul R₁ M₁]
+
+/-- Given an element `x` of a topological space `M` over a semiring `R`, the natural continuous
+linear map from `R` to `M` by taking multiples of `x`.-/
+def to_span_singleton (x : M₁) : R₁ →L[R₁] M₁ :=
+{ to_linear_map := linear_map.to_span_singleton R₁ M₁ x,
+  cont := continuous_id.smul continuous_const }
+
+lemma to_span_singleton_apply (x : M₁) (r : R₁) : to_span_singleton R₁ x r = r • x :=
+rfl
+
+lemma to_span_singleton_add [has_continuous_add M₁] (x y : M₁) :
+  to_span_singleton R₁ (x + y) = to_span_singleton R₁ x + to_span_singleton R₁ y :=
+by { ext1, simp [to_span_singleton_apply], }
+
+lemma to_span_singleton_smul' {α} [monoid α] [distrib_mul_action α M₁]
+  [has_continuous_const_smul α M₁]
+  [smul_comm_class R₁ α M₁] (c : α) (x : M₁) :
+  to_span_singleton R₁ (c • x) = c • to_span_singleton R₁ x :=
+by { ext1, rw [to_span_singleton_apply, smul_apply, to_span_singleton_apply, smul_comm], }
+
+/-- A special case of `to_span_singleton_smul'` for when `R` is commutative. -/
+lemma to_span_singleton_smul (R) {M₁} [comm_semiring R] [add_comm_monoid M₁] [module R M₁]
+  [topological_space R] [topological_space M₁] [has_continuous_smul R M₁] (c : R) (x : M₁) :
+  to_span_singleton R (c • x) = c • to_span_singleton R x :=
+to_span_singleton_smul' R c x
+
+end to_span_singleton
+
 end semiring
 
 section pi
diff --git a/src/topology/algebra/order/compact.lean b/src/topology/algebra/order/compact.lean
index c7e46e18e122e..0eedd6364138d 100644
--- a/src/topology/algebra/order/compact.lean
+++ b/src/topology/algebra/order/compact.lean
@@ -136,80 +136,39 @@ is_compact_iff_compact_space.mp is_compact_Icc
 end
 
 /-!
-### Min and max elements of a compact set
+### Extreme value theorem
 -/
 
-variables {α β γ : Type*} [conditionally_complete_linear_order α] [topological_space α]
-  [order_topology α] [topological_space β] [topological_space γ]
-
-lemma is_compact.Inf_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
-  Inf s ∈ s :=
-hs.is_closed.cInf_mem ne_s hs.bdd_below
-
-lemma is_compact.Sup_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : Sup s ∈ s :=
-@is_compact.Inf_mem αᵒᵈ _ _ _ _ hs ne_s
-
-lemma is_compact.is_glb_Inf {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
-  is_glb s (Inf s) :=
-is_glb_cInf ne_s hs.bdd_below
-
-lemma is_compact.is_lub_Sup {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
-  is_lub s (Sup s) :=
-@is_compact.is_glb_Inf αᵒᵈ _ _ _ _ hs ne_s
-
-lemma is_compact.is_least_Inf {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
-  is_least s (Inf s) :=
-⟨hs.Inf_mem ne_s, (hs.is_glb_Inf ne_s).1⟩
+section linear_order
 
-lemma is_compact.is_greatest_Sup {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
-  is_greatest s (Sup s) :=
-@is_compact.is_least_Inf αᵒᵈ _ _ _ _ hs ne_s
+variables {α β γ : Type*} [linear_order α] [topological_space α]
+  [order_closed_topology α] [topological_space β] [topological_space γ]
 
 lemma is_compact.exists_is_least {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
   ∃ x, is_least s x :=
-⟨_, hs.is_least_Inf ne_s⟩
+begin
+  haveI : nonempty s := ne_s.to_subtype,
+  suffices : (s ∩ ⋂ x ∈ s, Iic x).nonempty,
+    from ⟨this.some, this.some_spec.1, mem_Inter₂.mp this.some_spec.2⟩,
+  rw bInter_eq_Inter,
+  by_contra H,
+  rw not_nonempty_iff_eq_empty at H,
+  rcases hs.elim_directed_family_closed (λ x : s, Iic ↑x) (λ x, is_closed_Iic) H
+    ((is_total.directed coe).mono_comp _ (λ _ _, Iic_subset_Iic.mpr)) with ⟨x, hx⟩,
+  exact not_nonempty_iff_eq_empty.mpr hx ⟨x, x.2, le_rfl⟩
+end
 
 lemma is_compact.exists_is_greatest {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
   ∃ x, is_greatest s x :=
-⟨_, hs.is_greatest_Sup ne_s⟩
+@is_compact.exists_is_least αᵒᵈ _ _ _ _ hs ne_s
 
 lemma is_compact.exists_is_glb {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
   ∃ x ∈ s, is_glb s x :=
-⟨_, hs.Inf_mem ne_s, hs.is_glb_Inf ne_s⟩
+exists_imp_exists (λ x (hx : is_least s x), ⟨hx.1, hx.is_glb⟩) (hs.exists_is_least ne_s)
 
 lemma is_compact.exists_is_lub {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
   ∃ x ∈ s, is_lub s x :=
-⟨_, hs.Sup_mem ne_s, hs.is_lub_Sup ne_s⟩
-
-lemma is_compact.exists_Inf_image_eq_and_le {s : set β} (hs : is_compact s) (ne_s : s.nonempty)
-  {f : β → α} (hf : continuous_on f s) :
-  ∃ x ∈ s, Inf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y :=
-let ⟨x, hxs, hx⟩ := (hs.image_of_continuous_on hf).Inf_mem (ne_s.image f)
-in ⟨x, hxs, hx.symm, λ y hy,
-  hx.trans_le $ cInf_le (hs.image_of_continuous_on hf).bdd_below $ mem_image_of_mem f hy⟩
-
-lemma is_compact.exists_Sup_image_eq_and_ge {s : set β} (hs : is_compact s) (ne_s : s.nonempty)
-  {f : β → α} (hf : continuous_on f s) :
-  ∃ x ∈ s, Sup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x :=
-@is_compact.exists_Inf_image_eq_and_le αᵒᵈ _ _ _ _ _ _ hs ne_s _ hf
-
-lemma is_compact.exists_Inf_image_eq {s : set β} (hs : is_compact s) (ne_s : s.nonempty)
-  {f : β → α} (hf : continuous_on f s) :
-  ∃ x ∈ s,  Inf (f '' s) = f x :=
-let ⟨x, hxs, hx, _⟩ := hs.exists_Inf_image_eq_and_le ne_s hf in ⟨x, hxs, hx⟩
-
-lemma is_compact.exists_Sup_image_eq :
-  ∀ {s : set β}, is_compact s → s.nonempty → ∀ {f : β → α}, continuous_on f s →
-  ∃ x ∈ s, Sup (f '' s) = f x :=
-@is_compact.exists_Inf_image_eq αᵒᵈ _ _ _ _ _
-
-lemma eq_Icc_of_connected_compact {s : set α} (h₁ : is_connected s) (h₂ : is_compact s) :
-  s = Icc (Inf s) (Sup s) :=
-eq_Icc_cInf_cSup_of_connected_bdd_closed h₁ h₂.bdd_below h₂.bdd_above h₂.is_closed
-
-/-!
-### Extreme value theorem
--/
+@is_compact.exists_is_glb αᵒᵈ _ _ _ _ hs ne_s
 
 /-- The **extreme value theorem**: a continuous function realizes its minimum on a compact set. -/
 lemma is_compact.exists_forall_le {s : set β} (hs : is_compact s) (ne_s : s.nonempty)
@@ -277,6 +236,68 @@ lemma continuous.exists_forall_ge [nonempty β] {f : β → α}
   ∃ x, ∀ y, f y ≤ f x :=
 @continuous.exists_forall_le αᵒᵈ _ _ _ _ _ _ _ hf hlim
 
+/-- A continuous function with compact support has a global minimum. -/
+@[to_additive "A continuous function with compact support has a global minimum."]
+lemma continuous.exists_forall_le_of_has_compact_mul_support [nonempty β] [has_one α]
+  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
+  ∃ (x : β), ∀ (y : β), f x ≤ f y :=
+begin
+  obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.is_compact_range hf).exists_is_least (range_nonempty _),
+  rw [mem_lower_bounds, forall_range_iff] at hx,
+  exact ⟨x, hx⟩,
+end
+
+/-- A continuous function with compact support has a global maximum. -/
+@[to_additive "A continuous function with compact support has a global maximum."]
+lemma continuous.exists_forall_ge_of_has_compact_mul_support [nonempty β] [has_one α]
+  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
+  ∃ (x : β), ∀ (y : β), f y ≤ f x :=
+@continuous.exists_forall_le_of_has_compact_mul_support αᵒᵈ _ _ _ _ _ _ _ _ hf h
+
+/-- A compact set is bounded below -/
+lemma is_compact.bdd_below [nonempty α] {s : set α} (hs : is_compact s) : bdd_below s :=
+begin
+  cases s.eq_empty_or_nonempty,
+  { rw h,
+    exact bdd_below_empty },
+  { obtain ⟨a, ha, has⟩ := hs.exists_is_least h,
+    exact ⟨a, has⟩ },
+end
+
+/-- A compact set is bounded above -/
+lemma is_compact.bdd_above [nonempty α] {s : set α} (hs : is_compact s) : bdd_above s :=
+@is_compact.bdd_below αᵒᵈ _ _ _ _ _ hs
+
+/-- A continuous function is bounded below on a compact set. -/
+lemma is_compact.bdd_below_image [nonempty α] {f : β → α} {K : set β}
+  (hK : is_compact K) (hf : continuous_on f K) : bdd_below (f '' K) :=
+(hK.image_of_continuous_on hf).bdd_below
+
+/-- A continuous function is bounded above on a compact set. -/
+lemma is_compact.bdd_above_image [nonempty α] {f : β → α} {K : set β}
+  (hK : is_compact K) (hf : continuous_on f K) : bdd_above (f '' K) :=
+@is_compact.bdd_below_image αᵒᵈ _ _ _ _ _ _ _ _ hK hf
+
+/-- A continuous function with compact support is bounded below. -/
+@[to_additive /-" A continuous function with compact support is bounded below. "-/]
+lemma continuous.bdd_below_range_of_has_compact_mul_support [has_one α] {f : β → α}
+  (hf : continuous f) (h : has_compact_mul_support f) : bdd_below (range f) :=
+(h.is_compact_range hf).bdd_below
+
+/-- A continuous function with compact support is bounded above. -/
+@[to_additive /-" A continuous function with compact support is bounded above. "-/]
+lemma continuous.bdd_above_range_of_has_compact_mul_support [has_one α]
+  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
+  bdd_above (range f) :=
+@continuous.bdd_below_range_of_has_compact_mul_support αᵒᵈ _ _ _ _ _ _ _ hf h
+
+end linear_order
+
+section conditionally_complete_linear_order
+
+variables {α β γ : Type*} [conditionally_complete_linear_order α] [topological_space α]
+  [order_closed_topology α] [topological_space β] [topological_space γ]
+
 lemma is_compact.Sup_lt_iff_of_continuous {f : β → α}
   {K : set β} (hK : is_compact K) (h0K : K.nonempty) (hf : continuous_on f K) (y : α) :
   Sup (f '' K) < y ↔ ∀ x ∈ K, f x < y :=
@@ -294,23 +315,71 @@ lemma is_compact.lt_Inf_iff_of_continuous {α β : Type*}
   y < Inf (f '' K) ↔ ∀ x ∈ K, y < f x :=
 @is_compact.Sup_lt_iff_of_continuous αᵒᵈ β _ _ _ _ _ _ hK h0K hf y
 
-/-- A continuous function with compact support has a global minimum. -/
-@[to_additive "A continuous function with compact support has a global minimum."]
-lemma continuous.exists_forall_le_of_has_compact_mul_support [nonempty β] [has_one α]
-  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
-  ∃ (x : β), ∀ (y : β), f x ≤ f y :=
-begin
-  obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.is_compact_range hf).exists_is_least (range_nonempty _),
-  rw [mem_lower_bounds, forall_range_iff] at hx,
-  exact ⟨x, hx⟩,
-end
+end conditionally_complete_linear_order
 
-/-- A continuous function with compact support has a global maximum. -/
-@[to_additive "A continuous function with compact support has a global maximum."]
-lemma continuous.exists_forall_ge_of_has_compact_mul_support [nonempty β] [has_one α]
-  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
-  ∃ (x : β), ∀ (y : β), f y ≤ f x :=
-@continuous.exists_forall_le_of_has_compact_mul_support αᵒᵈ _ _ _ _ _ _ _ _ hf h
+/-!
+### Min and max elements of a compact set
+-/
+
+section order_closed_topology
+
+variables {α β γ : Type*} [conditionally_complete_linear_order α] [topological_space α]
+  [order_closed_topology α] [topological_space β] [topological_space γ]
+
+lemma is_compact.Inf_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
+  Inf s ∈ s :=
+let ⟨a, ha⟩ := hs.exists_is_least ne_s in
+ha.Inf_mem
+
+lemma is_compact.Sup_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : Sup s ∈ s :=
+@is_compact.Inf_mem αᵒᵈ _ _ _ _ hs ne_s
+
+lemma is_compact.is_glb_Inf {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
+  is_glb s (Inf s) :=
+is_glb_cInf ne_s hs.bdd_below
+
+lemma is_compact.is_lub_Sup {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
+  is_lub s (Sup s) :=
+@is_compact.is_glb_Inf αᵒᵈ _ _ _ _ hs ne_s
+
+lemma is_compact.is_least_Inf {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
+  is_least s (Inf s) :=
+⟨hs.Inf_mem ne_s, (hs.is_glb_Inf ne_s).1⟩
+
+lemma is_compact.is_greatest_Sup {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
+  is_greatest s (Sup s) :=
+@is_compact.is_least_Inf αᵒᵈ _ _ _ _ hs ne_s
+
+lemma is_compact.exists_Inf_image_eq_and_le {s : set β} (hs : is_compact s) (ne_s : s.nonempty)
+  {f : β → α} (hf : continuous_on f s) :
+  ∃ x ∈ s, Inf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y :=
+let ⟨x, hxs, hx⟩ := (hs.image_of_continuous_on hf).Inf_mem (ne_s.image f)
+in ⟨x, hxs, hx.symm, λ y hy,
+  hx.trans_le $ cInf_le (hs.image_of_continuous_on hf).bdd_below $ mem_image_of_mem f hy⟩
+
+lemma is_compact.exists_Sup_image_eq_and_ge {s : set β} (hs : is_compact s) (ne_s : s.nonempty)
+  {f : β → α} (hf : continuous_on f s) :
+  ∃ x ∈ s, Sup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x :=
+@is_compact.exists_Inf_image_eq_and_le αᵒᵈ _ _ _ _ _ _ hs ne_s _ hf
+
+lemma is_compact.exists_Inf_image_eq {s : set β} (hs : is_compact s) (ne_s : s.nonempty)
+  {f : β → α} (hf : continuous_on f s) :
+  ∃ x ∈ s,  Inf (f '' s) = f x :=
+let ⟨x, hxs, hx, _⟩ := hs.exists_Inf_image_eq_and_le ne_s hf in ⟨x, hxs, hx⟩
+
+lemma is_compact.exists_Sup_image_eq :
+  ∀ {s : set β}, is_compact s → s.nonempty → ∀ {f : β → α}, continuous_on f s →
+  ∃ x ∈ s, Sup (f '' s) = f x :=
+@is_compact.exists_Inf_image_eq αᵒᵈ _ _ _ _ _
+
+end order_closed_topology
+
+variables {α β γ : Type*} [conditionally_complete_linear_order α] [topological_space α]
+  [order_topology α] [topological_space β] [topological_space γ]
+
+lemma eq_Icc_of_connected_compact {s : set α} (h₁ : is_connected s) (h₂ : is_compact s) :
+  s = Icc (Inf s) (Sup s) :=
+eq_Icc_cInf_cSup_of_connected_bdd_closed h₁ h₂.bdd_below h₂.bdd_above h₂.is_closed
 
 lemma is_compact.continuous_Sup {f : γ → β → α}
   {K : set β} (hK : is_compact K) (hf : continuous ↿f) :
diff --git a/src/topology/order/basic.lean b/src/topology/order/basic.lean
index 733fa1a9de319..a17106de53df5 100644
--- a/src/topology/order/basic.lean
+++ b/src/topology/order/basic.lean
@@ -648,48 +648,6 @@ lemma dense.exists_between [densely_ordered α] {s : set α} (hs : dense s) {x y
   ∃ z ∈ s, z ∈ Ioo x y :=
 hs.exists_mem_open is_open_Ioo (nonempty_Ioo.2 h)
 
-variables [nonempty α] [topological_space β]
-
-/-- A compact set is bounded below -/
-lemma is_compact.bdd_below {s : set α} (hs : is_compact s) : bdd_below s :=
-begin
-  by_contra H,
-  rcases hs.elim_finite_subcover_image (λ x (_ : x ∈ s), @is_open_Ioi _ _ _ _ x) _
-    with ⟨t, st, ft, ht⟩,
-  { refine H (ft.bdd_below.imp $ λ C hC y hy, _),
-    rcases mem_Union₂.1 (ht hy) with ⟨x, hx, xy⟩,
-    exact le_trans (hC hx) (le_of_lt xy) },
-  { refine λ x hx, mem_Union₂.2 (not_imp_comm.1 _ H),
-    exact λ h, ⟨x, λ y hy, le_of_not_lt (h.imp $ λ ys, ⟨_, hy, ys⟩)⟩ }
-end
-
-/-- A compact set is bounded above -/
-lemma is_compact.bdd_above {s : set α} (hs : is_compact s) : bdd_above s :=
-@is_compact.bdd_below αᵒᵈ _ _ _ _ _ hs
-
-/-- A continuous function is bounded below on a compact set. -/
-lemma is_compact.bdd_below_image {f : β → α} {K : set β}
-  (hK : is_compact K) (hf : continuous_on f K) : bdd_below (f '' K) :=
-(hK.image_of_continuous_on hf).bdd_below
-
-/-- A continuous function is bounded above on a compact set. -/
-lemma is_compact.bdd_above_image {f : β → α} {K : set β}
-  (hK : is_compact K) (hf : continuous_on f K) : bdd_above (f '' K) :=
-@is_compact.bdd_below_image αᵒᵈ _ _ _ _ _ _ _ _ hK hf
-
-/-- A continuous function with compact support is bounded below. -/
-@[to_additive /-" A continuous function with compact support is bounded below. "-/]
-lemma continuous.bdd_below_range_of_has_compact_mul_support [has_one α] {f : β → α}
-  (hf : continuous f) (h : has_compact_mul_support f) : bdd_below (range f) :=
-(h.is_compact_range hf).bdd_below
-
-/-- A continuous function with compact support is bounded above. -/
-@[to_additive /-" A continuous function with compact support is bounded above. "-/]
-lemma continuous.bdd_above_range_of_has_compact_mul_support [has_one α]
-  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
-  bdd_above (range f) :=
-@continuous.bdd_below_range_of_has_compact_mul_support αᵒᵈ _ _ _ _ _ _ _ _ hf h
-
 end linear_order
 
 end order_closed_topology
diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean
index 36f63e1120bbb..97d583e2dacd9 100644
--- a/src/topology/subset_properties.lean
+++ b/src/topology/subset_properties.lean
@@ -230,6 +230,19 @@ lemma is_compact.disjoint_nhds_set_right {l : filter α} (hs : is_compact s) :
   disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, disjoint l (𝓝 x) :=
 by simpa only [disjoint.comm] using hs.disjoint_nhds_set_left
 
+/-- For every directed family of closed sets whose intersection avoids a compact set,
+there exists a single element of the family which itself avoids this compact set. -/
+lemma is_compact.elim_directed_family_closed {ι : Type v} [hι : nonempty ι] (hs : is_compact s)
+  (Z : ι → set α) (hZc : ∀ i, is_closed (Z i)) (hsZ : s ∩ (⋂ i, Z i) = ∅) (hdZ : directed (⊇) Z) :
+  ∃ i : ι, s ∩ Z i = ∅ :=
+let ⟨t, ht⟩ := hs.elim_directed_cover (compl ∘ Z) (λ i, (hZc i).is_open_compl)
+  (by simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_Union,
+    exists_prop, mem_inter_iff, not_and, iff_self, mem_Inter, mem_compl_iff] using hsZ)
+  (hdZ.mono_comp _ $ λ _ _, compl_subset_compl.mpr)
+    in
+⟨t, by simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_Union,
+    exists_prop, mem_inter_iff, not_and, iff_self, mem_Inter, mem_compl_iff] using ht⟩
+
 /-- For every family of closed sets whose intersection avoids a compact set,
 there exists a finite subfamily whose intersection avoids this compact set. -/
 lemma is_compact.elim_finite_subfamily_closed {s : set α} {ι : Type v} (hs : is_compact s)
@@ -273,25 +286,16 @@ lemma is_compact.nonempty_Inter_of_directed_nonempty_compact_closed
   (hZn : ∀ i, (Z i).nonempty) (hZc : ∀ i, is_compact (Z i)) (hZcl : ∀ i, is_closed (Z i)) :
   (⋂ i, Z i).nonempty :=
 begin
-  apply hι.elim,
-  intro i₀,
-  let Z' := λ i, Z i ∩ Z i₀,
-  suffices : (⋂ i, Z' i).nonempty,
-  { exact this.mono (Inter_mono $ λ i, inter_subset_left (Z i) (Z i₀)) },
-  rw nonempty_iff_ne_empty,
-  intro H,
-  obtain ⟨t, ht⟩ : ∃ (t : finset ι), ((Z i₀) ∩ ⋂ (i ∈ t), Z' i) = ∅,
-    from (hZc i₀).elim_finite_subfamily_closed Z'
-      (assume i, is_closed.inter (hZcl i) (hZcl i₀)) (by rw [H, inter_empty]),
-  obtain ⟨i₁, hi₁⟩ : ∃ i₁ : ι, Z i₁ ⊆ Z i₀ ∧ ∀ i ∈ t, Z i₁ ⊆ Z' i,
-  { rcases directed.finset_le hZd t with ⟨i, hi⟩,
-    rcases hZd i i₀ with ⟨i₁, hi₁, hi₁₀⟩,
-    use [i₁, hi₁₀],
-    intros j hj,
-    exact subset_inter (subset.trans hi₁ (hi j hj)) hi₁₀ },
-  suffices : ((Z i₀) ∩ ⋂ (i ∈ t), Z' i).nonempty,
-  { rw nonempty_iff_ne_empty at this, contradiction },
-  exact (hZn i₁).mono (subset_inter hi₁.left $ subset_Inter₂ hi₁.right),
+  let i₀ := hι.some,
+  suffices : (Z i₀ ∩ ⋂ i, Z i).nonempty,
+    by rwa inter_eq_right_iff_subset.mpr (Inter_subset _ i₀) at this,
+  simp only [nonempty_iff_ne_empty] at hZn ⊢,
+  apply mt ((hZc i₀).elim_directed_family_closed Z hZcl),
+  push_neg,
+  simp only [← nonempty_iff_ne_empty] at hZn ⊢,
+  refine ⟨hZd, λ i, _⟩,
+  rcases hZd i₀ i with ⟨j, hji₀, hji⟩,
+  exact (hZn j).mono (subset_inter hji₀ hji)
 end
 
 /-- Cantor's intersection theorem for sequences indexed by `ℕ`: