awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeInf α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (s ∩ {b : α | ¬a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
@bounded_le_inter_not_le αᵒᵈ s _ a

Premises used: Set.bounded_le_inter_not_le, setOf, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeInf α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (s ∩ {b : α | ¬a ≤ b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
@unbounded_le_inter_not_le αᵒᵈ s _ a

Premises used: Set.unbounded_le_inter_not_le, setOf, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (s ∩ {b : α | b < a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
@bounded_le_inter_lt αᵒᵈ s _ a

Premises used: setOf, Set.bounded_le_inter_lt, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (s ∩ {b : α | b < a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
@unbounded_le_inter_lt αᵒᵈ s _ a

Premises used: setOf, Set.unbounded_le_inter_lt, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (s ∩ {b : α | b ≤ a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
@bounded_le_inter_le αᵒᵈ s _ a

Premises used: setOf, Set.bounded_le_inter_le, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (s ∩ {b : α | b ≤ a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
@unbounded_le_inter_le αᵒᵈ s _ a

Premises used: Set.unbounded_le_inter_le, setOf, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeInf α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 > x2) (s ∩ {b : α | ¬a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 > x2) s

Tactic:
@bounded_lt_inter_not_lt αᵒᵈ s _ a

Premises used: Set.bounded_lt_inter_not_lt, setOf, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeInf α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) (s ∩ {b : α | ¬a < b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) s

Tactic:
@unbounded_lt_inter_not_lt αᵒᵈ s _ a

Premises used: setOf, Set.unbounded_lt_inter_not_lt, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 > x2) (s ∩ {b : α | b ≤ a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 > x2) s

Tactic:
@bounded_lt_inter_le αᵒᵈ s _ a

Premises used: setOf, OrderDual, Set.bounded_lt_inter_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) (s ∩ {b : α | b ≤ a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) s

Tactic:
@unbounded_lt_inter_le αᵒᵈ s _ a

Premises used: Set.unbounded_lt_inter_le, setOf, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMinOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 > x2) (s ∩ {b : α | b < a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 > x2) s

Tactic:
@bounded_lt_inter_lt αᵒᵈ s _ _ a

Premises used: setOf, Set.bounded_lt_inter_lt, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMinOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) (s ∩ {b : α | b < a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) s

Tactic:
@unbounded_lt_inter_lt αᵒᵈ s _ _ a

Premises used: setOf, OrderDual, Set.unbounded_lt_inter_lt
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : LE α
pos : (H : ∀ (a : α), ∃ (b : α), ¬b ≤ a) → OrderTop α ⊕' NoTopOrder α
neg : (H : ∃ (a : α), ∀ (b : α), b ≤ a) → OrderTop α ⊕' NoTopOrder α
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
by_cases! H : ∀ a : α, ∃ b, ¬b ≤ a
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : LE α
H : ∀ (a : α), ∃ (b : α), ¬b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
exact PSum.inr ⟨H⟩

Premises used: PSum.inr
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : LE α
H : ∃ (a : α), ∀ (b : α), b ≤ a
this : Top α := { top := Classical.choose (p := fun (x : α) ↦ ∀ (b : α), b ≤ x) H }
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
exact PSum.inl ⟨Classical.choose_spec H⟩

Premises used: PSum.inl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Top α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
isTrue : ∀ (h : p), a h ≠ ⊤
isFalse : ∀ (h : ¬p), b h ≠ ⊤
⊢ Ne.{u + 1} (α := α) (if h : p then a h else b h) ⊤

Tactic:
split
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Top α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h : p
⊢ a h ≠ ⊤

Tactic:
solve_by_elim
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Top α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h : ¬p
⊢ b h ≠ ⊤

Tactic:
solve_by_elim
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Top α
p : Prop
inst_1 : Decidable p
a b : α
ha : p → a ≠ ⊤
hb : ¬p → b ≠ ⊤
⊢ (if p then a else b) ≠ ⊤

Tactic:
dite_ne_top ha hb

Premises used: dite_ne_top, ite
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : LE α
inst_1 : OrderTop α
a : α
⊢ a ≤ ⊤

Tactic:
OrderTop.le_top a

Premises used: OrderTop.le_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : LE α
inst_1 : OrderTop α
⊢ IsTop.{u} (α := α) ⊤

Tactic:
fun _ => le_top

Premises used: le_top, IsTop
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : LE α
P : (x : α) → IsTop x → Sort u_1
h : [inst_1 : OrderTop α] → P ⊤ ⋯
x : α
hx : IsTop x
letI : P x hx
⊢ P x hx

Tactic:
letI : OrderTop α := { top := x, le_top := hx }
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : LE α
P : (x : α) → IsTop x → Sort u_1
h : [inst_1 : OrderTop α] → P ⊤ ⋯
x : α
hx : IsTop x
this : OrderTop α := { top := x, le_top := hx }
⊢ P x hx

Tactic:
apply h
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
⊢ IsMax.{u} (α := α) ⊤

Tactic:
isTop_top.isMax

Premises used: IsTop.isMax, isTop_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ ¬⊤ < a

Tactic:
isMax_top.not_lt

Premises used: isMax_top, IsMax.not_lt
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ ¬⊤ ⋖ a

Tactic:
fun h ↦ not_top_lt h.1

Premises used: not_top_lt, And.left, Not
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
a b : α
h : a < b
⊢ a ≠ ⊤

Tactic:
(h.trans_le le_top).ne

Premises used: LT.lt.trans_le, le_top, LT.lt.ne
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
a b : α
h : a < b
⊢ a < ⊤

Tactic:
lt_of_lt_of_le h le_top

Premises used: le_top, lt_of_lt_of_le
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ a < ⊤ ↔ ¬⊤ ≤ a

Tactic:
simp [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
a : α
rw : (∃ (b : α), a < b) ↔ a < ⊤
⊢ ¬IsMax a ↔ a < ⊤

Tactic:
rw [not_isMax_iff]

Premises used: not_isMax_iff
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ (∃ (b : α), a < b) ↔ a < ⊤

Tactic:
⟨fun ⟨b, hb⟩ ↦ hb.trans_le le_top, fun h ↦ ⟨⊤, h⟩⟩

Premises used: LT.lt.trans_le, le_top, LT.lt, Iff.intro, Exists.intro, _private.0.not_isMax_iff_lt_top.match_1, Top.top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ (∃ (b : α), a < b) ↔ a < ⊤

Tactic:
exact ⟨fun ⟨b, hb⟩ ↦ hb.trans_le le_top, fun h ↦ ⟨⊤, h⟩⟩
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ IsMax a ↔ a = ⊤

Tactic:
⟨fun h => h.eq_of_le le_top, fun h _ _ => h.symm ▸ le_top⟩

Premises used: Eq.rec, le_top, Iff.intro, IsMax.eq_of_le, Eq.symm
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ IsTop a ↔ a = ⊤

Tactic:
⟨fun h => h.isMax.eq_of_le le_top, fun h _ => h.symm ▸ le_top⟩

Premises used: Eq.rec, le_top, IsTop.isMax, Iff.intro, IsMax.eq_of_le, Eq.symm
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ ¬IsMax a ↔ a ≠ ⊤

Tactic:
isMax_iff_eq_top.not

Premises used: isMax_iff_eq_top, Iff.not
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ ¬IsTop a ↔ a ≠ ⊤

Tactic:
isTop_iff_eq_top.not

Premises used: Iff.not, isTop_iff_eq_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ ⊤ ≤ a ↔ a = ⊤

Tactic:
le_top.ge_iff_eq

Premises used: le_top, LE.le.ge_iff_eq
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
h : ⊤ ≤ a
⊢ a = ⊤

Tactic:
le_top.antisymm h

Premises used: LE.le.antisymm, le_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ a = ⊤ ↔ ⊤ ≤ a

Tactic:
top_le_iff.symm

Premises used: top_le_iff, Iff.symm
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a b : α
h : a ≤ b
h₂ : a = ⊤
⊢ b = ⊤

Tactic:
top_unique <| h₂ ▸ h

Premises used: Eq.rec, top_unique
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ a < ⊤ ↔ a ≠ ⊤

Tactic:
le_top.lt_iff_ne

Premises used: le_top, LE.le.lt_iff_ne
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ ¬a < ⊤ ↔ a = ⊤

Tactic:
lt_top_iff_ne_top.not_left

Premises used: lt_top_iff_ne_top, Iff.not_left
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ a = ⊤ ∨ a < ⊤

Tactic:
le_top.eq_or_lt

Premises used: LE.le.eq_or_lt, le_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
h : a ≠ ⊤
⊢ a < ⊤

Tactic:
lt_top_iff_ne_top.mpr h

Premises used: Iff.mpr, lt_top_iff_ne_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a : α
h : ⊤ ≠ a
⊢ a < ⊤

Tactic:
h.symm.lt_top

Premises used: Ne.symm, Ne.lt_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
a b : α
hb : b ≠ ⊤
hab : a ≤ b
⊢ a ≠ ⊤

Tactic:
(hab.trans_lt hb.lt_top).ne

Premises used: Ne.lt_top, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
s : Set α
⊢ ¬⊤ ∈ s ↔ ∀ (x : α), x ∈ s → x < ⊤

Tactic:
⟨fun h x hx ↦ Ne.lt_top (fun hx' : x = ⊤ ↦ h (hx' ▸ hx)), fun h h₀ ↦ (h ⊤ h₀).false⟩

Premises used: Eq.rec, Ne.lt_top, Iff.intro, LT.lt.false, Top.top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : Nontrivial α
⊢ ¬IsMin.{u} (α := α) ⊤

Tactic:
fun h =>
  let ⟨_, ha⟩ := exists_ne (⊤ : α)
  ha <| top_le_iff.1 <| h le_top

Premises used: False, _private.0.not_isMin_top.match_1, exists_ne, le_top, top_le_iff, Iff.mp, Top.top, Not
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u_1
hA : PartialOrder α
A : OrderTop α
hB : PartialOrder α
B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
refl : ∀ (B : OrderTop α) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y), Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ Eq.{u_1 + 1} (α := α) ⊤ ⊤

Tactic:
cases PartialOrder.ext H

Premises used: PartialOrder.ext
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
refl : LE.le.{u_1} (α := α) ⊤ ⊤
⊢ Eq.{u_1 + 1} (α := α) ⊤ ⊤

Tactic:
apply top_unique

Premises used: top_unique
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ LE.le.{u_1} (α := α) ⊤ ⊤

Tactic:
@le_top _ _ A _

Premises used: OrderTop.le_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ LE.le.{u_1} (α := α) ⊤ ⊤

Tactic:
exact @le_top _ _ A _

Premises used: OrderTop.le_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Bot α
⊢ Eq.{u + 1} (α := α) ((ofDual : (a : αᵒᵈ) → α) ⊤ : α) (⊥ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Top α
⊢ Eq.{u + 1} (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) ⊤ : αᵒᵈ) (⊥ : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Top α
a : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) (⊤ : α) ↔ a = ⊥

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Bot α
a : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) (⊤ : αᵒᵈ) ↔ a = ⊥

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : OrderBot α
a : α
h : ∀ (b : α), ¬b < a
⊢ a = ⊥

Tactic:
(eq_bot_or_bot_lt a).resolve_right (h ⊥)

Premises used: Bot.bot, eq_bot_or_bot_lt, Or.resolve_right
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
e_toBot : a = b
⊢ { bot := a, bot_le := ha : OrderBot α } = { bot := b, bot_le := hb }

Tactic:
congr
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ a = b

Tactic:
le_antisymm (ha _) (hb _)

Premises used: le_antisymm
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ a = b

Tactic:
exact le_antisymm (ha _) (hb _)

Premises used: le_antisymm
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder α
toOrderTop : OrderTop α
toOrderBot : OrderBot α
toOrderTop_1 : OrderTop α
toOrderBot_1 : OrderBot α
e_toOrderTop : toOrderTop = toOrderTop_1
e_toOrderBot : toOrderBot = toOrderBot_1
⊢ Eq.{u + 1} (α := BoundedOrder α) { toOrderTop := toOrderTop, toOrderBot := toOrderBot }
    { toOrderTop := toOrderTop_1, toOrderBot := toOrderBot_1 }

Tactic:
congr
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder α
toOrderTop : OrderTop α
toOrderBot : OrderBot α
toOrderTop_1 : OrderTop α
toOrderBot_1 : OrderBot α
⊢ toOrderTop = toOrderTop_1

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder α
toOrderTop : OrderTop α
toOrderBot : OrderBot α
toOrderTop_1 : OrderTop α
toOrderBot_1 : OrderBot α
⊢ toOrderTop = toOrderTop_1

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder α
toOrderTop : OrderTop α
toOrderBot : OrderBot α
toOrderTop_1 : OrderTop α
toOrderBot_1 : OrderBot α
⊢ toOrderBot = toOrderBot_1

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder α
toOrderTop : OrderTop α
toOrderBot : OrderBot α
toOrderTop_1 : OrderTop α
toOrderBot_1 : OrderBot α
⊢ toOrderBot = toOrderBot_1

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
ι : Type u_1
α' : ι → Type u_2
inst : (i : ι) → Bot (α' i)
i : ι
⊢ Eq.{u_2 + 1} (α := α' i) (⊥ i) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
ι : Type u_1
α' : ι → Type u_2
inst : (i : ι) → Bot (α' i)
⊢ Eq (α := (i : ι) → α' i) ⊥ fun (x : ι) ↦ ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Bot γ
x : α → β
⊢ Eq (α := α → γ) (⊥ ∘ x) ⊥

Tactic:
rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Preorder α
inst_1 : Unique α
⊢ ∀ (a : α), a ≤ default

Tactic:
simp
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Preorder α
inst_1 : Unique α
⊢ ∀ (a : α), default ≤ a

Tactic:
simp
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : BoundedOrder α
hα : Eq.{u + 1} (α := α) ⊥ ⊤
x : α
⊢ x = ⊥

Tactic:
eq_bot_mono le_top (Eq.symm hα)

Premises used: le_top, eq_bot_mono, Eq.symm
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : BoundedOrder α
hα : Eq.{u + 1} (α := α) ⊥ ⊤
x : α
⊢ x = ⊤

Tactic:
eq_top_mono bot_le hα

Premises used: eq_top_mono, bot_le
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : BoundedOrder α
h : LE.le.{u} (α := α) ⊤ ⊥
⊢ Subsingleton α

Tactic:
⟨fun _ _ => le_antisymm
    (le_trans le_top <| le_trans h bot_le) (le_trans le_top <| le_trans h bot_le)⟩

Premises used: le_antisymm, Subsingleton.intro, le_top, bot_le, le_trans
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : BoundedOrder α
hα : Eq.{u + 1} (α := α) ⊥ ⊤
⊢ Subsingleton α

Tactic:
subsingleton_of_top_le_bot (ge_of_eq hα)

Premises used: subsingleton_of_top_le_bot, ge_of_eq
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : BoundedOrder α
⊢ Eq.{u + 1} (α := α) ⊥ ⊤ ↔ Subsingleton α

Tactic:
⟨subsingleton_of_bot_eq_top, fun _ => Subsingleton.elim ⊥ ⊤⟩

Premises used: Bot.bot, subsingleton_of_bot_eq_top, Iff.intro, Subsingleton.elim, Top.top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : LE α
inst_1 : Top α
inst_2 : LE β
inst_3 : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
rw : f a ≤ ⊤
⊢ f a ≤ f ⊤

Tactic:
rw [map_top]
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : LE α
inst_1 : Top α
inst_2 : LE β
inst_3 : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ ⊤

Tactic:
le_top _

Premises used: OrderTop.le_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : LE α
inst_1 : Top α
inst_2 : LE β
inst_3 : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ ⊤

Tactic:
exact le_top _

Premises used: OrderTop.le_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
p : α → Prop
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : OrderBot (Subtype p)
hbot : p ⊥
⊢ mk (p := p) ⊥ hbot = ⊥

Tactic:
le_bot_iff.1 <| coe_le_coe.1 bot_le

Premises used: le_bot_iff, Subtype.coe_le_coe, Iff.mp, bot_le
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
p : α → Prop
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : OrderBot (Subtype p)
hbot : p ⊥
⊢ Eq.{u + 1} (α := α) (↑⊥ : α) ⊥

Tactic:
congr_arg Subtype.val (mk_bot hbot).symm

Premises used: congr_arg, Subtype.mk_bot, Eq.symm, Subtype.val
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
p : α → Prop
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : OrderBot (Subtype p)
hbot : p ⊥
x : { x : α // p x }
rw : (↑x : α) = (↑⊥ : α) ↔ x = ⊥
rw₁ rw₂ : (↑x : α) = (↑⊥ : α) ↔ (↑x : α) = (↑⊥ : α)
⊢ (↑x : α) = ⊥ ↔ x = ⊥

Tactic:
rw [← coe_bot hbot, Subtype.ext_iff]

Premises used: Subtype.coe_bot, Subtype.ext_iff
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
p : α → Prop
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : OrderBot (Subtype p)
hbot : p ⊥
x : α
hx : p x
⊢ mk (p := p) x hx = ⊥ ↔ x = ⊥

Tactic:
(coe_eq_bot_iff hbot).symm

Premises used: Iff.symm, Subtype.coe_eq_bot_iff
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : Top α
inst_1 : Top β
⊢ Eq.{u + 1} (α := α) (fst.{u, v} (β := β) ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
β : Type v
inst : Top α
inst_1 : Top β
⊢ Eq.{v + 1} (α := β) (snd.{u, v} (α := α) ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Top α
⊢ Eq (α := ULift.{u_1, u} α) { down := ⊤ } ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : Top α
⊢ Eq.{u + 1} (α := α) (down.{u_1, u} ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : Nontrivial α
⊢ Ne.{u + 1} (α := α) ⊥ ⊤

Tactic:
fun h => not_subsingleton _ <| subsingleton_of_bot_eq_top h

Premises used: subsingleton_of_bot_eq_top, not_subsingleton, Not
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
α : Type u
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : Nontrivial α
⊢ LT.lt.{u} (α := α) ⊥ ⊤

Tactic:
lt_top_iff_ne_top.2 bot_ne_top

Premises used: Iff.mpr, lt_top_iff_ne_top, bot_ne_top
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
⊢ ⊤ = true

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Basic
Goal:
⊢ ⊥ = false

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderTop α
a : α
⊢ ⊤ ⊔ a = ⊤

Tactic:
sup_of_le_left le_top

Premises used: le_top, sup_of_le_left
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderTop α
a : α
⊢ a ⊔ ⊤ = ⊤

Tactic:
sup_of_le_right le_top

Premises used: sup_of_le_right, le_top
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
a : α
⊢ ⊥ ⊔ a = a

Tactic:
sup_of_le_right bot_le

Premises used: sup_of_le_right, bot_le
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
a : α
⊢ a ⊔ ⊥ = a

Tactic:
sup_of_le_left bot_le

Premises used: sup_of_le_left, bot_le
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
a b : α
rw : a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
⊢ a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

Tactic:
rw [eq_bot_iff, sup_le_iff]

Premises used: sup_le_iff, eq_bot_iff
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
a b : α
⊢ a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥

Tactic:
simp
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a : α
⊢ min ⊥ a = ⊥

Tactic:
bot_inf_eq _

Premises used: bot_inf_eq
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a : α
⊢ min a ⊥ = ⊥

Tactic:
inf_bot_eq _

Premises used: inf_bot_eq
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a : α
⊢ max ⊥ a = a

Tactic:
bot_sup_eq _

Premises used: bot_sup_eq
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a : α
⊢ max a ⊥ = a

Tactic:
sup_bot_eq _

Premises used: sup_bot_eq
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a b : α
⊢ max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥

Tactic:
sup_eq_bot_iff

Premises used: sup_eq_bot_iff
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a b : α
simp_rw : min a b ≤ ⊥ ↔ a ≤ ⊥ ∨ b ≤ ⊥
⊢ min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Tactic:
simp_rw [← le_bot_iff, inf_le_iff]

Premises used: le_bot_iff, inf_le_iff
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a b : α
ha : a ≠ ⊥
hb : b ≠ ⊥
⊢ min a b ≠ ⊥

Tactic:
grind