awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithTop α
a : αᵒᵈ
coe :
  LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      (⊤ : WithTop α) ↔
    (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ ≤ (↑a : WithBot αᵒᵈ)
coe₁ :
  ∀ (a_1 : α),
    (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) ≤ (↑a_1 : WithTop α) ↔
      (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a_1 : WithTop α) ≤ (↑a : WithBot αᵒᵈ)
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) ≤ y ↔
    (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) (⊤ : WithTop α) ↔
    LE.le.{u_1} (α := WithBot αᵒᵈ) ((WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ≤ (↑a : WithTop α) ↔
    LE.le (α := WithBot αᵒᵈ) ((WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      (⊤ : WithTop α) ↔
    (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) ≤ (↑a_1 : WithTop α) ↔
    (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤
coe :
  ∀ (a : α),
    (↑a : WithTop α) ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y ↔
      y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α)
⊢ x ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y ↔ y ≤ (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LE.le.{u_1} (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ : WithBot αᵒᵈ)
top₁ :
  ∀ (a : αᵒᵈ),
    LE.le (α := WithTop α) (⊤ : WithTop α)
        ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α) ↔
      (↑a : WithBot αᵒᵈ) ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤
⊢ LE.le (α := WithTop α) (⊤ : WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithBot αᵒᵈ
a : α
coe :
  (↑a : WithTop α) ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ↔
    LE.le (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
      ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α) : WithBot αᵒᵈ)
coe₁ :
  ∀ (a_1 : αᵒᵈ),
    (↑a : WithTop α) ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a_1 : WithBot αᵒᵈ) ↔
      (↑a_1 : WithBot αᵒᵈ) ≤ (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α)
⊢ (↑a : WithTop α) ≤ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y ↔
    y ≤ (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LE.le.{u_1} (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ) ((WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α) ↔
    (↑a : WithBot αᵒᵈ) ≤ (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ↔
    LE.le (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
      ((WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a_1 : WithBot αᵒᵈ) ↔
    (↑a_1 : WithBot αᵒᵈ) ≤ (WithTop.toDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y ≤ ⊥
coe :
  ∀ (a : αᵒᵈ),
    LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
        ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
      y ≤ (↑a : WithBot αᵒᵈ)
⊢ LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) x : WithTop α)
      ((WithBot.ofDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LE.le.{u_1} (α := WithBot αᵒᵈ) ⊥ ⊥
bot₁ :
  ∀ (a : αᵒᵈ),
    LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
        ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α) ↔
      (↑a : WithBot αᵒᵈ) ≤ ⊥
⊢ LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    ⊥ ≤ (↑a : WithBot αᵒᵈ)
coe₁ :
  ∀ (a_1 : αᵒᵈ),
    LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
        ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a_1 : WithBot αᵒᵈ) : WithTop α) ↔
      (↑a_1 : WithBot αᵒᵈ) ≤ (↑a : WithBot αᵒᵈ)
⊢ LE.le (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (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.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LE.le.{u_1} (α := WithBot αᵒᵈ) ⊥ ⊥

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

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

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

Tactic:
simp_all
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x : WithBot α
y : WithTop αᵒᵈ
bot :
  (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ < y ↔
    LT.lt (α := 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 : LT α
y : WithTop αᵒᵈ
bot :
  LT.lt.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ↔
    LT.lt.{u_1} (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α) (⊥ : WithBot α)
bot₁ :
  ∀ (a : αᵒᵈ),
    (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ < (↑a : WithTop αᵒᵈ) ↔
      LT.lt (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
        (⊥ : WithBot α)
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ < y ↔
    LT.lt (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) y : WithBot α) (⊥ : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
y : WithTop αᵒᵈ
a : α
coe :
  LT.lt (α := 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 : LT α
⊢ LT.lt.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ↔
    LT.lt.{u_1} (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α) (⊥ : WithBot α)

Tactic:
simp [toDual_lt]

Premises used: OrderDual.toDual_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : αᵒᵈ
⊢ (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ < (↑a : WithTop αᵒᵈ) ↔
    LT.lt (α := WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)
      (⊥ : WithBot α)

Tactic:
simp [toDual_lt]

Premises used: OrderDual.toDual_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
⊢ LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      (⊤ : WithTop αᵒᵈ) ↔
    (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ < (↑a : WithBot α)

Tactic:
simp [toDual_lt]

Premises used: OrderDual.toDual_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
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_lt]

Premises used: OrderDual.toDual_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x : WithTop αᵒᵈ
y : WithBot α
top :
  LT.lt (α := 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 : LT α
y : WithBot α
top :
  LT.lt.{u_1} (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LT.lt.{u_1} (α := WithBot α) (⊥ : WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α)
top₁ :
  ∀ (a : α),
    LT.lt (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ)
        ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ) ↔
      (↑a : WithBot α) < (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤
⊢ LT.lt (α := 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 : LT α
y : WithBot α
a : αᵒᵈ
coe :
  (↑a : WithTop αᵒᵈ) < (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ↔
    LT.lt (α := 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 : LT α
⊢ LT.lt.{u_1} (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LT.lt.{u_1} (α := WithBot α) (⊥ : WithBot α) ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤ : WithBot α)

Tactic:
simp [lt_toDual]

Premises used: OrderDual.lt_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
⊢ LT.lt (α := WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ) ↔
    (↑a : WithBot α) < (WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) ⊤

Tactic:
simp [lt_toDual]

Premises used: OrderDual.lt_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : αᵒᵈ
⊢ (↑a : WithTop αᵒᵈ) < (WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ ↔
    LT.lt (α := WithBot α) (⊥ : WithBot α)
      ((WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α) (↑a : WithTop αᵒᵈ) : WithBot α)

Tactic:
simp [lt_toDual]

Premises used: OrderDual.lt_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
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 [lt_toDual]

Premises used: OrderDual.lt_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
bot :
  LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
    y < ⊥
coe :
  ∀ (a : α),
    LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
        ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) y : WithTop αᵒᵈ) ↔
      y < (↑a : WithBot α)
⊢ LT.lt (α := 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 : LT α
y : WithBot α
bot :
  LT.lt.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LT.lt.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ :
  ∀ (a : α),
    LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
        ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ) ↔
      (↑a : WithBot α) < ⊥
⊢ LT.lt (α := 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 : LT α
y : WithBot α
a : α
coe :
  LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    ⊥ < (↑a : WithBot α)
coe₁ :
  ∀ (a_1 : α),
    LT.lt (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a : WithBot α) : WithTop αᵒᵈ)
        ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) (↑a_1 : WithBot α) : WithTop αᵒᵈ) ↔
      (↑a_1 : WithBot α) < (↑a : WithBot α)
⊢ LT.lt (α := 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 : LT α
⊢ LT.lt.{u_1} (α := WithTop αᵒᵈ) ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ)
      ((WithBot.toDual : (a : WithBot α) → WithTop αᵒᵈ) ⊥ : WithTop αᵒᵈ) ↔
    LT.lt.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
⊢ LT.lt (α := 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 : LT α
a : α
⊢ LT.lt (α := 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 : LT α
a a_1 : α
⊢ LT.lt (α := 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 : LT α
x : WithBot αᵒᵈ
y : WithTop α
bot :
  (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ < y ↔
    LT.lt (α := 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 : LT α
y : WithTop α
bot :
  LT.lt.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) (⊤ : WithTop α) ↔
    LT.lt.{u_1} (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
bot₁ :
  ∀ (a : α),
    (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ < (↑a : WithTop α) ↔
      LT.lt (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α) : WithBot αᵒᵈ)
        (⊥ : WithBot αᵒᵈ)
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ < y ↔
    LT.lt (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) y : WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)

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

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

Tactic:
simp [toDual_lt]

Premises used: OrderDual.toDual_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
⊢ (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ < (↑a : WithTop α) ↔
    LT.lt (α := WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α) : WithBot αᵒᵈ)
      (⊥ : WithBot αᵒᵈ)

Tactic:
simp [toDual_lt]

Premises used: OrderDual.toDual_lt
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : αᵒᵈ
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      (⊤ : WithTop α) ↔
    (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ < (↑a : WithBot αᵒᵈ)

Tactic:
simp [toDual_lt]

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

Tactic:
simp [toDual_lt]

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

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

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

Tactic:
cases y