awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
if :
  ∀ (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ᶜ})
if₁ :
  ∀ (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ᶜ})
if₂ :
  ∀ (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ᶜ})
if₃ if₄ :
  ∀ (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ᶜ})
⊢ 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:
if h : (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥ then simp [h] else
    refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩; clear h
    have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right)
    revert this
    nontriviality α
    cases g c <;> simp

Premises used: cond, iInf, Compl.compl, Min.min
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
⊢ IsCoatomistic α

Tactic:
isAtomistic_dual_iff_isCoatomistic.1 inferInstance

Premises used: inferInstance, isAtomistic_dual_iff_isCoatomistic, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
a : α
ha : IsAtom a
s : Set α
hs : a ≤ sSup s
⊢ ∃ b ∈ s, a ≤ b

Tactic:
(IsAtom.le_sSup ha).mp hs

Premises used: Iff.mp, IsAtom.le_sSup
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
h : ∀ (a : α), a ∈ S ↔ Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a
⊢ S = {a : α | a ≤ sSup S ∧ IsAtom a}

Tactic:
ext a
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
⊢ a ∈ S ↔ Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a

Tactic:
⟨fun h => ⟨le_sSup h, hS a h⟩, fun ⟨hale, hatom⟩ => ?_⟩

Premises used: Membership.mem, And.intro, Iff.intro, _private.0.CompleteAtomicBooleanAlgebra.eq_setOf_le_sSup_and_isAtom.match_1, le_sSup
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
h : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a → ∀ (hale : a ≤ sSup S) (hatom : IsAtom a), a ∈ S
⊢ a ∈ S ↔ Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a

Tactic:
refine ⟨fun h => ⟨le_sSup h, hS a h⟩, fun ⟨hale, hatom⟩ => ?_⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
h_1 : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a
hale : a ≤ sSup S
hatom : IsAtom a
h : ∀ (b : α) (hbS : b ∈ S) (hba : a ≤ b), a ∈ S
⊢ a ∈ S

Tactic:
obtain ⟨b, hbS, hba⟩ := (IsAtom.le_sSup hatom).mp hale

Premises used: Iff.mp, IsAtom.le_sSup
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
h_1 : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a
hale : a ≤ sSup S
hatom : IsAtom a
b : α
hbS : b ∈ S
hba : a ≤ b
h :
  Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} ⊥ →
    ∀ (hale : ⊥ ≤ sSup S) (hatom : IsAtom.{u_4} (α := α) ⊥) (hba : ⊥ ≤ b), ⊥ ∈ S
h₁ : ∀ (hbS : a ∈ S) (hba : a ≤ a), a ∈ S
⊢ a ∈ S

Tactic:
obtain rfl | rfl := (hS b hbS).le_iff.mp hba

Premises used: IsAtom.le_iff, Iff.mp, rfl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
b : α
hbS : b ∈ S
h : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} ⊥
hale : ⊥ ≤ sSup S
hatom : IsAtom.{u_4} (α := α) ⊥
hba : ⊥ ≤ b
⊢ ⊥ ∈ S

Tactic:
simpa using hatom.1

Premises used: And.left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
h : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a
hale : a ≤ sSup S
hatom : IsAtom a
hbS : a ∈ S
hba : a ≤ a
⊢ a ∈ S

Tactic:
assumption
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
A : α
⊢ (fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S))
      ((fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a })) A) =
    A

Tactic:
simp [Subtype.coe_image]

Premises used: Subtype.coe_image
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
S : Set { a : α // IsAtom a }
a' : { a : α // IsAtom a }
ha' : a' ∈ S
⊢ IsAtom (↑a' : α)

Tactic:
a'.prop

Premises used: Subtype.prop
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
S : Set { a : α // IsAtom a }
a' : { a : α // IsAtom a }
ha' : a' ∈ S
⊢ IsAtom (↑a' : α)

Tactic:
exact a'.prop

Premises used: Subtype.prop
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
S : Set { a : α // IsAtom a }
⊢ ∀ a ∈ Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S, IsAtom a

Tactic:
have h : ∀ a ∈ Subtype.val '' S, IsAtom a := by
      rintro a ⟨a', ha', rfl⟩
      exact a'.prop
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
S : Set { a : α // IsAtom a }
h : ∀ a ∈ Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S, IsAtom a
rw :
  Eq.{u_4 + 1} (α := Set α)
    (Set.image (α := { a : α // IsAtom a }) (Subtype.val (p := fun (a : α) ↦ IsAtom a))
      ((fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
        ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S)))
    {a : α | a ≤ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S) ∧ IsAtom a}
⊢ (fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
      ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S) =
    S

Tactic:
rw [← Subtype.val_injective.image_injective.eq_iff, eq_setOf_le_sSup_and_isAtom h]

Premises used: Subtype.val_injective, CompleteAtomicBooleanAlgebra.eq_setOf_le_sSup_and_isAtom, Function.Injective.eq_iff, Function.Injective.image_injective
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
S : Set { a : α // IsAtom a }
h : ∀ a ∈ Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S, IsAtom a
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
        (Set.image (α := { a : α // IsAtom a }) (Subtype.val (p := fun (a : α) ↦ IsAtom a))
          ((fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
            ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S)))
        a ↔
      Membership.mem (γ := Set α) {a : α | a ≤ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S) ∧ IsAtom a} a
⊢ Eq.{u_4 + 1} (α := Set α)
    (Set.image (α := { a : α // IsAtom a }) (Subtype.val (p := fun (a : α) ↦ IsAtom a))
      ((fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
        ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S)))
    {a : α | a ≤ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S) ∧ IsAtom a}

Tactic:
ext a
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
S : Set { a : α // IsAtom a }
h : ∀ a ∈ Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S, IsAtom a
a : α
⊢ Membership.mem (γ := Set α)
      (Set.image (α := { a : α // IsAtom a }) (Subtype.val (p := fun (a : α) ↦ IsAtom a))
        ((fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
          ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S)))
      a ↔
    Membership.mem (γ := Set α) {a : α | a ≤ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S) ∧ IsAtom a} a

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 α
a b : α
⊢ LE.le (α := Set { a : α // IsAtom a })
      (({ toFun := fun (A : α) ↦ {a : { a : α // IsAtom a } | (↑a : α) ≤ A},
              invFun := fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : α) → Set { a : α // IsAtom a })
          a :
        Set { a : α // IsAtom a })
      (({ toFun := fun (A : α) ↦ {a : { a : α // IsAtom a } | (↑a : α) ≤ A},
              invFun := fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : α) → Set { a : α // IsAtom a })
          b :
        Set { a : α // IsAtom a }) ↔
    a ≤ b

Tactic:
simpa using le_iff_atom_le_imp.symm

Premises used: le_iff_atom_le_imp, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
mp : IsSimpleOrder α → IsSimpleOrder.{u_2} αᵒᵈ
mpr : IsSimpleOrder.{u_2} αᵒᵈ → IsSimpleOrder α
⊢ IsSimpleOrder α ↔ IsSimpleOrder.{u_2} αᵒᵈ

Tactic:
constructor
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
i : IsSimpleOrder α
⊢ IsSimpleOrder.{u_2} αᵒᵈ

Tactic:
{ eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.ofDual a) : _ ∨ _) }

Premises used: IsSimpleOrder.mk, OrderDual.ofDual, Or.symm, DFunLike.coe, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
i : IsSimpleOrder α
⊢ IsSimpleOrder.{u_2} αᵒᵈ

Tactic:
exact
      { eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.ofDual a) : _ ∨ _) }
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
i : IsSimpleOrder.{u_2} αᵒᵈ
⊢ IsSimpleOrder α

Tactic:
{ exists_pair_ne := @exists_pair_ne αᵒᵈ _
        eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }

Premises used: OrderDual.toDual, IsSimpleOrder.mk, Or.symm, DFunLike.coe, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
i : IsSimpleOrder.{u_2} αᵒᵈ
⊢ IsSimpleOrder α

Tactic:
exact
      { exists_pair_ne := @exists_pair_ne αᵒᵈ _
        eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
obtain : ∀ (a b : α) (h : a ≠ b), Ne.{u_2 + 1} (α := α) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
obtain ⟨a, b, h⟩ := exists_pair_ne α

Premises used: exists_pair_ne
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
a b : α
h : a ≠ b
inl : ∀ (h : ⊥ ≠ b), Ne.{u_2 + 1} (α := α) ⊥ ⊤
inr : ∀ (h : ⊤ ≠ b), Ne.{u_2 + 1} (α := α) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
b : α
h : ⊥ ≠ b
inl : ∀ (h : Ne.{u_2 + 1} (α := α) ⊥ ⊥), Ne.{u_2 + 1} (α := α) ⊥ ⊤
inl₁ : ∀ (h : Ne.{u_2 + 1} (α := α) ⊥ ⊤), Ne.{u_2 + 1} (α := α) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
rcases eq_bot_or_eq_top b with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
b : α
h : ⊤ ≠ b
inr : ∀ (h : Ne.{u_2 + 1} (α := α) ⊤ ⊥), Ne.{u_2 + 1} (α := α) ⊥ ⊤
inr₁ : ∀ (h : Ne.{u_2 + 1} (α := α) ⊤ ⊤), Ne.{u_2 + 1} (α := α) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
rcases eq_bot_or_eq_top b with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
h : Ne.{u_2 + 1} (α := α) ⊥ ⊥
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
simpa using h.symm

Premises used: Ne.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
h : Ne.{u_2 + 1} (α := α) ⊥ ⊥
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
first | simpa | simpa using h.symm

Premises used: Ne.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
h : Ne.{u_2 + 1} (α := α) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
simpa
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
h : Ne.{u_2 + 1} (α := α) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
first | simpa | simpa using h.symm

Premises used: Ne.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
h : Ne.{u_2 + 1} (α := α) ⊤ ⊥
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
simpa using h.symm

Premises used: Ne.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
h : Ne.{u_2 + 1} (α := α) ⊤ ⊥
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
first | simpa | simpa using h.symm

Premises used: Ne.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
h : Ne.{u_2 + 1} (α := α) ⊤ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
simpa using h.symm

Premises used: Ne.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
h : Ne.{u_2 + 1} (α := α) ⊤ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤

Tactic:
first | simpa | simpa using h.symm

Premises used: Ne.symm
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
⊢ IsSimpleOrder α

Tactic:
infer_instance
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
a : α
inl : LE.le.{u_4} (α := α) ⊥ ⊥
inr : LE.le.{u_4} (α := α) ⊤ ⊤
⊢ a ≤ a

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
⊢ LE.le.{u_4} (α := α) ⊥ ⊥

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
⊢ LE.le.{u_4} (α := α) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
a b c : α
inl : ⊥ ≤ b → b ≤ c → ⊥ ≤ c
inr : ⊤ ≤ b → b ≤ c → ⊤ ≤ c
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
b c : α
⊢ ⊥ ≤ b → b ≤ c → ⊥ ≤ c

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
b c : α
inr : LE.le.{u_4} (α := α) ⊤ ⊥ → ⊥ ≤ c → ⊤ ≤ c
inr₁ : LE.le.{u_4} (α := α) ⊤ ⊤ → ⊤ ≤ c → ⊤ ≤ c
⊢ ⊤ ≤ b → b ≤ c → ⊤ ≤ c

Tactic:
rcases eq_bot_or_eq_top b with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
c : α
inr : LE.le.{u_4} (α := α) ⊤ ⊥ → LE.le.{u_4} (α := α) ⊥ ⊥ → LE.le.{u_4} (α := α) ⊤ ⊥
inr₁ : LE.le.{u_4} (α := α) ⊤ ⊥ → LE.le.{u_4} (α := α) ⊥ ⊤ → LE.le.{u_4} (α := α) ⊤ ⊤
⊢ LE.le.{u_4} (α := α) ⊤ ⊥ → ⊥ ≤ c → ⊤ ≤ c

Tactic:
rcases eq_bot_or_eq_top c with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
⊢ LE.le.{u_4} (α := α) ⊤ ⊥ → LE.le.{u_4} (α := α) ⊥ ⊥ → LE.le.{u_4} (α := α) ⊤ ⊥

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
⊢ LE.le.{u_4} (α := α) ⊤ ⊥ → LE.le.{u_4} (α := α) ⊥ ⊤ → LE.le.{u_4} (α := α) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
c : α
⊢ LE.le.{u_4} (α := α) ⊤ ⊤ → ⊤ ≤ c → ⊤ ≤ c

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
inst_3 : DecidableEq α
a b : α
inl : ⊥ ≤ b ∨ b ≤ ⊥
inr : ⊤ ≤ b ∨ b ≤ ⊤
⊢ a ≤ b ∨ b ≤ a

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
inst_3 : DecidableEq α
b : α
⊢ ⊥ ≤ b ∨ b ≤ ⊥

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
inst_3 : DecidableEq α
b : α
⊢ ⊤ ≤ b ∨ b ≤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ IsAtom.{u_2} (α := α) ⊤

Tactic:
⟨top_ne_bot, fun a ha => Or.resolve_right (eq_bot_or_eq_top a) (ne_of_lt ha)⟩

Premises used: top_ne_bot, And.intro, IsAtom, Or.resolve_right, ne_of_lt, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
a : α
⊢ IsAtom a ↔ a = ⊤

Tactic:
⟨fun h ↦ (eq_bot_or_eq_top a).resolve_left h.1, (· ▸ isAtom_top)⟩

Premises used: Eq.rec, Or.resolve_left, And.left, Iff.intro, isAtom_top, Eq.symm, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ IsCoatom.{u_2} (α := α) ⊥

Tactic:
isAtom_dual_iff_isCoatom.1 isAtom_top

Premises used: isAtom_dual_iff_isCoatom, Iff.mp, isAtom_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
a : α
⊢ IsCoatom a ↔ a = ⊥

Tactic:
⟨fun h ↦ (eq_bot_or_eq_top a).resolve_right h.1, (· ▸ isCoatom_bot)⟩

Premises used: isCoatom_bot, Eq.rec, And.left, Iff.intro, Or.resolve_right, Eq.symm, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ CovBy.{u_2} (α := α) ⊥ ⊤

Tactic:
isAtom_top.bot_covBy

Premises used: IsAtom.bot_covBy, isAtom_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
a b : α
h : a < b
⊢ a = ⊥

Tactic:
(IsSimpleOrder.eq_bot_or_eq_top _).resolve_right h.ne_top

Premises used: LT.lt.ne_top, Or.resolve_right, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
a b : α
h : a < b
⊢ b = ⊤

Tactic:
(IsSimpleOrder.eq_bot_or_eq_top _).resolve_left h.ne_bot

Premises used: Or.resolve_left, IsSimpleOrder.eq_bot_or_eq_top, LT.lt.ne_bot
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
x y z : α
inl : (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z
inr : (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
rcases eq_bot_or_eq_top x with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
y z : α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
y z : α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ IsAtomic α

Tactic:
⟨fun b => (eq_bot_or_eq_top b).imp_right fun h => ⟨⊤, ⟨isAtom_top, ge_of_eq h⟩⟩⟩

Premises used: ge_of_eq, And.intro, Exists.intro, isAtom_top, Top.top, IsAtomic.mk, Or.imp_right, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ IsAtomic.{u_2} αᵒᵈ

Tactic:
infer_instance
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : LE α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : α
inl :
  Eq.{u_4 + 1} (α := α)
    ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) ((fun (x : α) ↦ decide (x = ⊤)) ⊥)) ⊥
inr :
  Eq.{u_4 + 1} (α := α)
    ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) ((fun (x : α) ↦ decide (x = ⊤)) ⊤)) ⊤
⊢ (fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) ((fun (x : α) ↦ decide (x = ⊤)) x) = x

Tactic:
rcases eq_bot_or_eq_top x with (rfl | rfl)

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : LE α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
⊢ Eq.{u_4 + 1} (α := α)
    ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) ((fun (x : α) ↦ decide (x = ⊤)) ⊥)) ⊥

Tactic:
simp [bot_ne_top]

Premises used: IsSimpleOrder.bot_ne_top