refactor: generalise compact from CompleteLattice to PartialOrder (leanprover-community#33061)

`IsCompactElement` assumes a `CompleteLattice` structure on the type for which it is defined. But a `PartialOrder` will suffice and this is the textbook definition of compact https://en.wikipedia.org/wiki/Compact_element.
Also it is currently defined in a non-standard way. The standard definition uses directed sets. Changing this has
indeed simplified most proofs by removing an `rw` into this more standard form.

Co-authored-by: Edwin Fernando <ef322@ic.ac.uk>

Author: edwin1729

Mathlib/Algebra/Lie/Submodule.lean

@@ -670,7 +670,7 @@ theorem lieSpan_induction {p : (x : M) → x ∈ lieSpan R L s → Prop}
   exact lieSpan_le (N := p) |>.mpr (fun y hy ↦ ⟨subset_lieSpan hy, mem y hy⟩) hx |>.elim fun _ ↦ id
 
 lemma isCompactElement_lieSpan_singleton (m : M) :
-    CompleteLattice.IsCompactElement (lieSpan R L {m}) := by
+    IsCompactElement (lieSpan R L {m}) := by
   rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]
   intro s hne hdir hsup
   replace hsup : m ∈ (↑(sSup s) : Set M) := (SetLike.le_def.mp hsup) (subset_lieSpan rfl)

Mathlib/LinearAlgebra/Span/Basic.lean

@@ -322,7 +322,7 @@ theorem iSup_induction' {ι : Sort*} (p : ι → Submodule R M) {motive : ∀ x,
     exact ⟨_, add _ _ _ _ Cx Cy⟩
 
 theorem singleton_span_isCompactElement (x : M) :
-    CompleteLattice.IsCompactElement (span R {x} : Submodule R M) := by
+    IsCompactElement (span R {x} : Submodule R M) := by
   rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]
   intro d hemp hdir hsup
   have : x ∈ (sSup d) := (SetLike.le_def.mp hsup) (mem_span_singleton_self x)
@@ -331,7 +331,7 @@ theorem singleton_span_isCompactElement (x : M) :
 
 /-- The span of a finite subset is compact in the lattice of submodules. -/
 theorem finset_span_isCompactElement (S : Finset M) :
-    CompleteLattice.IsCompactElement (span R S : Submodule R M) := by
+    IsCompactElement (span R S : Submodule R M) := by
   rw [span_eq_iSup_of_singleton_spans]
   simp only [Finset.mem_coe]
   rw [← Finset.sup_eq_iSup]
@@ -340,7 +340,7 @@ theorem finset_span_isCompactElement (S : Finset M) :
 
 /-- The span of a finite subset is compact in the lattice of submodules. -/
 theorem finite_span_isCompactElement (S : Set M) (h : S.Finite) :
-    CompleteLattice.IsCompactElement (span R S : Submodule R M) :=
+    IsCompactElement (span R S : Submodule R M) :=
   Finite.coe_toFinset h ▸ finset_span_isCompactElement h.toFinset
 
 instance : IsCompactlyGenerated (Submodule R M) :=

Mathlib/Order/BooleanGenerators.lean

@@ -77,7 +77,7 @@ lemma atomistic (hS : BooleanGenerators S) (a : α) (ha : a ≤ sSup S) : ∃ T
   obtain ⟨C, hC, rfl⟩ := IsCompactlyGenerated.exists_sSup_eq a
   have aux : ∀ b : α, IsCompactElement b → b ≤ sSup S → ∃ T ⊆ S, b = sSup T := by
     intro b hb hbS
-    obtain ⟨s, hs₁, hs₂⟩ := hb S hbS
+    obtain ⟨s, hs₁, hs₂⟩ := (isCompactElement_iff_exists_le_sSup_of_le_sSup α b).1 hb S hbS
     obtain ⟨t, ht, rfl⟩ := hS.finitelyAtomistic s b hs₁ hb hs₂
     refine ⟨t, ?_, Finset.sup_id_eq_sSup t⟩
     refine Set.Subset.trans ?_ hs₁

Mathlib/Order/CompactlyGenerated/Basic.lean

@@ -26,15 +26,15 @@ proofs that they are indeed equivalent to well-foundedness.
 ## Main definitions
 * `CompleteLattice.IsSupClosedCompact`
 * `CompleteLattice.IsSupFiniteCompact`
-* `CompleteLattice.IsCompactElement`
+* `IsCompactElement`
 * `IsCompactlyGenerated`
 
 ## Main results
 The main result is that the following four conditions are equivalent for a complete lattice:
 * `well_founded (>)`
 * `CompleteLattice.IsSupClosedCompact`
 * `CompleteLattice.IsSupFiniteCompact`
-* `∀ k, CompleteLattice.IsCompactElement k`
+* `∀ k, IsCompactElement k`
 
 This is demonstrated by means of the following four lemmas:
 * `CompleteLattice.WellFounded.isSupFiniteCompact`
@@ -56,6 +56,16 @@ complete lattice, well-founded, compact
 @[expose] public section
 
 open Set
+/-- An element `k` is compact if any directed set with `LUB` (least upper bound) above
+`k` has already got above `k` at some point in the set.
+Such an element is also called "finite" or "S-compact". -/
+def IsCompactElement {α : Type*} [PartialOrder α] (k : α) :=
+  ∀ (s : Set α) (u : α),
+    s.Nonempty →
+    DirectedOn (· ≤ ·) s →
+    IsLUB s u →
+    k ≤ u →
+    ∃ x ∈ s, k ≤ x
 
 variable {ι : Sort*} {α : Type*} [CompleteLattice α] {f : ι → α}
 
@@ -73,49 +83,26 @@ same `sSup`. -/
 def IsSupFiniteCompact : Prop :=
   ∀ s : Set α, ∃ t : Finset α, ↑t ⊆ s ∧ sSup s = t.sup id
 
-/-- An element `k` of a complete lattice is said to be compact if any set with `sSup`
-above `k` has a finite subset with `sSup` above `k`.  Such an element is also called
-"finite" or "S-compact". -/
-def IsCompactElement {α : Type*} [CompleteLattice α] (k : α) :=
-  ∀ s : Set α, k ≤ sSup s → ∃ t : Finset α, ↑t ⊆ s ∧ k ≤ t.sup id
-
-theorem isCompactElement_iff.{u} {α : Type u} [CompleteLattice α] (k : α) :
-    CompleteLattice.IsCompactElement k ↔
-      ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t : Finset ι, k ≤ t.sup s := by
-  classical
-    constructor
-    · intro H ι s hs
-      obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
-      have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
-      choose f hf using this
-      refine ⟨Finset.univ.image f, ht'.trans ?_⟩
-      rw [Finset.sup_le_iff]
-      intro b hb
-      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
-      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
-    · intro H s hs
-      obtain ⟨t, ht⟩ :=
-        H s Subtype.val
-          (by
-            delta iSup
-            rwa [Subtype.range_coe])
-      refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
-      rw [Finset.sup_le_iff]
-      exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)
-
 /-- An element `k` is compact if and only if any directed set with `sSup` above
 `k` already got above `k` at some point in the set. -/
 theorem isCompactElement_iff_le_of_directed_sSup_le (k : α) :
     IsCompactElement k ↔
       ∀ s : Set α, s.Nonempty → DirectedOn (· ≤ ·) s → k ≤ sSup s → ∃ x : α, x ∈ s ∧ k ≤ x := by
+  constructor
+  · intro hk s hs hs' h_le
+    exact hk s (sSup s) hs hs' (isLUB_sSup s) h_le
+  · intro h s u hs hs' hu h_le
+    rw [isLUB_iff_sSup_eq] at hu
+    rw [← hu] at h_le
+    exact h s hs hs' h_le
+
+/-- An element `k` of is compact if any set with `sSup`
+above `k` has a finite subset with `sSup` above `k`. -/
+theorem isCompactElement_iff_exists_le_sSup_of_le_sSup (k : α) :
+    IsCompactElement k ↔ ∀ s : Set α, k ≤ sSup s → ∃ t : Finset α, ↑t ⊆ s ∧ k ≤ t.sup id := by
   classical
+    rw [isCompactElement_iff_le_of_directed_sSup_le]
     constructor
-    · intro hk s hne hdir hsup
-      obtain ⟨t, ht⟩ := hk s hsup
-      -- certainly every element of t is below something in s, since ↑t ⊆ s.
-      have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
-      obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
-      exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩
     · intro hk s hsup
       -- Consider the set of finite joins of elements of the (plain) set s.
       let S : Set α := { x | ∃ t : Finset α, ↑t ⊆ s ∧ x = t.sup id }
@@ -145,10 +132,42 @@ theorem isCompactElement_iff_le_of_directed_sSup_le (k : α) :
       obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
       use t
       exact ⟨htS, by rwa [← htsup]⟩
+    · intro hk s hne hdir hsup
+      obtain ⟨t, ht⟩ := hk s hsup
+      -- certainly every element of t is below something in s, since ↑t ⊆ s.
+      have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
+      obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
+      exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩
+
+theorem isCompactElement_iff_exists_le_iSup_of_le_iSup.{u} {α : Type u} [CompleteLattice α]
+    (k : α) : IsCompactElement k ↔
+      ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t : Finset ι, k ≤ t.sup s := by
+  classical
+    rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]
+    constructor
+    · intro H ι s hs
+      obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
+      have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
+      choose f hf using this
+      refine ⟨Finset.univ.image f, ht'.trans ?_⟩
+      rw [Finset.sup_le_iff]
+      intro b hb
+      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
+      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
+    · intro H s hs
+      obtain ⟨t, ht⟩ :=
+        H s Subtype.val
+          (by
+            delta iSup
+            rwa [Subtype.range_coe])
+      refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
+      rw [Finset.sup_le_iff]
+      exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)
 
 theorem IsCompactElement.exists_finset_of_le_iSup {k : α} (hk : IsCompactElement k) {ι : Type*}
     (f : ι → α) (h : k ≤ ⨆ i, f i) : ∃ s : Finset ι, k ≤ ⨆ i ∈ s, f i := by
   classical
+    rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
     let g : Finset ι → α := fun s => ⨆ i ∈ s, f i
     have h1 : DirectedOn (· ≤ ·) (Set.range g) := by
       rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
@@ -160,9 +179,7 @@ theorem IsCompactElement.exists_finset_of_le_iSup {k : α} (hk : IsCompactElemen
         (iSup_le fun i =>
           le_sSup_of_le ⟨{i}, rfl⟩
             (le_iSup_of_le i (le_iSup_of_le (Finset.mem_singleton_self i) le_rfl)))
-    obtain ⟨-, ⟨s, rfl⟩, hs⟩ :=
-      (isCompactElement_iff_le_of_directed_sSup_le α k).mp hk (Set.range g) (Set.range_nonempty g)
-        h1 h2
+    obtain ⟨-, ⟨s, rfl⟩, hs⟩ := hk (Set.range g) (Set.range_nonempty g) h1 h2
     exact ⟨s, hs⟩
 
 /-- A compact element `k` has the property that any directed set lying strictly below `k` has
@@ -181,15 +198,14 @@ theorem IsCompactElement.directed_sSup_lt_of_lt {α : Type*} [CompleteLattice α
 theorem isCompactElement_finsetSup {α β : Type*} [CompleteLattice α] {f : β → α} (s : Finset β)
     (h : ∀ x ∈ s, IsCompactElement (f x)) : IsCompactElement (s.sup f) := by
   classical
-    rw [isCompactElement_iff_le_of_directed_sSup_le]
+    simp_rw [isCompactElement_iff_le_of_directed_sSup_le] at ⊢ h
     intro d hemp hdir hsup
     rw [← Function.id_comp f]
     rw [← Finset.sup_image]
     apply Finset.sup_le_of_le_directed d hemp hdir
     rintro x hx
     obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
     specialize h p hps
-    rw [isCompactElement_iff_le_of_directed_sSup_le] at h
     specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
     simpa only [exists_prop]
 
@@ -239,6 +255,7 @@ theorem IsSupClosedCompact.wellFoundedGT (h : IsSupClosedCompact α) :
 
 theorem isSupFiniteCompact_iff_all_elements_compact :
     IsSupFiniteCompact α ↔ ∀ k : α, IsCompactElement k := by
+  simp_rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]
   refine ⟨fun h k s hs => ?_, fun h s => ?_⟩
   · obtain ⟨t, ⟨hts, htsup⟩⟩ := h s
     use t, hts
@@ -334,25 +351,25 @@ element is the `sSup` of compact elements. -/
 class IsCompactlyGenerated (α : Type*) [CompleteLattice α] : Prop where
   /-- In a compactly generated complete lattice,
   every element is the `sSup` of some set of compact elements. -/
-  exists_sSup_eq : ∀ x : α, ∃ s : Set α, (∀ x ∈ s, CompleteLattice.IsCompactElement x) ∧ sSup s = x
+  exists_sSup_eq : ∀ x : α, ∃ s : Set α, (∀ x ∈ s, IsCompactElement x) ∧ sSup s = x
 
 section
 
 variable [IsCompactlyGenerated α] {a : α} {s : Set α}
 
 @[simp]
 theorem sSup_compact_le_eq (b) :
-    sSup { c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b } = b := by
+    sSup { c : α | IsCompactElement c ∧ c ≤ b } = b := by
   rcases IsCompactlyGenerated.exists_sSup_eq b with ⟨s, hs, rfl⟩
   exact le_antisymm (sSup_le fun c hc => hc.2) (sSup_le_sSup fun c cs => ⟨hs c cs, le_sSup cs⟩)
 
 @[simp]
-theorem sSup_compact_eq_top : sSup { a : α | CompleteLattice.IsCompactElement a } = ⊤ := by
+theorem sSup_compact_eq_top : sSup { a : α | IsCompactElement a } = ⊤ := by
   refine Eq.trans (congr rfl (Set.ext fun x => ?_)) (sSup_compact_le_eq ⊤)
   exact (and_iff_left le_top).symm
 
 theorem le_iff_compact_le_imp {a b : α} :
-    a ≤ b ↔ ∀ c : α, CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b :=
+    a ≤ b ↔ ∀ c : α, IsCompactElement c → c ≤ a → c ≤ b :=
   ⟨fun ab _ _ ca => le_trans ca ab, fun h => by
     rw [← sSup_compact_le_eq a, ← sSup_compact_le_eq b]
     exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩⟩
@@ -364,8 +381,8 @@ theorem DirectedOn.inf_sSup_eq (h : DirectedOn (· ≤ ·) s) : a ⊓ sSup s = 
       rw [le_iff_compact_le_imp]
       by_cases hs : s.Nonempty
       · intro c hc hcinf
-        rw [le_inf_iff] at hcinf
         rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc
+        rw [le_inf_iff] at hcinf
         rcases hc s hs h hcinf.2 with ⟨d, ds, cd⟩
         refine (le_inf hcinf.1 cd).trans (le_trans ?_ (le_iSup₂ d ds))
         rfl
@@ -409,6 +426,7 @@ theorem inf_sSup_eq_iSup_inf_sup_finset :
     (by
       rw [le_iff_compact_le_imp]
       intro c hc hcinf
+      rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at hc
       rw [le_inf_iff] at hcinf
       rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩
       refine (le_inf hcinf.1 ht2).trans (le_trans ?_ (le_iSup₂ t ht1))
@@ -498,7 +516,7 @@ theorem Iic_coatomic_of_compact_element {k : α} (h : IsCompactElement k) :
     exact lt_irrefl _ hck
   · intro S SC cC I _
     by_cases hS : S.Nonempty
-    · refine ⟨sSup S, h.directed_sSup_lt_of_lt hS cC.directedOn SC, ?_⟩
+    · refine ⟨sSup S, IsCompactElement.directed_sSup_lt_of_lt h hS cC.directedOn SC, ?_⟩
       intro; apply le_sSup
     exact
       ⟨b, lt_of_le_of_ne hbk H, by
@@ -538,7 +556,7 @@ theorem iSupIndep.iInf {ι : Type*} {κ : ι → Type*} (f : (i : ι) → κ i 
 
 instance (priority := 100) isAtomic_of_complementedLattice [ComplementedLattice α] : IsAtomic α :=
   ⟨fun b => by
-    by_cases h : { c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b } ⊆ {⊥}
+    by_cases h : { c : α | IsCompactElement c ∧ c ≤ b } ⊆ {⊥}
     · left
       rw [← sSup_compact_le_eq b, sSup_eq_bot]
       exact h

Mathlib/Order/CompactlyGenerated/Intervals.lean

@@ -18,9 +18,10 @@ variable {ι α : Type*} [CompleteLattice α]
 
 namespace Set.Iic
 
-theorem isCompactElement {a : α} {b : Iic a} (h : CompleteLattice.IsCompactElement (b : α)) :
-    CompleteLattice.IsCompactElement b := by
-  simp only [CompleteLattice.isCompactElement_iff, Finset.sup_eq_iSup] at h ⊢
+theorem isCompactElement {a : α} {b : Iic a} (h : IsCompactElement (b : α)) :
+    IsCompactElement b := by
+  simp only [CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup,
+    Finset.sup_eq_iSup] at h ⊢
   intro ι s hb
   replace hb : (b : α) ≤ iSup ((↑) ∘ s) := le_trans hb <| (coe_iSup s) ▸ le_refl _
   obtain ⟨t, ht⟩ := h ι ((↑) ∘ s) hb

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -178,7 +178,7 @@ theorem FG.stabilizes_of_iSup_eq {M' : Submodule R M} (hM' : M'.FG) (N : ℕ →
     exact le_iSup _ _
 
 /-- Finitely generated submodules are precisely compact elements in the submodule lattice. -/
-theorem fg_iff_compact (s : Submodule R M) : s.FG ↔ CompleteLattice.IsCompactElement s := by
+theorem fg_iff_compact (s : Submodule R M) : s.FG ↔ IsCompactElement s := by
   classical
     -- Introduce shorthand for span of an element
     let sp : M → Submodule R M := fun a => span R {a}
@@ -190,6 +190,7 @@ theorem fg_iff_compact (s : Submodule R M) : s.FG ↔ CompleteLattice.IsCompactE
       apply CompleteLattice.isCompactElement_finsetSup
       exact fun n _ => singleton_span_isCompactElement n
     · intro h
+      rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at h
       -- s is the Sup of the spans of its elements.
       have sSup' : s = sSup (sp '' ↑s) := by
         rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]

Mathlib/RingTheory/Ideal/Span.lean

@@ -90,7 +90,7 @@ theorem span_eq : span (I : Set α) = I :=
 theorem span_singleton_one : span ({1} : Set α) = ⊤ :=
   (eq_top_iff_one _).2 <| subset_span <| mem_singleton _
 
-theorem isCompactElement_top : CompleteLattice.IsCompactElement (⊤ : Ideal α) := by
+theorem isCompactElement_top : IsCompactElement (⊤ : Ideal α) := by
   simpa only [← span_singleton_one] using Submodule.singleton_span_isCompactElement 1
 
 theorem mem_span_insert {s : Set α} {x y} :

Mathlib/RingTheory/Spectrum/Prime/Topology.lean

@@ -286,7 +286,8 @@ instance compactSpace : CompactSpace (PrimeSpectrum R) := by
   refine compactSpace_of_finite_subfamily_closed fun S S_closed S_empty ↦ ?_
   choose I hI using fun i ↦ (isClosed_iff_zeroLocus_ideal (S i)).mp (S_closed i)
   simp_rw [hI, ← zeroLocus_iSup, zeroLocus_empty_iff_eq_top, ← top_le_iff] at S_empty ⊢
-  exact Ideal.isCompactElement_top.exists_finset_of_le_iSup _ _ S_empty
+  exact CompleteLattice.IsCompactElement.exists_finset_of_le_iSup _
+    Ideal.isCompactElement_top _ S_empty
 
 /-- The prime spectrum of a commutative semiring has discrete Zariski topology iff it is finite and
 the semiring has Krull dimension zero or is trivial. -/

Mathlib/Topology/Sets/Opens.lean

@@ -350,8 +350,8 @@ lemma IsBasis.of_isInducing {B : Set (Opens β)} (H : IsBasis B) {f : α → β}
 
 @[simp]
 theorem isCompactElement_iff (s : Opens α) :
-    CompleteLattice.IsCompactElement s ↔ IsCompact (s : Set α) := by
-  rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff]
+    IsCompactElement s ↔ IsCompact (s : Set α) := by
+  rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup]
   refine ⟨?_, fun H ι U hU => ?_⟩
   · introv H hU hU'
     obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)