-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem exists_sSupIndep_isCompl_sSup_atoms (h : sSup { a : α | IsAtom a } = ⊤) (b : α) :
    ∃ s : Set α, sSupIndep s ∧
    IsCompl b (sSup s) ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a

Proof state:
case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ Disjoint x (sSup (s \ {x}) ⊔ a)

Tactic:
apply
  (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
    (a_dis_Sup_s.mono_right _).symm

Result:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ x ⊔ sSup (s \ {x}) ≤ sSup s

Proof state:
case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
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

Result:
case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Proof state:
case refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
zorn : ∃ m, Maximal (fun x => x ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}) m
⊢ ∃ s, sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}
hc2 : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ Disjoint b (sSup (⋃₀ c))

Tactic:
swap

Result:
case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}
hc2 : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ Disjoint b (sSup (⋃₀ c))

case refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
zorn : ∃ m, Maximal (fun x => x ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}) m
⊢ ∃ s, sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ⊓ (b ⊔ sSup s) = a

Tactic:
refine (ha.le_iff.mp inf_le_left).resolve_left fun con => ha.1 ?_

Result:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a = ⊥

Proof state:
case refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
zorn :
  ∃ m ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a},
    ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → m ⊆ t → m = t
⊢ ∃ s, sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn

Result:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
⊢ ∃ s, sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ∈ s

Tactic:
rw [← disjoint_iff] at con

Result:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
⊢ a ∈ s

Proof state:
case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}
hc2 : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ Disjoint b (sSup (⋃₀ c))

Tactic:
rw [sSup_sUnion, ← sSup_image, DirectedOn.disjoint_sSup_right]

Result:
case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}
hc2 : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ sSup '' c → Disjoint b b_1

case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}
hc2 : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ DirectedOn (fun x1 x2 => x1 ≤ x2) (sSup '' c)