awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ a ∈ s ∪ {a}

Tactic:
Set.mem_union_right _ (Set.mem_singleton _)

Premises used: Set.mem_singleton, Set.mem_union_right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ a ∈ s ∪ {a}

Tactic:
exact Set.mem_union_right _ (Set.mem_singleton _)

Premises used: Set.mem_singleton, Set.mem_union_right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
rw : Disjoint b (sSup s ⊔ a)
⊢ Disjoint b (sSup (s ∪ {a}))

Tactic:
rw [sSup_union, sSup_singleton]

Premises used: sSup_union, sSup_singleton
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup s ⊔ a)

Tactic:
b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm

Premises used: Disjoint.symm, Disjoint.disjoint_sup_right_of_disjoint_sup_left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup s ⊔ a)

Tactic:
exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm

Premises used: Disjoint.symm, Disjoint.disjoint_sup_right_of_disjoint_sup_left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ x ∈ s ∨ x = a

Tactic:
rw [Set.mem_union, Set.mem_singleton_iff] at hx

Premises used: Set.mem_union, Set.mem_singleton_iff
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
inl :
  ∀ (ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} x) (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}))
inr : ∀ (xa : x ≠ a), Disjoint x (sSup ((s ∪ {a}) \ {x}))
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
obtain rfl | xa := eq_or_ne x a

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
x : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} x
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
inl : Disjoint x (sSup (s \ {x}))
⊢ Disjoint x (sSup ((s ∪ {x}) \ {x}))

Tactic:
simp only [Set.mem_singleton, Set.insert_diff_of_mem, Set.union_singleton]

Premises used: Set.mem_singleton, Set.insert_diff_of_mem, Set.union_singleton
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
x : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} x
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup (s \ {x}))

Tactic:
con.mono_right ((sSup_le_sSup Set.diff_subset).trans le_sup_right)

Premises used: Set.diff_subset, le_sup_right, LE.le.trans, Disjoint.mono_right, sSup_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
x : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} x
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup (s \ {x}))

Tactic:
exact con.mono_right ((sSup_le_sSup Set.diff_subset).trans le_sup_right)

Premises used: Set.diff_subset, LE.le.trans, Disjoint.mono_right, sSup_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
simp : insert a s \ {x} = insert a (s \ {x})
⊢ (s ∪ {a}) \ {x} = s \ {x} ∪ {a}

Tactic:
simp only [Set.union_singleton]

Premises used: Set.union_singleton
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} 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₁ : a ∉ {x}
⊢ insert a s \ {x} = insert a (s \ {x})

Tactic:
rw [Set.insert_diff_of_notMem]

Premises used: Set.insert_diff_of_notMem
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} 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

Tactic:
Ne.symm xa

Premises used: Ne.symm
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} 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

Tactic:
exact Ne.symm xa

Premises used: Ne.symm
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} 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}

Tactic:
have h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a} := by
        simp only [Set.union_singleton]
        rw [Set.insert_diff_of_notMem]
        rw [Set.mem_singleton_iff]
        exact Ne.symm xa
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h_1 : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} 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}
inr : Disjoint x (sSup (s \ {x}) ⊔ a)
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
rw [h, sSup_union, sSup_singleton]

Premises used: sSup_union, sSup_singleton
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h_1 : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} 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}
this : x ⊔ sSup (s \ {x}) ≤ sSup s
⊢ 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

Premises used: Disjoint.symm, Disjoint.disjoint_sup_right_of_disjoint_sup_left, Or.resolve_right, Disjoint.mono_right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h_1 : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} 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}
rw : sSup (insert x (s \ {x})) ≤ sSup s
rw₁ : sSup (insert x s) ≤ sSup s
rw₂ rw₃ : sSup s ≤ sSup s
⊢ x ⊔ sSup (s \ {x}) ≤ sSup s

Tactic:
rw [← sSup_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]

Premises used: sSup_insert, Set.insert_eq_of_mem, Set.insert_diff_singleton, Or.resolve_right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
inl : ∀ (hx : x ∈ s), IsAtom x ∧ x ≤ c
inr :
  ∀ (ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} x) (con : Disjoint x (b ⊔ sSup s))
    (a_dis_Sup_s : Disjoint x (sSup s)), IsAtom x ∧ x ≤ c
⊢ IsAtom x ∧ x ≤ c

Tactic:
obtain hx | rfl := hx

Premises used: rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s
⊢ IsAtom x ∧ x ≤ c

Tactic:
s_atoms x hx
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} a
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s
⊢ IsAtom x ∧ x ≤ c

Tactic:
exact s_atoms x hx
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
x : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} x
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
⊢ IsAtom x ∧ x ≤ c

Tactic:
ha.symm

Premises used: And.symm
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a : α | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max :
  ∀ ⦃t : Set α⦄,
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} t →
      s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
x : α
ha : Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} x
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
⊢ IsAtom x ∧ x ≤ c

Tactic:
exact ha.symm

Premises used: And.symm
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
h : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
b : α
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | a ≤ ⊤ ∧ IsAtom a}) ⊤

Tactic:
simpa using h
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
h : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
b : α
⊢ ∃ (s : Set α), sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
simpa [isCompl_iff, codisjoint_iff, and_assoc]
    using exists_sSupIndep_disjoint_sSup_atoms b ⊤ le_top <| by simpa using h

Premises used: codisjoint_iff, isCompl_iff, exists_sSupIndep_disjoint_sSup_atoms, le_top, and_assoc, Top.top
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b : α
h : sSup {a : α | a ≤ b ∧ IsAtom a} = b
s : Set α
s_ind : sSupIndep s
left : Disjoint ⊥ (sSup s)
s_atoms : ⊥ ⊔ sSup s = b ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
⊢ sSup s = b ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
simpa using s_atoms
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
h : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | a ≤ ⊤ ∧ IsAtom a}) ⊤

Tactic:
simpa
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
h : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
b : α
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤

Tactic:
simpa
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : IsAtomistic α
⊢ ComplementedLattice α

Tactic:
complementedLattice_of_sSup_atoms_eq_top sSup_atoms_eq_top

Premises used: complementedLattice_of_sSup_atoms_eq_top, sSup_atoms_eq_top
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
mp : ComplementedLattice α → IsAtomistic α
mpr : IsAtomistic α → ComplementedLattice α
⊢ ComplementedLattice α ↔ IsAtomistic α

Tactic:
constructor
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
h : ComplementedLattice α
⊢ IsAtomistic α

Tactic:
isAtomistic_of_complementedLattice

Premises used: isAtomistic_of_complementedLattice
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
h : ComplementedLattice α
⊢ IsAtomistic α

Tactic:
exact isAtomistic_of_complementedLattice

Premises used: isAtomistic_of_complementedLattice
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
h : IsAtomistic α
⊢ ComplementedLattice α

Tactic:
complementedLattice_of_isAtomistic

Premises used: complementedLattice_of_isAtomistic
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
h : IsAtomistic α
⊢ ComplementedLattice α

Tactic:
exact complementedLattice_of_isAtomistic

Premises used: complementedLattice_of_isAtomistic
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
α : Type u_2
inst : CompleteLattice α
a : α
b : (↑(Iic a) : Type u_2)
h : IsCompactElement (↑b : α)
simp :
  ∀ (h : ∀ (ι : Type u_2) (s : ι → α), (↑b : α) ≤ iSup s → ∃ (t : Finset ι), (↑b : α) ≤ ⨆ a ∈ t, s a) (ι : Type u_2)
    (s : ι → (↑(Iic a) : Type u_2)), b ≤ iSup s → ∃ (t : Finset ι), b ≤ ⨆ a_2 ∈ t, s a_2
⊢ IsCompactElement b

Tactic:
simp only [CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup,
    Finset.sup_eq_iSup] at h ⊢

Premises used: CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup, Finset.sup_eq_iSup
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
α : Type u_2
inst : CompleteLattice α
a : α
b : (↑(Iic a) : Type u_2)
h : ∀ (ι : Type u_2) (s : ι → α), (↑b : α) ≤ iSup s → ∃ (t : Finset ι), (↑b : α) ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → (↑(Iic a) : Type u_2)
hb : b ≤ iSup s
⊢ (↑b : α) ≤ iSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ s)

Tactic:
replace hb : (b : α) ≤ iSup ((↑) ∘ s) := le_trans hb <| (coe_iSup s) ▸ le_refl _
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
α : Type u_2
inst : CompleteLattice α
a : α
b : (↑(Iic a) : Type u_2)
h : ∀ (ι : Type u_2) (s : ι → α), (↑b : α) ≤ iSup s → ∃ (t : Finset ι), (↑b : α) ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → (↑(Iic a) : Type u_2)
hb : (↑b : α) ≤ iSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ s)
obtain :
  ∀ (t : Finset ι) (ht : (↑b : α) ≤ ⨆ a_1 ∈ t, (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ s) a_1),
    ∃ (t : Finset ι), b ≤ ⨆ a_1 ∈ t, s a_1
⊢ ∃ (t : Finset ι), b ≤ ⨆ a_1 ∈ t, s a_1

Tactic:
obtain ⟨t, ht⟩ := h ι ((↑) ∘ s) hb

Premises used: Function.comp
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
α : Type u_2
inst : CompleteLattice α
a : α
b : (↑(Iic a) : Type u_2)
h : ∀ (ι : Type u_2) (s : ι → α), (↑b : α) ≤ iSup s → ∃ (t : Finset ι), (↑b : α) ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → (↑(Iic a) : Type u_2)
hb : (↑b : α) ≤ iSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ s)
t : Finset ι
ht : (↑b : α) ≤ ⨆ a_1 ∈ t, (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ s) a_1
⊢ (↑b : α) ≤ (↑(⨆ a_1 ∈ t, s a_1) : α)

Tactic:
simpa using ht