awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
a_1 : α
⊢ (↑a_1 : WithTop α) < ⊤ ∨ (↑a_1 : WithTop α) = ⊤ ∨ ⊤ < (↑a_1 : WithTop α)

Tactic:
simp [trichotomous]

Premises used: trichotomous
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
a_1 a_2 : α
⊢ (↑a_1 : WithTop α) < (↑a_2 : WithTop α) ∨
    (↑a_1 : WithTop α) = (↑a_2 : WithTop α) ∨ (↑a_2 : WithTop α) < (↑a_1 : WithTop α)

Tactic:
simp [trichotomous]

Premises used: trichotomous
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 > x2
⊢ Std.Trichotomous fun (x1 x2 : WithBot α) ↦ x1 > x2

Tactic:
have : @Std.Trichotomous α (· < ·) := inferInstanceAs <| Std.Trichotomous <| Function.swap _
  inferInstance

Premises used: inferInstance, _private.0.WithBot.trichotomous.gt._proof_1
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 > x2
⊢ Std.Trichotomous fun (x1 x2 : WithTop α) ↦ x1 > x2

Tactic:
have : @Std.Trichotomous α (· < ·) := inferInstanceAs <| Std.Trichotomous <| Function.swap _
  inferInstance

Premises used: inferInstance, _private.0.WithBot.trichotomous.gt._proof_1
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (↑(min a b) : WithBot α) = min (↑a : WithBot α) (↑b : WithBot α)

Tactic:
rfl

Premises used: WithBot.some, WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (↑(max a b) : WithBot α) = max (↑a : WithBot α) (↑b : WithBot α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
bot : (∀ (z : α), ⊥ < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ ⊥
coe : ∀ (a : α), (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ (↑a : WithBot α)
⊢ (∀ (z : α), x < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
bot : (∀ (z : α), ⊥ < (↑z : WithBot α) → ⊥ ≤ (↑z : WithBot α)) ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), (∀ (z : α), ⊥ < (↑z : WithBot α) → (↑a : WithBot α) ≤ (↑z : WithBot α)) ↔ (↑a : WithBot α) ≤ ⊥
⊢ (∀ (z : α), ⊥ < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ ⊥

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
coe : (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → ⊥ ≤ (↑z : WithBot α)) ↔ ⊥ ≤ (↑a : WithBot α)
coe₁ :
  ∀ (a_1 : α),
    (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → (↑a_1 : WithBot α) ≤ (↑z : WithBot α)) ↔
      (↑a_1 : WithBot α) ≤ (↑a : WithBot α)
⊢ (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → y ≤ (↑z : WithBot α)) ↔ y ≤ (↑a : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
⊢ (∀ (z : α), ⊥ < (↑z : WithBot α) → ⊥ ≤ (↑z : WithBot α)) ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

Premises used: forall_gt_imp_ge_iff_le_of_dense, NoMinOrder.exists_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
⊢ (∀ (z : α), ⊥ < (↑z : WithBot α) → (↑a : WithBot α) ≤ (↑z : WithBot α)) ↔ (↑a : WithBot α) ≤ ⊥

Tactic:
simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

Premises used: forall_gt_imp_ge_iff_le_of_dense, NoMinOrder.exists_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
⊢ (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → ⊥ ≤ (↑z : WithBot α)) ↔ ⊥ ≤ (↑a : WithBot α)

Tactic:
simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

Premises used: forall_gt_imp_ge_iff_le_of_dense, NoMinOrder.exists_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a a_1 : α
⊢ (∀ (z : α), (↑a : WithBot α) < (↑z : WithBot α) → (↑a_1 : WithBot α) ≤ (↑z : WithBot α)) ↔
    (↑a_1 : WithBot α) ≤ (↑a : WithBot α)

Tactic:
simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

Premises used: forall_gt_imp_ge_iff_le_of_dense, NoMinOrder.exists_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
bot : (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ y) ↔ ⊥ ≤ y
coe : ∀ (a : α), (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ y) ↔ (↑a : WithBot α) ≤ y
⊢ (∀ (z : α), (↑z : WithBot α) < x → (↑z : WithBot α) ≤ y) ↔ x ≤ y

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
bot : (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ ⊥) ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ (↑a : WithBot α)) ↔ ⊥ ≤ (↑a : WithBot α)
⊢ (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ y) ↔ ⊥ ≤ y

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
y : WithBot α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
coe : (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ ⊥) ↔ (↑a : WithBot α) ≤ ⊥
coe₁ :
  ∀ (a_1 : α),
    (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ (↑a_1 : WithBot α)) ↔
      (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ y) ↔ (↑a : WithBot α) ≤ y

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
⊢ (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ ⊥) ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Premises used: forall_lt_imp_le_iff_le_of_dense, NoMinOrder.exists_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
⊢ (∀ (z : α), (↑z : WithBot α) < ⊥ → (↑z : WithBot α) ≤ (↑a : WithBot α)) ↔ ⊥ ≤ (↑a : WithBot α)

Tactic:
simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Premises used: forall_lt_imp_le_iff_le_of_dense, NoMinOrder.exists_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a : α
⊢ (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ ⊥) ↔ (↑a : WithBot α) ≤ ⊥

Tactic:
simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Premises used: forall_lt_imp_le_iff_le_of_dense, NoMinOrder.exists_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a a_1 : α
⊢ (∀ (z : α), (↑z : WithBot α) < (↑a : WithBot α) → (↑z : WithBot α) ≤ (↑a_1 : WithBot α)) ↔
    (↑a : WithBot α) ≤ (↑a_1 : WithBot α)

Tactic:
simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Premises used: forall_lt_imp_le_iff_le_of_dense, NoMinOrder.exists_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a b : WithBot α
⊢ a < b ↔ ∃ (x : α), a < (↑x : WithBot α) ∧ (↑x : WithBot α) < b

Tactic:
⟨fun h =>
    let ⟨_, hy⟩ := exists_between h
    let ⟨x, hx⟩ := lt_iff_exists_coe.1 hy.1
    ⟨x, hx.1 ▸ hy⟩,
    fun ⟨_, hx⟩ => lt_trans hx.1 hx.2⟩

Premises used: _private.0.WithBot.lt_iff_exists_coe_btwn.match_2, WithBot.some, lt_trans, Exists, Eq.rec, WithBot.lt_iff_exists_coe, exists_between, _private.0.WithBot.lt_iff_exists_coe_btwn.match_1, And, And.right, And.left, LT.lt, Iff.intro, Exists.intro, Iff.mp, _private.0.WithBot.lt_iff_exists_coe_btwn.match_3
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a b : WithBot α
rw : (∃ (x : α), a < (↑x : WithBot α) ∧ (↑x : WithBot α) < b) ↔ ∃ (x : α), (↑x : WithBot α) < b ∧ a < (↑x : WithBot α)
⊢ a < b ↔ ∃ (x : α), (↑x : WithBot α) < b ∧ a < (↑x : WithBot α)

Tactic:
rw [lt_iff_exists_coe_btwn]

Premises used: WithBot.lt_iff_exists_coe_btwn
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
a b : WithBot α
⊢ (∃ (x : α), a < (↑x : WithBot α) ∧ (↑x : WithBot α) < b) ↔ ∃ (x : α), (↑x : WithBot α) < b ∧ a < (↑x : WithBot α)

Tactic:
simp_rw [and_comm]

Premises used: and_comm
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a_1 b : α
inst : LE α
inst_1 : NoTopOrder α
inst_2 : Nonempty α
a : α
⊢ ¬(↑a : WithBot α) ≤ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a_1 b : α
inst : LT α
inst_1 : NoMaxOrder α
inst_2 : Nonempty α
a : α
⊢ ⊥ < (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithTop αᵒᵈ ≃ WithBot α) (Equiv.symm WithBot.toDual) WithTop.ofDual

Tactic:
rfl

Premises used: WithTop.ofDual, OrderDual, Equiv.symm, Equiv.refl, rfl, WithTop
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : WithTop αᵒᵈ
⊢ Eq (α := WithBot α) ((Equiv.symm WithBot.toDual : (a : WithTop αᵒᵈ) → WithBot α) a : WithBot α)
    ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) a : WithBot α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithTop α ≃ WithBot αᵒᵈ) (Equiv.symm WithBot.ofDual) WithTop.toDual

Tactic:
rfl

Premises used: WithTop.toDual, OrderDual, Equiv.symm, Equiv.refl, rfl, WithTop
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : WithTop α
⊢ Eq (α := WithBot αᵒᵈ) ((Equiv.symm WithBot.ofDual : (a : WithTop α) → WithBot αᵒᵈ) a : WithBot αᵒᵈ)
    ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) a : WithBot αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ)

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) (⊤ : WithTop α)

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
⊢ Eq (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
    ((↑((toDual : (a : α) → αᵒᵈ) a) : WithTop αᵒᵈ) : WithTop αᵒᵈ)

Tactic:
rfl

Premises used: WithBot.some, WithTop.some, OrderDual, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : αᵒᵈ
⊢ Eq (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
    ((↑((ofDual : (a : αᵒᵈ) → α) a) : WithTop α) : WithTop α)

Tactic:
rfl

Premises used: WithBot.some, WithTop.some, OrderDual, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : αᵒᵈ → βᵒᵈ
a : WithBot α
⊢ map f ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) a) = map ((⇑toDual : (a : βᵒᵈ) → βᵒᵈᵒᵈ) ∘ f) a

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : WithBot αᵒᵈ
⊢ map f ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) a) = map ((⇑ofDual : (a : βᵒᵈ) → β) ∘ f) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : WithBot α
⊢ Eq (α := WithTop βᵒᵈ) ((WithBot.toDual : (a : WithBot β) → WithTop βᵒᵈ) (map f a) : WithTop βᵒᵈ)
    (WithTop.map (α := αᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
        ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) a) :
      WithTop βᵒᵈ)

Tactic:
rfl

Premises used: WithTop.map, OrderDual, WithBot.map, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : αᵒᵈ → βᵒᵈ
a : WithBot αᵒᵈ
⊢ Eq (α := WithTop β) ((WithBot.ofDual : (a : WithBot βᵒᵈ) → WithTop β) (map f a) : WithTop β)
    (WithTop.map (α := α) ((⇑ofDual : (a : βᵒᵈ) → β) ∘ f ∘ (⇑toDual : (a : α) → αᵒᵈ))
        ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) a) :
      WithTop β)

Tactic:
rfl

Premises used: WithTop.map, OrderDual, WithBot.map, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x : WithBot α
y : WithTop αᵒᵈ
bot :
  (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ≤ y ↔
    LE.le (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y : WithBot α) (⊥ : WithBot α)
coe :
  ∀ (a : α),
    (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) ≤ y ↔
      (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y ≤ (↑a : WithBot α)
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) x ≤ y ↔ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y ≤ x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithTop αᵒᵈ
bot :
  LE.le.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ↔
    LE.le.{u_1} (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α) (⊥ : WithBot α)
bot₁ :
  ∀ (a : αᵒᵈ),
    (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ≤ (↑a : WithTop αᵒᵈ) ↔
      LE.le (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
        (⊥ : WithBot α)
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ≤ y ↔
    LE.le (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y : WithBot α) (⊥ : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithTop αᵒᵈ
a : α
coe :
  LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      (⊤ : WithTop αᵒᵈ) ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ ≤ (↑a : WithBot α)
coe₁ :
  ∀ (a_1 : αᵒᵈ),
    (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) ≤ (↑a_1 : WithTop αᵒᵈ) ↔
      (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a_1 : WithTop αᵒᵈ) ≤ (↑a : WithBot α)
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) ≤ y ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y ≤ (↑a : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
⊢ LE.le.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ↔
    LE.le.{u_1} (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α) (⊥ : WithBot α)

Tactic:
simp [toDual_le]

Premises used: OrderDual.toDual_le
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : αᵒᵈ
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ≤ (↑a : WithTop αᵒᵈ) ↔
    LE.le (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
      (⊥ : WithBot α)

Tactic:
simp [toDual_le]

Premises used: OrderDual.toDual_le
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      (⊤ : WithTop αᵒᵈ) ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ ≤ (↑a : WithBot α)

Tactic:
simp [toDual_le]

Premises used: OrderDual.toDual_le
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : α
a_1 : αᵒᵈ
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) ≤ (↑a_1 : WithTop αᵒᵈ) ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a_1 : WithTop αᵒᵈ) ≤ (↑a : WithBot α)

Tactic:
simp [toDual_le]

Premises used: OrderDual.toDual_le
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x : WithTop αᵒᵈ
y : WithBot α
top :
  LE.le (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
coe :
  ∀ (a : αᵒᵈ),
    (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔
      y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)
⊢ x ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔ y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithBot α
top :
  LE.le.{u_1} (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α)
top₁ :
  ∀ (a : α),
    LE.le (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ)
        ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ) ↔
      (↑a : WithBot α) ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
⊢ LE.le (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithBot α
a : αᵒᵈ
coe :
  (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ↔
    LE.le (α := WithBot α) (⊥ : WithBot α)
      ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a_1 : WithBot α) ↔
      (↑a_1 : WithBot α) ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)
⊢ (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y ↔
    y ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
⊢ LE.le.{u_1} (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α)

Tactic:
simp [le_toDual]

Premises used: OrderDual.le_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ LE.le (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ) ↔
    (↑a : WithBot α) ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤

Tactic:
simp [le_toDual]

Premises used: OrderDual.le_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : αᵒᵈ
⊢ (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ↔
    LE.le (α := WithBot α) (⊥ : WithBot α)
      ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)

Tactic:
simp [le_toDual]

Premises used: OrderDual.le_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : αᵒᵈ
a_1 : α
⊢ (↑a : WithTop αᵒᵈ) ≤ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a_1 : WithBot α) ↔
    (↑a_1 : WithBot α) ≤ (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ)

Tactic:
simp [le_toDual]

Premises used: OrderDual.le_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x y : WithBot α
bot :
  LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ ⊥
coe :
  ∀ (a : α),
    LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
        ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
      y ≤ (↑a : WithBot α)
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) x : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithBot α
bot :
  LE.le.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ :
  ∀ (a : α),
    LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
        ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ) ↔
      (↑a : WithBot α) ≤ ⊥
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ ⊥

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithBot α
a : α
coe :
  LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    ⊥ ≤ (↑a : WithBot α)
coe₁ :
  ∀ (a_1 : α),
    LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
        ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a_1 : WithBot α) : WithTop αᵒᵈ) ↔
      (↑a_1 : WithBot α) ≤ (↑a : WithBot α)
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y ≤ (↑a : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
⊢ LE.le.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ) ↔
    (↑a : WithBot α) ≤ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    ⊥ ≤ (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a a_1 : α
⊢ LE.le (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a_1 : WithBot α) : WithTop αᵒᵈ) ↔
    (↑a_1 : WithBot α) ≤ (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x : WithBot αᵒᵈ
y : WithTop α
bot :
  (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ≤ y ↔
    LE.le (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
coe :
  ∀ (a : αᵒᵈ),
    (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) ≤ y ↔
      (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y ≤ (↑a : WithBot αᵒᵈ)
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) x ≤ y ↔ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y ≤ x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithTop α
bot :
  LE.le.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) (⊤ : WithTop α) ↔
    LE.le.{u_1} (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
bot₁ :
  ∀ (a : α),
    (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ≤ (↑a : WithTop α) ↔
      LE.le (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α) : WithBot αᵒᵈ)
        (⊥ : WithBot αᵒᵈ)
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ≤ y ↔
    LE.le (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)

Tactic:
cases y