awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
-- 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 : Bool
false :
  (fun (x : α) ↦ decide (x = ⊤))
      ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) Bool.false) =
    Bool.false
true :
  (fun (x : α) ↦ decide (x = ⊤))
      ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) Bool.true) =
    Bool.true
⊢ (fun (x : α) ↦ decide (x = ⊤)) ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) x) = x

Tactic:
cases x
-- 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 α
⊢ (fun (x : α) ↦ decide (x = ⊤)) ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) false) =
    false

Tactic:
simp [bot_ne_top]

Premises used: IsSimpleOrder.bot_ne_top
-- 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 α
⊢ (fun (x : α) ↦ decide (x = ⊤)) ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) true) =
    true

Tactic:
simp [bot_ne_top]

Premises used: IsSimpleOrder.bot_ne_top
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : PartialOrder α
inst_2 : BoundedOrder α
inst_3 : IsSimpleOrder α
a b : α
inl : LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊥ : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ ⊥ ≤ b
inr : LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ ⊤ ≤ b
⊢ LE.le (α := Bool) ((equivBool : (a : α) → Bool) a : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ a ≤ b

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 : DecidableEq α
inst_1 : PartialOrder α
inst_2 : BoundedOrder α
inst_3 : IsSimpleOrder α
b : α
⊢ LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊥ : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ ⊥ ≤ b

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

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
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : PartialOrder α
inst_2 : BoundedOrder α
inst_3 : IsSimpleOrder α
⊢ LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ((equivBool : (a : α) → Bool) ⊥ : Bool) ↔
    LE.le.{u_2} (α := α) ⊤ ⊥

Tactic:
simp [bot_ne_top.symm, Bool.false_lt_true]

Premises used: IsSimpleOrder.bot_ne_top, Ne.symm, Bool.false_lt_true
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : PartialOrder α
inst_2 : BoundedOrder α
inst_3 : IsSimpleOrder α
⊢ LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ↔
    LE.le.{u_2} (α := α) ⊤ ⊤

Tactic:
simp
-- 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 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : α
inl : LE.le.{u_4} (α := α) (⊥ ⊓ if Eq.{u_4 + 1} (α := α) ⊥ ⊥ then ⊤ else ⊥) ⊥
inr : LE.le.{u_4} (α := α) (⊤ ⊓ if Eq.{u_4 + 1} (α := α) ⊤ ⊥ then ⊤ else ⊥) ⊥
⊢ (x ⊓ if x = ⊥ then ⊤ else ⊥) ≤ ⊥

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 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
⊢ LE.le.{u_4} (α := α) (⊥ ⊓ if Eq.{u_4 + 1} (α := α) ⊥ ⊥ then ⊤ else ⊥) ⊥

Tactic:
simp
-- 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 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
⊢ LE.le.{u_4} (α := α) (⊤ ⊓ if Eq.{u_4 + 1} (α := α) ⊤ ⊥ then ⊤ else ⊥) ⊥

Tactic:
simp
-- 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 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : α
inl : LE.le.{u_4} (α := α) ⊤ (⊥ ⊔ if Eq.{u_4 + 1} (α := α) ⊥ ⊥ then ⊤ else ⊥)
inr : LE.le.{u_4} (α := α) ⊤ (⊤ ⊔ if Eq.{u_4 + 1} (α := α) ⊤ ⊥ then ⊤ else ⊥)
⊢ ⊤ ≤ x ⊔ if x = ⊥ then ⊤ else ⊥

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 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
⊢ LE.le.{u_4} (α := α) ⊤ (⊥ ⊔ if Eq.{u_4 + 1} (α := α) ⊥ ⊥ then ⊤ else ⊥)

Tactic:
simp
-- 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 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
⊢ LE.le.{u_4} (α := α) ⊤ (⊤ ⊔ if Eq.{u_4 + 1} (α := α) ⊤ ⊥ then ⊤ else ⊥)

Tactic:
simp
-- 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 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x y : α
inl : Eq.{u_4 + 1} (α := α) (if Eq.{u_4 + 1} (α := α) ⊥ ⊤ ∧ y = ⊥ then ⊤ else ⊥) (⊥ ⊓ if y = ⊥ then ⊤ else ⊥)
inr : Eq.{u_4 + 1} (α := α) (if Eq.{u_4 + 1} (α := α) ⊤ ⊤ ∧ y = ⊥ then ⊤ else ⊥) (⊤ ⊓ if y = ⊥ then ⊤ else ⊥)
⊢ (if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = x ⊓ if y = ⊥ then ⊤ else ⊥

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 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
y : α
⊢ Eq.{u_4 + 1} (α := α) (if Eq.{u_4 + 1} (α := α) ⊥ ⊤ ∧ y = ⊥ then ⊤ else ⊥) (⊥ ⊓ if y = ⊥ then ⊤ else ⊥)

Tactic:
simp
-- 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 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
y : α
⊢ Eq.{u_4 + 1} (α := α) (if Eq.{u_4 + 1} (α := α) ⊤ ⊤ ∧ y = ⊥ then ⊤ else ⊥) (⊤ ⊓ if y = ⊥ then ⊤ else ⊥)

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
⊢ IsLUB s (if ⊤ ∈ s then ⊤ else ⊥)

Tactic:
⟨fun x h ↦ ?_, fun x h ↦ ?_⟩

Premises used: IsLeast, And.intro, IsLUB
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
refine_1 : ∀ (x : α) (h : x ∈ s), x ≤ if ⊤ ∈ s then ⊤ else ⊥
refine_2 : ∀ (x : α) (h : x ∈ upperBounds s), (if ⊤ ∈ s then ⊤ else ⊥) ≤ x
⊢ IsLUB s (if ⊤ ∈ s then ⊤ else ⊥)

Tactic:
refine ⟨fun x h ↦ ?_, fun x h ↦ ?_⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
refine_1 : ∀ (h : ⊥ ∈ s), LE.le.{u_2} (α := α) ⊥ (if ⊤ ∈ s then ⊤ else ⊥)
refine_1₁ : ∀ (h : ⊤ ∈ s), LE.le.{u_2} (α := α) ⊤ (if ⊤ ∈ s then ⊤ else ⊥)
⊢ x ≤ if ⊤ ∈ s then ⊤ else ⊥

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 α
s : Set α
h : ⊥ ∈ s
⊢ LE.le.{u_2} (α := α) ⊥ (if ⊤ ∈ s then ⊤ else ⊥)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊥ ∈ s
⊢ LE.le.{u_2} (α := α) ⊥ (if ⊤ ∈ s then ⊤ else ⊥)

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
refine_1 refine_1₁ : LE.le.{u_2} (α := α) ⊤ ⊤
⊢ LE.le.{u_2} (α := α) ⊤ (if ⊤ ∈ s then ⊤ else ⊥)

Tactic:
rw [if_pos h]

Premises used: if_pos
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ upperBounds s
refine_2 : ∀ (h : ⊥ ∈ upperBounds s), LE.le.{u_2} (α := α) (if ⊤ ∈ s then ⊤ else ⊥) ⊥
refine_2₁ : ∀ (h : ⊤ ∈ upperBounds s), LE.le.{u_2} (α := α) (if ⊤ ∈ s then ⊤ else ⊥) ⊤
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ 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
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
refine_2 : ⊤ ∉ s
⊢ LE.le.{u_2} (α := α) (if ⊤ ∈ s then ⊤ else ⊥) ⊥

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
con : ⊤ ∈ s
⊢ False

Tactic:
bot_ne_top (eq_top_iff.2 (h con))

Premises used: Iff.mpr, eq_top_iff, IsSimpleOrder.bot_ne_top
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
con : ⊤ ∈ s
⊢ False

Tactic:
exact bot_ne_top (eq_top_iff.2 (h con))

Premises used: Iff.mpr, eq_top_iff, IsSimpleOrder.bot_ne_top
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ upperBounds s
⊢ LE.le.{u_2} (α := α) (if ⊤ ∈ s then ⊤ else ⊥) ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ upperBounds s
⊢ LE.le.{u_2} (α := α) (if ⊤ ∈ s then ⊤ else ⊥) ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
⊢ IsGLB s (if ⊥ ∈ s then ⊥ else ⊤)

Tactic:
⟨fun x h ↦ ?_, fun x h ↦ ?_⟩

Premises used: IsGreatest, IsGLB, And.intro
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
refine_1 : ∀ (x : α) (h : x ∈ s), (if ⊥ ∈ s then ⊥ else ⊤) ≤ x
refine_2 : ∀ (x : α) (h : x ∈ lowerBounds s), x ≤ if ⊥ ∈ s then ⊥ else ⊤
⊢ IsGLB s (if ⊥ ∈ s then ⊥ else ⊤)

Tactic:
refine ⟨fun x h ↦ ?_, fun x h ↦ ?_⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
refine_1 : ∀ (h : ⊥ ∈ s), LE.le.{u_2} (α := α) (if ⊥ ∈ s then ⊥ else ⊤) ⊥
refine_1₁ : ∀ (h : ⊤ ∈ s), LE.le.{u_2} (α := α) (if ⊥ ∈ s then ⊥ else ⊤) ⊤
⊢ (if ⊥ ∈ s then ⊥ else ⊤) ≤ 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
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊥ ∈ s
refine_1 refine_1₁ : LE.le.{u_2} (α := α) ⊥ ⊥
⊢ LE.le.{u_2} (α := α) (if ⊥ ∈ s then ⊥ else ⊤) ⊥

Tactic:
rw [if_pos h]

Premises used: if_pos
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
⊢ LE.le.{u_2} (α := α) (if ⊥ ∈ s then ⊥ else ⊤) ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
⊢ LE.le.{u_2} (α := α) (if ⊥ ∈ s then ⊥ else ⊤) ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ lowerBounds s
refine_2 : ∀ (h : ⊥ ∈ lowerBounds s), LE.le.{u_2} (α := α) ⊥ (if ⊥ ∈ s then ⊥ else ⊤)
refine_2₁ : ∀ (h : ⊤ ∈ lowerBounds s), LE.le.{u_2} (α := α) ⊤ (if ⊥ ∈ s then ⊥ else ⊤)
⊢ x ≤ if ⊥ ∈ s then ⊥ else ⊤

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 α
s : Set α
h : ⊥ ∈ lowerBounds s
⊢ LE.le.{u_2} (α := α) ⊥ (if ⊥ ∈ s then ⊥ else ⊤)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊥ ∈ lowerBounds s
⊢ LE.le.{u_2} (α := α) ⊥ (if ⊥ ∈ s then ⊥ else ⊤)

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
refine_2 : ⊥ ∉ s
⊢ LE.le.{u_2} (α := α) ⊤ (if ⊥ ∈ s then ⊥ else ⊤)

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
con : ⊥ ∈ s
⊢ False

Tactic:
top_ne_bot (eq_bot_iff.2 (h con))

Premises used: Iff.mpr, top_ne_bot, eq_bot_iff
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
con : ⊥ ∈ s
⊢ False

Tactic:
exact top_ne_bot (eq_bot_iff.2 (h con))

Premises used: Iff.mpr, top_ne_bot, eq_bot_iff
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ ComplementedLattice α

Tactic:
letI := IsSimpleOrder.completeBooleanAlgebra (α := α); inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
b : α
h : b = ⊥
⊢ IsLUB ∅ b ∧ ∀ (a : α), Membership.mem (γ := Set α) ∅ a → IsAtom a

Tactic:
simp [h]
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
b : α
h : b = ⊤
⊢ IsLUB {⊤} b ∧ ∀ (a : α), Membership.mem (γ := Set α) {⊤} a → IsAtom a

Tactic:
simp [h]
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ IsAtomistic.{u_2} αᵒᵈ

Tactic:
infer_instance
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
a : α
⊢ ⊥ < a ↔ a = ⊤

Tactic:
⟨eq_top_of_lt, fun h ↦ h ▸ bot_lt_top⟩

Premises used: Eq.rec, bot_lt_top, Iff.intro, IsSimpleOrder.eq_top_of_lt, Eq.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
a : α
⊢ a < ⊤ ↔ a = ⊥

Tactic:
⟨eq_bot_of_lt, fun h ↦ h ▸ bot_lt_top⟩

Premises used: Eq.rec, bot_lt_top, Iff.intro, IsSimpleOrder.eq_bot_of_lt, Eq.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : BoundedOrder α
⊢ IsSimpleOrder α ↔ IsAtom.{u_2} (α := α) ⊤

Tactic:
⟨fun h => @isAtom_top _ _ _ h, fun h =>
    { exists_pair_ne := ⟨⊤, ⊥, h.1⟩
      eq_bot_or_eq_top := fun a => ((eq_or_lt_of_le le_top).imp_right (h.2 a)).symm }⟩

Premises used: IsSimpleOrder.mk, eq_or_lt_of_le, Or.symm, And.right, le_top, Iff.intro, isAtom_top, Or.imp_right
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : BoundedOrder α
⊢ IsSimpleOrder α ↔ IsCoatom.{u_2} (α := α) ⊥

Tactic:
isSimpleOrder_iff_isSimpleOrder_orderDual.trans isSimpleOrder_iff_isAtom_top

Premises used: isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isSimpleOrder_orderDual, Iff.trans
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a : α
⊢ IsSimpleOrder.{u_2} (↑(Iic a) : Type u_2) ↔ IsAtom a

Tactic:
isSimpleOrder_iff_isAtom_top.trans <|
    and_congr (not_congr Subtype.mk_eq_mk)
      ⟨fun h b ab => Subtype.mk_eq_mk.1 (h ⟨b, le_of_lt ab⟩ ab), fun h ⟨b, _⟩ hbotb =>
        Subtype.mk_eq_mk.2 (h b (Subtype.mk_lt_mk.1 hbotb))⟩

Premises used: Iff.mpr, isSimpleOrder_iff_isAtom_top, le_of_lt, Subtype.mk_lt_mk, Bot.bot, _private.0.Set.isSimpleOrder_Iic_iff_isAtom.match_1, Subtype.mk, Iff.intro, Subtype.mk_eq_mk, Iff.mp, Iff.trans, Eq, not_congr, and_congr
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ IsSimpleOrder.{u_2} (↑(Ici a) : Type u_2) ↔ IsCoatom a

Tactic:
isSimpleOrder_iff_isCoatom_bot.trans <|
    and_congr (not_congr Subtype.mk_eq_mk)
      ⟨fun h b ab => Subtype.mk_eq_mk.1 (h ⟨b, le_of_lt ab⟩ ab), fun h ⟨b, _⟩ hbotb =>
        Subtype.mk_eq_mk.2 (h b (Subtype.mk_lt_mk.1 hbotb))⟩

Premises used: Iff.mpr, le_of_lt, Subtype.mk_lt_mk, Subtype.mk, isSimpleOrder_iff_isCoatom_bot, Iff.intro, Subtype.mk_eq_mk, Iff.mp, Iff.trans, Top.top, Eq, not_congr, and_congr, _private.0.Set.isSimpleOrder_Ici_iff_isCoatom.match_1
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
f : β ↪o α
hbot : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) ⊥ : α) (⊥ : α)
b : β
hb : IsAtom.{u_2} (α := α) ((f : (a : β) → α) b : α)
simp : ∀ (hb : CovBy.{u_2} (α := α) (⊥ : α) ((f : (a : β) → α) b : α)), ⊥ ⋖ b
⊢ IsAtom b

Tactic:
simp only [← bot_covBy_iff] at hb ⊢

Premises used: bot_covBy_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
f : β ↪o α
hbot : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) ⊥ : α) (⊥ : α)
b : β
hb : CovBy.{u_2} (α := α) (⊥ : α) ((f : (a : β) → α) b : α)
⊢ ⊥ ⋖ b

Tactic:
CovBy.of_image f (hbot.symm ▸ hb)

Premises used: Eq.rec, Eq.symm, CovBy.of_image
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
f : β ↪o α
hbot : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) ⊥ : α) (⊥ : α)
b : β
hb : CovBy.{u_2} (α := α) (⊥ : α) ((f : (a : β) → α) b : α)
⊢ ⊥ ⋖ b

Tactic:
exact CovBy.of_image f (hbot.symm ▸ hb)

Premises used: CovBy.of_image
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : OrderTop β
f : β ↪o α
htop : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) ⊤ : α) (⊤ : α)
b : β
hb : IsCoatom.{u_2} (α := α) ((f : (a : β) → α) b : α)
⊢ IsCoatom b

Tactic:
f.dual.isAtom_of_map_bot_of_image htop hb

Premises used: IsCoatom, OrderEmbedding.isAtom_of_map_bot_of_image, OrderDual, OrderEmbedding.dual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
b : β
hb : IsAtom (u b)
⊢ IsAtom b

Tactic:
OrderEmbedding.isAtom_of_map_bot_of_image
    ⟨⟨u, gi.u_injective⟩, @GaloisInsertion.u_le_u_iff _ _ _ _ _ _ gi⟩ hbot hb

Premises used: RelEmbedding.mk, Function.Embedding.mk, GaloisInsertion.u_injective, OrderEmbedding.isAtom_of_map_bot_of_image, GaloisInsertion.u_le_u_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
⊢ IsAtom (l a) ↔ IsAtom a

Tactic:
⟨fun hla => ?_, fun ha => gi.isAtom_of_u_bot hbot ((h_atom a ha).symm ▸ ha)⟩

Premises used: Eq.rec, Iff.intro, GaloisInsertion.isAtom_of_u_bot, Eq.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
refine : ∀ (hla : IsAtom (l a)), IsAtom a
⊢ IsAtom (l a) ↔ IsAtom a

Tactic:
refine ⟨fun hla => ?_, fun ha => gi.isAtom_of_u_bot hbot ((h_atom a ha).symm ▸ ha)⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
obtain : ∀ (a' : α) (ha' : IsAtom a') (hab' : a' ≤ u (l a)), IsAtom a
⊢ IsAtom a

Tactic:
obtain ⟨a', ha', hab'⟩ :=
    (eq_bot_or_exists_atom_le (u (l a))).resolve_left (hbot ▸ fun h => hla.1 (gi.u_injective h))

Premises used: IsAtomic.eq_bot_or_exists_atom_le, Eq.rec, Or.resolve_left, GaloisInsertion.u_injective, And.left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
⊢ l a' = l a

Tactic:
have :=
    (hla.le_iff.mp <| (gi.l_u_eq (l a) ▸ gi.gc.monotone_l hab' : l a' ≤ l a)).resolve_left fun h =>
      ha'.1 (hbot ▸ h_atom a' ha' ▸ congr_arg u h)