feat: For any b, there exists a set s of independent atoms such t…

…hat `Sup s` is the complement of `b` (#3588)

Match leanprover-community/mathlib#8475

* [`order.compactly_generated`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`e8cf0cfec5fcab9baf46dc17d30c5e22048468be`](https://leanprover-community.github.io/mathlib-port-status/file/order/compactly_generated?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..e8cf0cfec5fcab9baf46dc17d30c5e22048468be)
* [`order.directed`@`485b24ed47b1b7978d38a1e445158c6224c3f42c`..`e8cf0cfec5fcab9baf46dc17d30c5e22048468be`](https://leanprover-community.github.io/mathlib-port-status/file/order/directed?range=485b24ed47b1b7978d38a1e445158c6224c3f42c..e8cf0cfec5fcab9baf46dc17d30c5e22048468be)

Mathlib/Order/CompactlyGenerated.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module order.compactly_generated
-! leanprover-community/mathlib commit 210657c4ea4a4a7b234392f70a3a2a83346dfa90
+! leanprover-community/mathlib commit e8cf0cfec5fcab9baf46dc17d30c5e22048468be
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -55,8 +55,7 @@ This is demonstrated by means of the following four lemmas:
 complete lattice, well-founded, compact
 -/
 
-
-variable {α : Type _} [CompleteLattice α]
+variable {ι : Sort _} {α : Type _} [CompleteLattice α] {f : ι → α}
 
 namespace CompleteLattice
 
@@ -368,7 +367,7 @@ theorem le_iff_compact_le_imp {a b : α} :
 #align le_iff_compact_le_imp le_iff_compact_le_imp
 
 /-- This property is sometimes referred to as `α` being upper continuous. -/
-theorem inf_supₛ_eq_of_directedOn (h : DirectedOn (· ≤ ·) s) : a ⊓ supₛ s = ⨆ b ∈ s, a ⊓ b :=
+theorem DirectedOn.inf_supₛ_eq (h : DirectedOn (· ≤ ·) s) : a ⊓ supₛ s = ⨆ b ∈ s, a ⊓ b :=
   le_antisymm
     (by
       rw [le_iff_compact_le_imp]
@@ -382,7 +381,40 @@ theorem inf_supₛ_eq_of_directedOn (h : DirectedOn (· ≤ ·) s) : a ⊓ sup
       · rw [Set.not_nonempty_iff_eq_empty] at hs
         simp [hs])
     supᵢ_inf_le_inf_supₛ
-#align inf_Sup_eq_of_directed_on inf_supₛ_eq_of_directedOn
+#align directed_on.inf_Sup_eq DirectedOn.inf_supₛ_eq
+
+/-- This property is sometimes referred to as `α` being upper continuous. -/
+protected theorem DirectedOn.supₛ_inf_eq (h : DirectedOn (· ≤ ·) s) : supₛ s ⊓ a = ⨆ b ∈ s, b ⊓ a :=
+  by simp_rw [@inf_comm _ _ _ a, h.inf_supₛ_eq]
+#align directed_on.Sup_inf_eq DirectedOn.supₛ_inf_eq
+
+protected theorem Directed.inf_supᵢ_eq (h : Directed (· ≤ ·) f) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i :=
+  by rw [supᵢ, h.directedOn_range.inf_supₛ_eq, supᵢ_range]
+#align directed.inf_supr_eq Directed.inf_supᵢ_eq
+
+protected theorem Directed.supᵢ_inf_eq (h : Directed (· ≤ ·) f) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a :=
+  by rw [supᵢ, h.directedOn_range.supₛ_inf_eq, supᵢ_range]
+#align directed.supr_inf_eq Directed.supᵢ_inf_eq
+
+protected theorem DirectedOn.disjoint_supₛ_right (h : DirectedOn (· ≤ ·) s) :
+    Disjoint a (supₛ s) ↔ ∀ ⦃b⦄, b ∈ s → Disjoint a b := by
+  simp_rw [disjoint_iff, h.inf_supₛ_eq, supᵢ_eq_bot]
+#align directed_on.disjoint_Sup_right DirectedOn.disjoint_supₛ_right
+
+protected theorem DirectedOn.disjoint_supₛ_left (h : DirectedOn (· ≤ ·) s) :
+    Disjoint (supₛ s) a ↔ ∀ ⦃b⦄, b ∈ s → Disjoint b a := by
+  simp_rw [disjoint_iff, h.supₛ_inf_eq, supᵢ_eq_bot]
+#align directed_on.disjoint_Sup_left DirectedOn.disjoint_supₛ_left
+
+protected theorem Directed.disjoint_supᵢ_right (h : Directed (· ≤ ·) f) :
+    Disjoint a (⨆ i, f i) ↔ ∀ i, Disjoint a (f i) := by
+  simp_rw [disjoint_iff, h.inf_supᵢ_eq, supᵢ_eq_bot]
+#align directed.disjoint_supr_right Directed.disjoint_supᵢ_right
+
+protected theorem Directed.disjoint_supᵢ_left (h : Directed (· ≤ ·) f) :
+    Disjoint (⨆ i, f i) a ↔ ∀ i, Disjoint (f i) a := by
+  simp_rw [disjoint_iff, h.supᵢ_inf_eq, supᵢ_eq_bot]
+#align directed.disjoint_supr_left Directed.disjoint_supᵢ_left
 
 /-- This property is equivalent to `α` being upper continuous. -/
 theorem inf_supₛ_eq_supᵢ_inf_sup_finset :
@@ -501,7 +533,7 @@ instance (priority := 100) isAtomic_of_complementedLattice [ComplementedLattice
       exact ⟨a, ha.of_isAtom_coe_Iic, hac.trans hcb⟩⟩
 #align is_atomic_of_complemented_lattice isAtomic_of_complementedLattice
 
-/-- See Lemma 5.1, Călugăreanu -/
+/-- See [Lemma 5.1][calugareanu]. -/
 instance (priority := 100) isAtomistic_of_complementedLattice [ComplementedLattice α] :
     IsAtomistic α :=
   ⟨fun b =>
@@ -520,70 +552,83 @@ instance (priority := 100) isAtomistic_of_complementedLattice [ComplementedLatti
         exact le_supₛ ⟨ha.of_isAtom_coe_Iic, a.2⟩, fun _ => And.left⟩⟩
 #align is_atomistic_of_complemented_lattice isAtomistic_of_complementedLattice
 
-/-- See Theorem 6.6, Călugăreanu -/
+/-!
+Now we will prove that a compactly generated modular atomistic lattice is a complemented lattice.
+Most explicitly, every element is the complement of a supremum of indepedendent atoms.
+-/
+
+/-- In an atomic lattice, every element `b` has a complement of the form `Sup s`, where each element
+of `s` is an atom. See also `complemented_lattice_of_Sup_atoms_eq_top`. -/
+theorem exists_setIndependent_isCompl_supₛ_atoms (h : supₛ { a : α | IsAtom a } = ⊤) (b : α) :
+    ∃ s : Set α, CompleteLattice.SetIndependent s ∧ IsCompl b (supₛ s) ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a :=
+  by
+  -- porting note: `obtain` chokes on the placeholder.
+  have := zorn_subset
+    {s : Set α | CompleteLattice.SetIndependent s ∧ Disjoint b (supₛ s) ∧ ∀ a ∈ s, IsAtom a}
+    fun c hc1 hc2 =>
+      ⟨⋃₀ c,
+        ⟨CompleteLattice.independent_unionₛ_of_directed hc2.directedOn fun s hs => (hc1 hs).1, ?_,
+          fun a ⟨s, sc, as⟩ => (hc1 sc).2.2 a as⟩,
+        fun _ => Set.subset_unionₛ_of_mem⟩
+  obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := this
+  swap
+  · rw [supₛ_unionₛ, ← supₛ_image, DirectedOn.disjoint_supₛ_right]
+    · rintro _ ⟨s, hs, rfl⟩
+      exact (hc1 hs).2.1
+    · rw [directedOn_image]
+      exact hc2.directedOn.mono @fun s t => supₛ_le_supₛ
+  refine' ⟨s, s_ind, ⟨b_inf_Sup_s, _⟩, s_atoms⟩
+  rw [codisjoint_iff_le_sup, ← h, supₛ_le_iff]
+  intro a ha
+  rw [← inf_eq_left]
+  refine' (ha.le_iff.mp inf_le_left).resolve_left fun con => ha.1 _
+  rw [← con, eq_comm, inf_eq_left]
+  refine' (le_supₛ _).trans le_sup_right
+  rw [← disjoint_iff] at con
+  have a_dis_Sup_s : Disjoint a (supₛ s) := con.mono_right le_sup_right
+  -- porting note: The two following `fun x hx => _` are no-op
+  rw [← s_max (s ∪ {a}) ⟨fun x hx => _, _, fun x hx => _⟩ (Set.subset_union_left _ _)]
+  · exact Set.mem_union_right _ (Set.mem_singleton _)
+  · intro x hx
+    rw [Set.mem_union, Set.mem_singleton_iff] at hx
+    obtain rfl | xa := eq_or_ne x a
+    · simp only [Set.mem_singleton, Set.insert_diff_of_mem, Set.union_singleton]
+      exact con.mono_right ((supₛ_le_supₛ <| Set.diff_subset _ _).trans le_sup_right)
+    · have h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a} :=
+        by
+        simp only [Set.union_singleton]
+        rw [Set.insert_diff_of_not_mem]
+        rw [Set.mem_singleton_iff]
+        exact Ne.symm xa
+      rw [h, supₛ_union, supₛ_singleton]
+      apply
+        (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
+          (a_dis_Sup_s.mono_right _).symm
+      rw [← supₛ_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]
+  · rw [supₛ_union, supₛ_singleton]
+    exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm
+  · intro x hx
+    rw [Set.mem_union, Set.mem_singleton_iff] at hx
+    obtain hx | rfl := hx
+    · exact s_atoms x hx
+    · exact ha
+#align exists_set_independent_is_compl_Sup_atoms exists_setIndependent_isCompl_supₛ_atoms
+
+theorem exists_setIndependent_of_supₛ_atoms_eq_top (h : supₛ { a : α | IsAtom a } = ⊤) :
+    ∃ s : Set α, CompleteLattice.SetIndependent s ∧ supₛ s = ⊤ ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a :=
+  let ⟨s, s_ind, s_top, s_atoms⟩ := exists_setIndependent_isCompl_supₛ_atoms h ⊥
+  ⟨s, s_ind, eq_top_of_isCompl_bot s_top.symm, s_atoms⟩
+#align exists_set_independent_of_Sup_atoms_eq_top exists_setIndependent_of_supₛ_atoms_eq_top
+
+/-- See [Theorem 6.6][calugareanu]. -/
 theorem complementedLattice_of_supₛ_atoms_eq_top (h : supₛ { a : α | IsAtom a } = ⊤) :
     ComplementedLattice α :=
-  ⟨fun b => by
-    have H : ?_ := ?_ -- Porting note: this is an ugly hack, but `?H` on the next line fails
-    obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ :=
-      zorn_subset
-        { s : Set α | CompleteLattice.SetIndependent s ∧ b ⊓ supₛ s = ⊥ ∧ ∀ a ∈ s, IsAtom a } H
-    · refine'
-        ⟨supₛ s, disjoint_iff.mpr b_inf_Sup_s,
-          codisjoint_iff_le_sup.mpr <| h.symm.trans_le <| supₛ_le_iff.2 fun a ha => _⟩
-      rw [← inf_eq_left]
-      refine' (ha.le_iff.mp inf_le_left).resolve_left fun con => ha.1 _
-      rw [eq_bot_iff, ← con]
-      refine' le_inf (le_refl a) ((le_supₛ _).trans le_sup_right)
-      rw [← disjoint_iff] at *
-      have a_dis_Sup_s : Disjoint a (supₛ s) := con.mono_right le_sup_right
-      rw [← s_max (s ∪ {a}) ⟨_, ⟨_, _⟩⟩ (Set.subset_union_left _ _)]
-      · exact Set.mem_union_right _ (Set.mem_singleton _)
-      · intro x hx
-        rw [Set.mem_union, Set.mem_singleton_iff] at hx
-        by_cases xa : x = a
-        · simp only [xa, Set.mem_singleton, Set.insert_diff_of_mem, Set.union_singleton]
-          exact con.mono_right (le_trans (supₛ_le_supₛ (Set.diff_subset s {a})) le_sup_right)
-        · have h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a} :=
-            by
-            simp only [Set.union_singleton]
-            rw [Set.insert_diff_of_not_mem]
-            rw [Set.mem_singleton_iff]
-            exact Ne.symm xa
-          rw [h, supₛ_union, supₛ_singleton]
-          apply
-            (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
-              (a_dis_Sup_s.mono_right _).symm
-          rw [← supₛ_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]
-      · rw [supₛ_union, supₛ_singleton, ← disjoint_iff]
-        exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm
-      · intro x hx
-        rw [Set.mem_union, Set.mem_singleton_iff] at hx
-        cases' hx with hx hx
-        · exact s_atoms x hx
-        · rw [hx]
-          exact ha
-    · intro c hc1 hc2
-      refine'
-        ⟨⋃₀ c,
-          ⟨CompleteLattice.independent_unionₛ_of_directed hc2.directedOn fun s hs => (hc1 hs).1, _,
-            fun a ha => _⟩,
-          fun _ => Set.subset_unionₛ_of_mem⟩
-      · rw [supₛ_unionₛ, ← supₛ_image, inf_supₛ_eq_of_directedOn, supᵢ_eq_bot]
-        · intro i
-          rw [supᵢ_eq_bot]
-          intro hi
-          obtain ⟨x, xc, rfl⟩ := (Set.mem_image _ _ _).1 hi
-          exact (hc1 xc).2.1
-        · rw [directedOn_image]
-          refine' hc2.directedOn.mono _
-          intro s t
-          apply supₛ_le_supₛ
-      · rcases Set.mem_unionₛ.1 ha with ⟨s, sc, as⟩
-        exact (hc1 sc).2.2 a as⟩
+  ⟨fun b =>
+    let ⟨s, _, s_top, _⟩ := exists_setIndependent_isCompl_supₛ_atoms h b
+    ⟨supₛ s, s_top⟩⟩
 #align complemented_lattice_of_Sup_atoms_eq_top complementedLattice_of_supₛ_atoms_eq_top
 
-/-- See Theorem 6.6, Călugăreanu -/
+/-- See [Theorem 6.6][calugareanu]. -/
 theorem complementedLattice_of_isAtomistic [IsAtomistic α] : ComplementedLattice α :=
   complementedLattice_of_supₛ_atoms_eq_top supₛ_atoms_eq_top
 #align complemented_lattice_of_is_atomistic complementedLattice_of_isAtomistic

Mathlib/Order/Directed.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module order.directed
-! leanprover-community/mathlib commit 485b24ed47b1b7978d38a1e445158c6224c3f42c
+! leanprover-community/mathlib commit e8cf0cfec5fcab9baf46dc17d30c5e22048468be
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -63,10 +63,17 @@ theorem directedOn_iff_directed {s} : @DirectedOn α r s ↔ Directed r (Subtype
 alias directedOn_iff_directed ↔ DirectedOn.directed_val _
 #align directed_on.directed_coe DirectedOn.directed_val
 
-theorem directedOn_range {f : β → α} : Directed r f ↔ DirectedOn r (Set.range f) := by
+theorem directedOn_range {f : ι → α} : Directed r f ↔ DirectedOn r (Set.range f) := by
   simp_rw [Directed, DirectedOn, Set.forall_range_iff, Set.exists_range_iff]
 #align directed_on_range directedOn_range
 
+-- porting note: This alias was misplaced in `order/compactly_generated.lean` in mathlib3
+alias directedOn_range ↔ Directed.directedOn_range _
+#align directed.directed_on_range Directed.directedOn_range
+
+-- porting note: `attribute [protected]` doesn't work
+-- attribute [protected] Directed.directedOn_range
+
 theorem directedOn_image {s : Set β} {f : β → α} :
     DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s := by
   simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,