case refine_2
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
this :
  ∃ m,
    m ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} ∧
      ∀ (a : Set α),
        a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → m ⊆ a → a = m
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Disjoint b (sSup (⋃₀ c))
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
have := zorn_subset
  {s : Set α | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}
  fun c hc1 hc2 =>
    ⟨⋃₀ c,
      ⟨CompleteLattice.independent_sUnion_of_directed hc2.directedOn fun s hs => (hc1 hs).1, ?_,
        fun a ⟨s, sc, as⟩ => (hc1 sc).2.2 a as⟩,
      fun _ => Set.subset_sUnion_of_mem⟩
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Disjoint b (sSup (⋃₀ c))
case refine_2
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
this :
  ∃ m,
    m ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} ∧
      ∀ (a : Set α),
        a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → m ⊆ a → a = m
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Disjoint b (sSup (⋃₀ c))
obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := this
case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Disjoint b (sSup (⋃₀ c))

case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Disjoint b (sSup (⋃₀ c))
swap
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ Codisjoint b (sSup s)
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
refine' ⟨s, s_ind, ⟨b_inf_Sup_s, _⟩, s_atoms⟩
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ ∀ (b_1 : α), b_1 ∈ {a | IsAtom a} → b_1 ≤ b ⊔ sSup s
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ Codisjoint b (sSup s)
rw [codisjoint_iff_le_sup, ← h, sSup_le_iff]
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ≤ b ⊔ sSup s
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ ∀ (b_1 : α), b_1 ∈ {a | IsAtom a} → b_1 ≤ b ⊔ sSup s
intro a ha
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ⊓ (b ⊔ sSup s) = a
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ≤ b ⊔ sSup s
rw [← inf_eq_left]
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a = ⊥
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ⊓ (b ⊔ sSup s) = a
refine' (ha.le_iff.mp inf_le_left).resolve_left fun con => ha.1 _
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ≤ b ⊔ sSup s
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a = ⊥
rw [← con, eq_comm, inf_eq_left]
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ∈ s
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ≤ b ⊔ sSup s
refine' (le_sSup _).trans le_sup_right
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
⊢ a ∈ s
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ∈ s
rw [← disjoint_iff] at con
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ a ∈ s
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
⊢ a ∈ s
have a_dis_Sup_s : Disjoint a (sSup s) := con.mono_right le_sup_right
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ a ∈ s ∪ {a}

ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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 : α), x ∈ s ∪ {a} → Disjoint x (sSup ((s ∪ {a}) \ {x}))

ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup (s ∪ {a}))

ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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 : α), x ∈ s ∪ {a} → IsAtom x
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ a ∈ s
rw [← s_max (s ∪ {a}) ⟨fun x hx => _, _, fun x hx => _⟩ (Set.subset_union_left _ _)]
case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ (fun t => sSup t) '' c → Disjoint b b_1

case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ DirectedOn (fun x x_1 => x ≤ x_1) ((fun t => sSup t) '' c)
case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Disjoint b (sSup (⋃₀ c))
rw [sSup_sUnion, ← sSup_image, DirectedOn.disjoint_sSup_right]
case refine_1.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hs : s ∈ c
⊢ Disjoint b ((fun t => sSup t) s)
case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ (fun t => sSup t) '' c → Disjoint b b_1
rintro _ ⟨s, hs, rfl⟩
no goals
case refine_1.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hs : s ∈ c
⊢ Disjoint b ((fun t => sSup t) s)
exact (hc1 hs).2.1
case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ DirectedOn ((fun t => sSup t) ⁻¹'o fun x x_1 => x ≤ x_1) c
case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ DirectedOn (fun x x_1 => x ≤ x_1) ((fun t => sSup t) '' c)
rw [directedOn_image]
no goals
case refine_1
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ DirectedOn ((fun t => sSup t) ⁻¹'o fun x x_1 => x ≤ x_1) c
exact hc2.directedOn.mono @fun s t => sSup_le_sSup
no goals
case refine_2.intro.intro.intro.intro
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ a ∈ s ∪ {a}
exact Set.mem_union_right _ (Set.mem_singleton _)
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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 ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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 : α), x ∈ s ∪ {a} → Disjoint x (sSup ((s ∪ {a}) \ {x}))
intro x hx
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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 ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
rw [Set.mem_union, Set.mem_singleton_iff] at hx
case inl
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup ((s ∪ {x}) \ {x}))

case inr
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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}))
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
obtain rfl | xa := eq_or_ne x a
case inl
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup (s \ {x}))
case inl
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup ((s ∪ {x}) \ {x}))
simp only [Set.mem_singleton, Set.insert_diff_of_mem, Set.union_singleton]
no goals
case inl
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup (s \ {x}))
exact con.mono_right ((sSup_le_sSup <| Set.diff_subset _ _).trans le_sup_right)
case inr
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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}))
case inr
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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}))
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
case inr
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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)
case inr
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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}))
rw [h, sSup_union, sSup_singleton]
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
case inr
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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)
apply
  (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
    (a_dis_Sup_s.mono_right _).symm
no goals
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
rw [← sSup_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ insert a s \ {x} = insert a (s \ {x})
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
simp only [Set.union_singleton]
case h
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ ¬a ∈ {x}
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ insert a s \ {x} = insert a (s \ {x})
rw [Set.insert_diff_of_not_mem]
case h
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ ¬a = x
case h
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ ¬a ∈ {x}
rw [Set.mem_singleton_iff]
no goals
case h
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ ¬a = x
exact Ne.symm xa
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup s ⊔ a)
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup (s ∪ {a}))
rw [sSup_union, sSup_singleton]
no goals
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup s ⊔ a)
exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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 ∪ {a}
⊢ IsAtom x
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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 : α), x ∈ s ∪ {a} → IsAtom x
intro x hx
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ IsAtom x
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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 ∪ {a}
⊢ IsAtom x
rw [Set.mem_union, Set.mem_singleton_iff] at hx
case inl
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ IsAtom x

case inr
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
⊢ IsAtom x
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ IsAtom x
obtain hx | rfl := hx
no goals
case inl
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), 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
⊢ IsAtom x
exact s_atoms x hx
no goals
case inr
ι : Sort ?u.122982
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
⊢ IsAtom x
exact ha