awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ≤ ⊥
have apply : a ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle
Tactic: apply le_trans (le_inf _ hac) hc.disjoint.le_bot
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have rw : (↑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]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
have 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
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⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
have 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))
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⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ Disjoint b (sSup (⋃₀ c))
have refine_1 : ∀ ⦃b_1 : α⦄, b_1 ∈ sSup '' c → Disjoint b b_1
Tactic: rw [sSup_sUnion, ← sSup_image, DirectedOn.disjoint_sSup_right]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ Disjoint b (sSup (⋃₀ c))
have refine_1₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (sSup '' c)
Tactic: rw [sSup_sUnion, ← sSup_image, DirectedOn.disjoint_sSup_right]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 (fun (x1 x2 : α) ↦ x1 ≤ x2) (sSup '' c)
have refine_1 : DirectedOn (sSup ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) c
Tactic: rw [directedOn_image]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
have 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
Tactic: simp_rw [maximal_subset_iff] at zorn
Cleared hypotheses: zorn
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
have 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
Tactic: obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn
Cleared hypotheses: zorn
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have refine_2 : b ⊔ sSup s ≤ c
Tactic: refine ⟨s, s_ind, b_inf_Sup_s, le_antisymm ?_ ?_, fun a ha ↦ (s_atoms a ha).1⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (s : Set α), sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
have refine_2₁ : c ≤ b ⊔ sSup s
Tactic: refine ⟨s, s_ind, b_inf_Sup_s, le_antisymm ?_ ?_, fun a ha ↦ (s_atoms a ha).1⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ c ≤ b ⊔ sSup s
have refine_2 : ∀ (b_1 : α), Membership.mem (γ := Set α) {a : α | a ≤ c ∧ IsAtom a} b_1 → b_1 ≤ b ⊔ sSup s
Tactic: rw [← h, sSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have refine_2 : a ⊓ (b ⊔ sSup s) = a
Tactic: rw [← inf_eq_left]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have refine_2 : ∀ (con : a ⊓ (b ⊔ sSup s) = ⊥), a = ⊥
Tactic: refine (ha.2.le_iff.mp inf_le_left).resolve_left fun con => ha.2.1 ?_
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 = ⊥
have refine_2 : a ≤ b ⊔ sSup s
Tactic: rw [← con, eq_comm, inf_eq_left]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have refine_2 : a ∈ s
Tactic: refine (le_sSup ?_).trans le_sup_right
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 ∈ s
have con₁ : Disjoint a (b ⊔ sSup s)
Tactic: rw [← disjoint_iff] at con
Cleared hypotheses: con
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 ∈ s
have a_dis_Sup_s : Disjoint a (sSup s)
Tactic: have a_dis_Sup_s : Disjoint a (sSup s) := con.mono_right le_sup_right
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have refine_2 : a ∈ s ∪ {a}
Tactic: rw [s_max ⟨fun x hx => ?_, ?_, fun x hx => ?_⟩ Set.subset_union_left]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 α
⊢ a ∈ s
have rw₁ : Disjoint b (sSup (s ∪ {a}))
Tactic: rw [s_max ⟨fun x hx => ?_, ?_, fun x hx => ?_⟩ Set.subset_union_left]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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}))
⊢ a ∈ s
have rw₂ : ∀ (x : α) (hx : x ∈ s ∪ {a}), Disjoint x (sSup ((s ∪ {a}) \ {x}))
Tactic: rw [s_max ⟨fun x hx => ?_, ?_, fun x hx => ?_⟩ Set.subset_union_left]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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}))
⊢ a ∈ s
have rw₃ : ∀ (x : α) (hx : x ∈ s ∪ {a}), IsAtom x ∧ x ≤ c
Tactic: rw [s_max ⟨fun x hx => ?_, ?_, fun x hx => ?_⟩ Set.subset_union_left]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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}))
have rw : Disjoint b (sSup s ⊔ a)
Tactic: rw [sSup_union, sSup_singleton]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
have hx₁ : x ∈ s ∨ x = a
Tactic: rw [Set.mem_union, Set.mem_singleton_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
have 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}))
Tactic: obtain rfl | xa := eq_or_ne x a
Cleared hypotheses: a, ha, con, a_dis_Sup_s, hx
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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}))
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
have inr : ∀ (xa : x ≠ a), Disjoint x (sSup ((s ∪ {a}) \ {x}))
Tactic: obtain rfl | xa := eq_or_ne x a
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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}) \ {x}))
have inl : Disjoint x (sSup (s \ {x}))
Tactic: simp only [Set.mem_singleton, Set.insert_diff_of_mem, Set.union_singleton]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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}
have simp : insert a s \ {x} = insert a (s \ {x})
Tactic: simp only [Set.union_singleton]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ insert a s \ {x} = insert a (s \ {x})
have h₁ : a ∉ {x}
Tactic: rw [Set.insert_diff_of_notMem]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
have h₁ : (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