awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
h : WellFounded fun (x1 x2 : α) ↦ x1 < x2
a b : α
hab : a < b
refine :
  a ⋖ h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ∧
    h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ≤ b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
refine ⟨WellFounded.min h (Set.Ioc a b) ⟨b, hab,rfl.le⟩, ?_⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
h : WellFounded fun (x1 x2 : α) ↦ x1 < x2
a b : α
hab : a < b
⊢ h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ∈ Set.Ioc a b

Tactic:
have hmem := (WellFounded.min_mem h (Set.Ioc a b) ⟨b, hab,rfl.le⟩)
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
h : WellFounded fun (x1 x2 : α) ↦ x1 < x2
a b : α
hab : a < b
hmem : h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ∈ Set.Ioc a b
⊢ a ⋖ h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ∧
    h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ≤ b

Tactic:
⟨⟨hmem.1,fun c hac hlt ↦ WellFounded.not_lt_min h
      (Set.Ioc a b) ⟨hac, hlt.le.trans hmem.2⟩ hlt⟩, hmem.2⟩

Premises used: Set.Ioc, LT.lt.le, And.right, And.left, And.intro, WellFounded.not_lt_min, LE.le.trans
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
h : WellFounded fun (x1 x2 : α) ↦ x1 < x2
a b : α
hab : a < b
hmem : h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ∈ Set.Ioc a b
⊢ a ⋖ h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ∧
    h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ≤ b

Tactic:
exact ⟨⟨hmem.1,fun c hac hlt ↦ WellFounded.not_lt_min h
      (Set.Ioc a b) ⟨hac, hlt.le.trans hmem.2⟩ hlt⟩, hmem.2⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
h : WellFounded fun (x1 x2 : α) ↦ x1 > x2
⊢ IsStronglyCoatomic α

Tactic:
isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 <| IsStronglyAtomic.of_wellFounded_lt (α := αᵒᵈ) h

Premises used: isStronglyAtomic_dual_iff_is_stronglyCoatomic, IsStronglyAtomic.of_wellFounded_lt, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : WellFoundedLT α
⊢ IsStronglyAtomic α

Tactic:
IsStronglyAtomic.of_wellFounded_lt wellFounded_lt

Premises used: IsStronglyAtomic.of_wellFounded_lt, wellFounded_lt
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : WellFoundedGT α
⊢ IsStronglyCoatomic α

Tactic:
IsStronglyCoatomic.of_wellFounded_gt wellFounded_gt

Premises used: IsStronglyCoatomic.of_wellFounded_gt, wellFounded_gt
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
h : WellFounded fun (x1 x2 : α) ↦ x1 < x2
⊢ IsAtomic α

Tactic:
(IsStronglyAtomic.of_wellFounded_lt h).isAtomic

Premises used: IsStronglyAtomic.isAtomic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
h : WellFounded fun (x1 x2 : α) ↦ x1 > x2
⊢ IsCoatomic α

Tactic:
isAtomic_dual_iff_isCoatomic.1 (@isAtomic_of_orderBot_wellFounded_lt αᵒᵈ _ _ h)

Premises used: isAtomic_dual_iff_isCoatomic, isAtomic_of_orderBot_wellFounded_lt, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
⊢ x ≤ y ↔ ∀ (a : α), IsAtom a → a ≤ x → a ≤ y

Tactic:
⟨fun h a _ => (le_trans · h), fun h => ?_⟩

Premises used: Iff.intro, le_trans
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
refine : ∀ (h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y), x ≤ y
⊢ x ≤ y ↔ ∀ (a : α), IsAtom a → a ≤ x → a ≤ y

Tactic:
refine ⟨fun h a _ => (le_trans · h), fun h => ?_⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
hbot : ¬x ⊓ yᶜ = ⊥
a : α
ha : IsAtom a
hle : a ≤ x ⊓ yᶜ
hx : a ≤ x
hy' : a ≤ yᶜ
hy : a ≤ y
this : a ≤ y ⊓ yᶜ
⊢ a = ⊥

Tactic:
simpa using this
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
⊢ x ⊓ yᶜ = ⊥

Tactic:
have : x ⊓ yᶜ = ⊥ := of_not_not fun hbot =>
    have ⟨a, ha, hle⟩ := (eq_bot_or_exists_atom_le _).resolve_left hbot
    have ⟨hx, hy'⟩ := le_inf_iff.1 hle
    have hy := h a ha hx
    have : a ≤ y ⊓ yᶜ := le_inf_iff.2 ⟨hy, hy'⟩
    ha.1 (by simpa using this)
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ y = yᶜᶜ

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ x ≤ y

Tactic:
exact (eq_compl_iff_isCompl.1 (by simp)).inf_right_eq_bot_iff.1 this

Premises used: eq_compl_iff_isCompl, Iff.mp, IsCompl.inf_right_eq_bot_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
h : x = y
⊢ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ x)

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
refine : ∀ (h : ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)), x = y
⊢ x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)

Tactic:
refine ⟨fun h => h ▸ by simp, fun h => ?_⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
⊢ x = y

Tactic:
le_antisymm (le_iff_atom_le_imp.2 fun a ha hx => (h a ha).1 hx)
    (le_iff_atom_le_imp.2 fun a ha hy => (h a ha).2 hy)

Premises used: Iff.mpr, BooleanAlgebra.le_iff_atom_le_imp, le_antisymm, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
⊢ x = y

Tactic:
exact le_antisymm (le_iff_atom_le_imp.2 fun a ha hx => (h a ha).1 hx)
    (le_iff_atom_le_imp.2 fun a ha hy => (h a ha).2 hy)

Premises used: Iff.mpr, BooleanAlgebra.le_iff_atom_le_imp, le_antisymm, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteBooleanAlgebra α
inst_2 : IsAtomic α
ι_1 : Type u_4
κ : ι_1 → Type u_4
f : (a : ι_1) → κ a → α
a : α
ha : IsAtom a
⊢ a ≤ ⨅ (a : ι_1), ⨆ (b : κ a), f a b ↔ a ≤ ⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)

Tactic:
simp only [le_iInf_iff, ha.le_iSup, Classical.skolem]

Premises used: Classical.skolem, le_iInf_iff, IsAtom.le_iSup
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
h : IsCoatomistic.{u_2} αᵒᵈ
b : α
⊢ ∃ (s : Set α), IsLUB s b ∧ ∀ a ∈ s, IsAtom a

Tactic:
apply h.isGLB_coatoms

Premises used: IsCoatomistic.isGLB_coatoms
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
h : IsAtomistic α
b : αᵒᵈ
⊢ ∃ (s : Set αᵒᵈ), IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

Tactic:
apply h.isLUB_atoms

Premises used: IsAtomistic.isLUB_atoms
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
h : IsAtomistic.{u_2} αᵒᵈ
b : α
⊢ ∃ (s : Set α), IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

Tactic:
apply h.isLUB_atoms

Premises used: IsAtomistic.isLUB_atoms
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
h : IsCoatomistic α
b : αᵒᵈ
⊢ ∃ (s : Set αᵒᵈ), IsLUB s b ∧ ∀ a ∈ s, IsAtom a

Tactic:
apply h.isGLB_coatoms

Premises used: IsCoatomistic.isGLB_coatoms
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
h : IsAtomistic α
⊢ IsCoatomistic.{u_2} αᵒᵈ

Tactic:
isCoatomistic_dual_iff_isAtomistic.2 h

Premises used: Iff.mpr, isCoatomistic_dual_iff_isAtomistic
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
rcases : ∀ (s : Set α) (hsb : IsLUB s b) (hs : ∀ a ∈ s, IsAtom a), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
rcases isLUB_atoms b with ⟨s, hsb, hs⟩

Premises used: IsAtomistic.isLUB_atoms
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
inl :
  ∀ (hsb : IsLUB ∅ b) (hs : ∀ (a : α), Membership.mem (γ := Set α) ∅ a → IsAtom a), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
inr : ∀ (a : α) (ha : a ∈ s), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
hsb : IsLUB ∅ b
hs : ∀ (a : α), Membership.mem (γ := Set α) ∅ a → IsAtom a
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
simp_all
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ s
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

Premises used: And.left, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ s
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

Premises used: Or.inr
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
rcases : ∀ (s : Set α) (hsb : IsLUB s b) (hs : ∀ a ∈ s, IsAtom a), IsLUB {a : α | IsAtom a ∧ a ≤ b} b
⊢ IsLUB {a : α | IsAtom a ∧ a ≤ b} b

Tactic:
rcases isLUB_atoms b with ⟨s, hsb, hs⟩

Premises used: IsAtomistic.isLUB_atoms
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
⊢ IsLUB {a : α | IsAtom a ∧ a ≤ b} b

Tactic:
⟨fun c hc ↦ hc.2, fun c hc ↦ hsb.2 fun i hi ↦ hc ⟨hs _ hi, hsb.1 hi⟩⟩

Premises used: IsLeast, And.right, And.left, And.intro, IsLUB
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
⊢ IsLUB {a : α | IsAtom a ∧ a ≤ b} b

Tactic:
exact ⟨fun c hc ↦ hc.2, fun c hc ↦ hsb.2 fun i hi ↦ hc ⟨hs _ hi, hsb.1 hi⟩⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
inst_3 : OrderTop α
⊢ IsLUB.{u_2} (α := α) {a : α | IsAtom a} ⊤

Tactic:
simpa using isLUB_atoms_le (⊤ : α)

Premises used: Top.top, isLUB_atoms_le
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
a b : α
⊢ a ≤ b ↔ ∀ (c : α), IsAtom c → c ≤ a → c ≤ b

Tactic:
⟨fun hab _ _ hca ↦ hca.trans hab,
   fun h ↦ (isLUB_atoms_le a).mono (isLUB_atoms_le b) fun _ ⟨h₁, h₂⟩ ↦ ⟨h₁, h _ h₁ h₂⟩⟩

Premises used: setOf, Membership.mem, LE.le, IsLUB.mono, _private.0.le_iff_atom_le_imp.match_1, And, And.intro, Iff.intro, IsAtom, LE.le.trans, isLUB_atoms_le
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
a b : α
h : a = b
⊢ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)

Tactic:
simp [h]
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
a b : α
refine : ∀ (h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)), a = b
⊢ a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)

Tactic:
refine ⟨fun h => by simp [h], fun h => ?_⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
rw : (∀ (c : α), IsAtom c → c ≤ a → c ≤ b) ∧ ∀ (c : α), IsAtom c → c ≤ b → c ≤ a
⊢ a = b

Tactic:
rw [le_antisymm_iff, le_iff_atom_le_imp, le_iff_atom_le_imp]

Premises used: le_iff_atom_le_imp, le_antisymm_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ (∀ (c : α), IsAtom c → c ≤ a → c ≤ b) ∧ ∀ (c : α), IsAtom c → c ≤ b → c ≤ a

Tactic:
simp_all
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
h : IsCoatomistic α
⊢ IsAtomistic.{u_2} αᵒᵈ

Tactic:
isAtomistic_dual_iff_isCoatomistic.2 h

Premises used: Iff.mpr, isAtomistic_dual_iff_isCoatomistic
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomistic α
b : α
rcases : ∀ (s : Set α) (hsb : IsGLB s b) (hs : ∀ a ∈ s, IsCoatom a), b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
⊢ b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a

Tactic:
rcases isGLB_coatoms b with ⟨s, hsb, hs⟩

Premises used: IsCoatomistic.isGLB_coatoms
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomistic α
b : α
s : Set α
hsb : IsGLB s b
hs : ∀ a ∈ s, IsCoatom a
inl :
  ∀ (hsb : IsGLB ∅ b) (hs : ∀ (a : α), Membership.mem (γ := Set α) ∅ a → IsCoatom a),
    b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
inr : ∀ (a : α) (ha : a ∈ s), b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
⊢ b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomistic α
b : α
hsb : IsGLB ∅ b
hs : ∀ (a : α), Membership.mem (γ := Set α) ∅ a → IsCoatom a
⊢ b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a

Tactic:
simp_all
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomistic α
b : α
s : Set α
hsb : IsGLB s b
hs : ∀ a ∈ s, IsCoatom a
a : α
ha : a ∈ s
⊢ b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a

Tactic:
Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

Premises used: And.left, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomistic α
b : α
s : Set α
hsb : IsGLB s b
hs : ∀ a ∈ s, IsCoatom a
a : α
ha : a ∈ s
⊢ b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a

Tactic:
exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

Premises used: Or.inr
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteLattice α
inst_1 : IsAtomistic α
b : α
⊢ sSup {a : α | IsAtom a ∧ a ≤ b} = b

Tactic:
(isLUB_atoms_le b).sSup_eq

Premises used: IsLUB.sSup_eq, isLUB_atoms_le
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteLattice α
inst_1 : IsAtomistic α
⊢ Eq.{u_4 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤

Tactic:
isLUB_atoms_top.sSup_eq

Premises used: setOf, IsLUB.sSup_eq, isLUB_atoms_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteLattice α
simp_rw :
  (∀ (b : α), ∃ (s : Set α), IsLUB s b ∧ ∀ a ∈ s, IsAtom a) ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
simp_rw₁ :
  (∀ (b : α), ∃ (s : Set α), sSup s = b ∧ ∀ a ∈ s, IsAtom a) ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
⊢ IsAtomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
simp_rw [isAtomistic_iff, isLUB_iff_sSup_eq, eq_comm]

Premises used: isLUB_iff_sSup_eq, eq_comm, CompleteLattice.isAtomistic_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteLattice α
inst_1 : IsAtomistic α
b : α
⊢ ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
CompleteLattice.isAtomistic_iff.1 ‹_› b

Premises used: Iff.mp, CompleteLattice.isAtomistic_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteLattice α
simp_rw :
  (∀ (b : α), ∃ (s : Set α), IsGLB s b ∧ ∀ a ∈ s, IsCoatom a) ↔
    ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a
simp_rw₁ :
  (∀ (b : α), ∃ (s : Set α), sInf s = b ∧ ∀ a ∈ s, IsCoatom a) ↔
    ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a
⊢ IsCoatomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a

Tactic:
simp_rw [isCoatomistic_iff, isGLB_iff_sInf_eq, eq_comm]

Premises used: eq_comm, isGLB_iff_sInf_eq, CompleteLattice.isCoatomistic_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteLattice α
inst_1 : IsCoatomistic α
b : α
⊢ ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a

Tactic:
CompleteLattice.isCoatomistic_iff.1 ‹_› b

Premises used: CompleteLattice.isCoatomistic_iff, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabit : ∀ (inhabited_h : Inhabited α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
⊢ ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
inhabit α
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
⟨{ a | IsAtom a ∧ a ≤ b }, ?_, fun a ha => ha.1⟩

Premises used: setOf, LE.le, And, And.left, And.intro, Exists.intro, IsAtom
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
refine : b = sSup {a : α | IsAtom a ∧ a ≤ b}
⊢ ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
refine ⟨{ a | IsAtom a ∧ a ≤ b }, ?_, fun a ha => ha.1⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ b = sSup {a : α | IsAtom a ∧ a ≤ b}

Tactic:
le_antisymm ?_ (sSup_le fun c hc => hc.2)

Premises used: le_antisymm, And.right, sSup_le
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
refine : b ≤ sSup {a : α | IsAtom a ∧ a ≤ b}
⊢ b = sSup {a : α | IsAtom a ∧ a ≤ b}

Tactic:
refine le_antisymm ?_ (sSup_le fun c hc => hc.2)

Premises used: le_antisymm, sSup_le
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) = b

Tactic:
simp [iSup_bool_eq]

Premises used: iSup_bool_eq
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) = b

Tactic:
have : (⨅ c : α, ⨆ x, b ⊓ cond x c (cᶜ)) = b := by simp [iSup_bool_eq]
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
this : (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) = b
rw :
  LE.le.{u_4} (α := α) (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ})
⊢ b ≤ sSup {a : α | IsAtom a ∧ a ≤ b}

Tactic:
rw [← this]
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
simp_rw :
  ∀ (i : (a : α) → Bool),
    LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif i a then a else aᶜ)
      (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})
⊢ LE.le.{u_4} (α := α) (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ})

Tactic:
simp_rw [iInf_iSup_eq, iSup_le_iff]

Premises used: iInf_iSup_eq, iSup_le_iff
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
h : Eq.{u_4 + 1} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ⊥
⊢ LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})

Tactic:
simp [h]
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
h : ¬Eq.{u_4 + 1} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ⊥
⊢ LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ) (⨅ (a : α), b ⊓ bif g a then a else aᶜ)

Tactic:
rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
h : ¬Eq.{u_4 + 1} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ⊥
refine : ∀ (c : α) (hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ), c = ⊥
⊢ LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})

Tactic:
refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
⊢ c < bif g c then c else cᶜ

Tactic:
have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right)
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
this : c < bif g c then c else cᶜ
revert : ∀ (this : c < bif g c then c else cᶜ), c = ⊥
⊢ c = ⊥

Tactic:
revert this
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
h : Nontrivial α
false : ∀ (this : c < bif Bool.false then c else cᶜ), c = ⊥
true : ∀ (this : c < bif Bool.true then c else cᶜ), c = ⊥
⊢ ∀ (this : c < bif g c then c else cᶜ), c = ⊥

Tactic:
cases g c
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
h : Nontrivial α
⊢ ∀ (this : c < bif false then c else cᶜ), c = ⊥

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
h : Nontrivial α
⊢ ∀ (this : c < bif true then c else cᶜ), c = ⊥

Tactic:
simp