awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
a : { x : α // x ∈ Iic c }
ha : IsAtom a
hac : (↑a : α) ≤ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c ⋯ : { x : α // x ∈ Iic c }) : α)
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
⟨a, ha.of_isAtom_coe_Iic, hac.trans hcb⟩

Premises used: IsAtom.of_isAtom_coe_Iic, And.intro, Exists.intro, LE.le.trans, Subtype.val
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
a : { x : α // x ∈ Iic c }
ha : IsAtom a
hac : (↑a : α) ≤ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c ⋯ : { x : α // x ∈ Iic c }) : α)
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
exact ⟨a, ha.of_isAtom_coe_Iic, hac.trans hcb⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
symm : sSup {a : α | IsAtom a ∧ a ≤ b} = b
⊢ b = sSup {a : α | IsAtom a ∧ a ≤ b}

Tactic:
symm
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
⊢ sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b

Tactic:
have hle : sSup { a : α | IsAtom a ∧ a ≤ b } ≤ b := sSup_le fun _ => And.right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
apply : ¬sSup {a : α | IsAtom a ∧ a ≤ b} < b
⊢ sSup {a : α | IsAtom a ∧ a ≤ b} = b

Tactic:
apply (lt_or_eq_of_le hle).resolve_left _

Premises used: lt_or_eq_of_le, Or.resolve_left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
obtain :
  ∀ (c : { x : α // x ∈ Iic b })
    (hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c), False
⊢ False

Tactic:
obtain ⟨c, hc⟩ := exists_isCompl (⟨sSup { a : α | IsAtom a ∧ a ≤ b }, hle⟩ : Set.Iic b)

Premises used: setOf, ComplementedLattice.exists_isCompl, LE.le, Subtype.mk, And, IsAtom, SupSet.sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
inl : ∀ (hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) ⊥), False
inr : ∀ (a : { x : α // x ∈ Iic b }) (ha : IsAtom a) (hac : a ≤ c), False
⊢ False

Tactic:
obtain rfl | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le c

Premises used: IsAtomic.eq_bot_or_exists_atom_le, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) ⊥
⊢ False

Tactic:
ne_of_lt con (Subtype.ext_iff.1 (eq_top_of_isCompl_bot hc))

Premises used: Subtype.ext_iff, Iff.mp, eq_top_of_isCompl_bot, ne_of_lt
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) ⊥
⊢ False

Tactic:
exact ne_of_lt con (Subtype.ext_iff.1 (eq_top_of_isCompl_bot hc))

Premises used: Subtype.ext_iff, Iff.mp, eq_top_of_isCompl_bot, ne_of_lt
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
a : { x : α // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
inr : a = ⊥
⊢ False

Tactic:
apply ha.1

Premises used: And.left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
a : { x : α // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
inr : a ≤ ⊥
⊢ a = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
a : { x : α // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
apply : a ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle
⊢ a ≤ ⊥

Tactic:
apply le_trans (le_inf _ hac) hc.disjoint.le_bot

Premises used: Disjoint.le_bot, le_inf, IsCompl.disjoint, le_trans
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
a : { x : α // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
rw : (↑a : α) ≤ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) : α)
⊢ a ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle

Tactic:
rw [← Subtype.coe_le_coe, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Subtype.coe_le_coe
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
a : { x : α // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ (↑a : α) ≤ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) : α)

Tactic:
le_sSup ⟨ha.of_isAtom_coe_Iic, a.2⟩

Premises used: IsAtom.of_isAtom_coe_Iic, And.intro, le_sSup, Subtype.property
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
a : { x : α // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ (↑a : α) ≤ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) : α)

Tactic:
exact le_sSup ⟨ha.of_isAtom_coe_Iic, a.2⟩
-- 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
refine_2 :
  ∀
    (zorn :
      ∃ (m : Set α),
        Maximal
          (fun (x : Set α) ↦
            Membership.mem (γ := Set (Set α))
              {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} x)
          m),
    ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
refine_1 :
  ∀ (c_1 : Set (Set α)) (hc1 : c_1 ⊆ {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c})
    (hc2 : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c_1), Disjoint b (sSup (⋃₀ c_1))
⊢ ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
have zorn := zorn_subset
    (S := {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c})
    fun c hc1 hc2 =>
      ⟨⋃₀ c,
        ⟨iSupIndep_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⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c_1 : α
hbc : b ≤ c_1
h : sSup {a : α | a ≤ c_1 ∧ IsAtom a} = c_1
c : Set (Set α)
hc1 : c ⊆ {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c_1}
hc2 : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
refine_1 : ∀ ⦃b_1 : α⦄, b_1 ∈ sSup '' c → Disjoint b b_1
refine_1₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (sSup '' c)
⊢ Disjoint b (sSup (⋃₀ c))

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

Premises used: sSup_image, sSup_sUnion, DirectedOn.disjoint_sSup_right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c_1 : α
hbc : b ≤ c_1
h : sSup {a : α | a ≤ c_1 ∧ IsAtom a} = c_1
c : Set (Set α)
hc1 : c ⊆ {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c_1}
hc2 : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
s : Set α
hs : s ∈ c
⊢ Disjoint b (sSup s)

Tactic:
(hc1 hs).2.1

Premises used: And.right, And.left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c_1 : α
hbc : b ≤ c_1
h : sSup {a : α | a ≤ c_1 ∧ IsAtom a} = c_1
c : Set (Set α)
hc1 : c ⊆ {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c_1}
hc2 : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
s : Set α
hs : s ∈ c
⊢ Disjoint b (sSup s)

Tactic:
exact (hc1 hs).2.1

Premises used: And.right, And.left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c_1 : α
hbc : b ≤ c_1
h : sSup {a : α | a ≤ c_1 ∧ IsAtom a} = c_1
c : Set (Set α)
hc1 : c ⊆ {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c_1}
hc2 : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
refine_1 : DirectedOn (sSup ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) c
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (sSup '' c)

Tactic:
rw [directedOn_image]

Premises used: directedOn_image
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c_1 : α
hbc : b ≤ c_1
h : sSup {a : α | a ≤ c_1 ∧ IsAtom a} = c_1
c : Set (Set α)
hc1 : c ⊆ {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c_1}
hc2 : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
⊢ DirectedOn (sSup ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) c

Tactic:
hc2.directedOn.mono @fun s t => sSup_le_sSup

Premises used: IsChain.directedOn, DirectedOn.mono, sSup_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
b c_1 : α
hbc : b ≤ c_1
h : sSup {a : α | a ≤ c_1 ∧ IsAtom a} = c_1
c : Set (Set α)
hc1 : c ⊆ {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c_1}
hc2 : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
⊢ DirectedOn (sSup ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) c

Tactic:
exact hc2.directedOn.mono @fun s t => sSup_le_sSup

Premises used: IsChain.directedOn, DirectedOn.mono, 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
zorn :
  ∃ (m : Set α),
    Maximal
      (fun (x : Set α) ↦
        Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} x)
      m
⊢ ∃ (m : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} m ∧
      ∀ ⦃t : Set α⦄,
        Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c}
            t →
          m ⊆ t → m = t

Tactic:
simp_rw [maximal_subset_iff] at zorn

Premises used: maximal_subset_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
zorn :
  ∃ (m : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} m ∧
      ∀ ⦃t : Set α⦄,
        Membership.mem (γ := Set (Set α)) {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c}
            t →
          m ⊆ t → m = t
refine_2 :
  ∀ (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),
    ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
⊢ ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn
-- 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
⊢ ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
⟨s, s_ind, b_inf_Sup_s, le_antisymm ?_ ?_, fun a ha ↦ (s_atoms a ha).1⟩

Premises used: le_antisymm, And.left, And.intro, Exists.intro
-- 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
refine_2 : b ⊔ sSup s ≤ c
refine_2₁ : c ≤ b ⊔ sSup s
⊢ ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
refine ⟨s, s_ind, b_inf_Sup_s, le_antisymm ?_ ?_, fun a ha ↦ (s_atoms a ha).1⟩
-- 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
⊢ b ⊔ sSup s ≤ c

Tactic:
simp_all
-- 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
refine_2 : ∀ (b_1 : α), Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} b_1 → b_1 ≤ b ⊔ sSup s
⊢ c ≤ b ⊔ sSup s

Tactic:
rw [← h, sSup_le_iff]

Premises used: sSup_le_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
refine_2 : a ⊓ (b ⊔ sSup s) = a
⊢ a ≤ b ⊔ sSup s

Tactic:
rw [← inf_eq_left]

Premises used: inf_eq_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
⊢ a ⊓ (b ⊔ sSup s) = a

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

Premises used: Or.resolve_left, IsAtom.le_iff, And.right, And.left, Iff.mp, inf_le_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
refine_2 : ∀ (con : a ⊓ (b ⊔ sSup s) = ⊥), a = ⊥
⊢ a ⊓ (b ⊔ sSup s) = a

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

Premises used: Or.resolve_left, IsAtom.le_iff, And.right, And.left, Iff.mp, inf_le_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 : a ⊓ (b ⊔ sSup s) = ⊥
refine_2 : a ≤ b ⊔ sSup s
⊢ a = ⊥

Tactic:
rw [← con, eq_comm, inf_eq_left]

Premises used: eq_comm, inf_eq_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 : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ≤ b ⊔ sSup s

Tactic:
(le_sSup ?_).trans le_sup_right

Premises used: le_sup_right, le_sSup, LE.le.trans
-- 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 : a ⊓ (b ⊔ sSup s) = ⊥
refine_2 : a ∈ s
⊢ a ≤ b ⊔ sSup s

Tactic:
refine (le_sSup ?_).trans le_sup_right

Premises used: le_sSup, LE.le.trans
-- 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 : a ⊓ (b ⊔ sSup s) = ⊥
⊢ Disjoint a (b ⊔ sSup s)

Tactic:
rw [← disjoint_iff] at con

Premises used: disjoint_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)
⊢ Disjoint a (sSup s)

Tactic:
have a_dis_Sup_s : Disjoint a (sSup s) := con.mono_right le_sup_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)
refine_2 : a ∈ s ∪ {a}
rw : Set α
rw₁ : Disjoint b (sSup (s ∪ {a}))
rw₂ : ∀ (x : α) (hx : x ∈ s ∪ {a}), Disjoint x (sSup ((s ∪ {a}) \ {x}))
rw₃ : ∀ (x : α) (hx : x ∈ s ∪ {a}), IsAtom x ∧ x ≤ c
⊢ a ∈ s

Tactic:
rw [s_max ⟨fun x hx => ?_, ?_, fun x hx => ?_⟩ Set.subset_union_left]

Premises used: Set.subset_union_left, And.intro