awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
have inr : Disjoint x (sSup (s \ {x}) ⊔ a)
Tactic: rw [h, sSup_union, sSup_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_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}
⊢ Disjoint x (sSup (s \ {x}) ⊔ a)
have this : x ⊔ sSup (s \ {x}) ≤ sSup s
Tactic: apply
        (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
          (a_dis_Sup_s.mono_right _).symm
-- 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_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}
⊢ x ⊔ sSup (s \ {x}) ≤ sSup s
have rw : sSup (insert x (s \ {x})) ≤ sSup s
Tactic: rw [← sSup_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]
-- 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_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
⊢ x ⊔ sSup (s \ {x}) ≤ sSup s
have rw₁ : sSup (insert x s) ≤ sSup s
Tactic: rw [← sSup_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]
-- 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_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
⊢ x ⊔ sSup (s \ {x}) ≤ sSup s
have rw₂ : sSup s ≤ sSup s
Tactic: rw [← sSup_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]
-- 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}
⊢ IsAtom x ∧ x ≤ c
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
⊢ IsAtom x ∧ x ≤ c
have inl : ∀ (hx : x ∈ s), IsAtom x ∧ x ≤ c
Tactic: obtain hx | rfl := 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
inl : ∀ (hx : x ∈ s), IsAtom x ∧ x ≤ c
⊢ IsAtom x ∧ x ≤ c
have 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
Tactic: obtain hx | rfl := hx
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 α
⊢ ComplementedLattice α ↔ IsAtomistic α
have mp : ComplementedLattice α → IsAtomistic α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
mp : ComplementedLattice α → IsAtomistic α
⊢ ComplementedLattice α ↔ IsAtomistic α
have mpr : IsAtomistic α → ComplementedLattice α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
a : α
b : (↑(Iic a) : Type u_2)
h : IsCompactElement (↑b : α)
⊢ IsCompactElement b
have 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
Tactic: simp only [CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup,
    Finset.sup_eq_iSup] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (hypothesis)
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
⊢ ∃ (t : Finset ι), b ≤ ⨆ a_1 ∈ t, s a_1
have hb₁ : (↑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 _
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
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 ι), b ≤ ⨆ a_1 ∈ t, s a_1
have 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
Tactic: obtain ⟨t, ht⟩ := h ι ((↑) ∘ s) hb
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
⊢ IsCompactlyGenerated.{u_2} (↑(Iic a) : Type u_2)
have refine : ∀ (x : (↑(Iic a) : Type u_2)) (x : α) (hx : x ≤ a),
  ∃ (s : Set (↑(Iic a) : Type u_2)),
    (∀ x ∈ s, IsCompactElement x) ∧ sSup s = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) x hx
Tactic: refine ⟨fun ⟨x, (hx : x ≤ a)⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x_1 : (↑(Iic a) : Type u_2)
x : α
hx : x ≤ a
⊢ ∃ (s : Set (↑(Iic a) : Type u_2)),
    (∀ x ∈ s, IsCompactElement x) ∧ sSup s = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) x hx
have obtain : ∀ (s : Set α) (hs : ∀ x ∈ s, IsCompactElement x) (hx : sSup s ≤ a),
  ∃ (s_1 : Set (↑(Iic a) : Type u_2)),
    (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx
Tactic: obtain ⟨s, hs, rfl⟩ := IsCompactlyGenerated.exists_sSup_eq x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx : sSup s ≤ a
⊢ ∃ (s_1 : Set (↑(Iic a) : Type u_2)),
    (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx
have hx₁ : ∀ b ∈ s, b ≤ a
Tactic: rw [sSup_le_iff] at hx
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
⊢ ∃ (s_1 : Set (↑(Iic a) : Type u_2)),
    (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1
have refine_1 : ∀ x ∈ range f, IsCompactElement x
Tactic: refine ⟨range f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
refine_1 : ∀ x ∈ range f, IsCompactElement x
⊢ ∃ (s_1 : Set (↑(Iic a) : Type u_2)),
    (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1
have refine_2 : sSup (range f) = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1
Tactic: refine ⟨range f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
⊢ sSup (range f) = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1
have refine_2 : (↑(sSup (range f)) : α) = (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1) : α)
Tactic: rw [Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
⊢ (↑(sSup (range f)) : α) = (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1) : α)
have refine_2 : sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f) = sSup s
Tactic: change sSup (((↑) : Iic a → α) '' (range f)) = sSup s
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f) = sSup s
have refine_2 : Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f = s
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f = s
have refine_2 : ∀ (b : α), b ∈ Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f ↔ b ∈ s
Tactic: ext b
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
⊢ ComplementedLattice α
have h₁ : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
Tactic: apply complementedLattice_of_sSup_atoms_eq_top
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
⊢ ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a
have h₁ : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
Tactic: replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
⊢ ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a
have obtain : ∀ (u : Set (↑(Iic (f i)) : Type u_2)) (hu : ⊤ = sSup u) (hu' : ∀ a ∈ u, IsAtom a),
  ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a
Tactic: obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a
have refine_1 : f i = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u)
Tactic: refine ⟨(↑) '' u, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
refine_1 : f i = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u)
⊢ ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a
have refine_2 : ∀ a ∈ Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u, IsAtom a
Tactic: refine ⟨(↑) '' u, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ f i = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u)
have hu₁ : f i = (↑(sSup u) : α)
Tactic: replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu' : ∀ a ∈ u, IsAtom a
hu : f i = (↑(sSup u) : α)
⊢ f i = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u)
have refine_1 : (↑(sSup u) : α) = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u)
Tactic: simp_rw [hu, Iic.coe_sSup]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
have this : ∀ i ∈ s, ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a
Tactic: have : ∀ i ∈ s, ∃ t : Set α, f i = sSup t ∧ ∀ a ∈ t, IsAtom a := fun i hi ↦ by
    replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
    obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))
    refine ⟨(↑) '' u, ?_, ?_⟩
    · replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
      simp_rw [hu, Iic.coe_sSup]
    · rintro b ⟨⟨a, ha'⟩, ha, rfl⟩
      exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
this : ∀ i ∈ s, ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
have h₁ : ∀ (t : (i : ι) → i ∈ s → Set α) (ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a))
  (ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1), Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
Tactic: choose t ht ht' using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
have hu₁ : u ⊆ {a : α | IsAtom a}
Tactic: have hu₁ : u ⊆ {a | IsAtom a} := by
    rintro a ⟨-, ⟨i, rfl⟩, ⟨-, ⟨hi, rfl⟩, ha : a ∈ t i hi⟩⟩
    exact ht' i hi a ha
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a : α | IsAtom a}
simp_rw : Eq.{u_2 + 1} (α := α) (sSup (⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi)) (⨆ i ∈ s, f i)
⊢ sSup u = ⨆ i ∈ s, f i
have simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), ⨆ (i_1 : i ∈ s), sSup (t i i_1)) (⨆ i ∈ s, f i)
Tactic: simp_rw [u, sSup_iUnion, biSup_congr' ht]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a : α | IsAtom a}
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
have hu₂ : sSup u = ⨆ i ∈ s, f i
Tactic: have hu₂ : sSup u = ⨆ i ∈ s, f i := by simp_rw [u, sSup_iUnion, biSup_congr' ht]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Intervals (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a : α | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
have h₁ : sSup u ≤ sSup {a : α | IsAtom a}
Tactic: rw [eq_top_iff, ← h', ← hu₂]
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ ¬IncompRel r a b ↔ SymmGen r a b
have rw : ¬¬SymmGen r a b ↔ SymmGen r a b
Tactic: rw [← not_symmGen_iff, not_not]
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
r : α → α → Prop
rw : ¬¬SymmGen r a b ↔ SymmGen r a b
⊢ ¬IncompRel r a b ↔ SymmGen r a b
have rw₁ : SymmGen r a b ↔ SymmGen r a b
Tactic: rw [← not_symmGen_iff, not_not]
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Total r
a b : α
⊢ ¬IncompRel r a b
have rw : SymmGen r a b
Tactic: rw [not_incompRel_iff_symmGen]
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
⊢ ¬b ≤ a ↔ a < b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have rw : ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
Tactic: rw [lt_iff_le_not_ge, IncompRel]
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
have mp : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
Tactic: tauto