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 α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_1 : WithBot α)

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
x y z : WithBot α
bot : ⊥ ≤ y → y ≤ z → ⊥ ≤ z
coe : ∀ (a : α), (↑a : WithBot α) ≤ y → y ≤ z → (↑a : WithBot α) ≤ z
⊢ x ≤ y → y ≤ z → x ≤ z

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
y z : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → ⊥ ≤ z
bot₁ : ∀ (a : α), ⊥ ≤ (↑a : WithBot α) → (↑a : WithBot α) ≤ z → ⊥ ≤ z
⊢ ⊥ ≤ y → y ≤ z → ⊥ ≤ z

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
y z : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ z → (↑a_1 : WithBot α) ≤ z
coe₁ : ∀ (a : α), (↑a_1 : WithBot α) ≤ (↑a : WithBot α) → (↑a : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ z
⊢ (↑a_1 : WithBot α) ≤ y → y ≤ z → (↑a_1 : WithBot α) ≤ z

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
z : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ (↑a : WithBot α) → ⊥ ≤ (↑a : WithBot α)
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → ⊥ ≤ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
z : WithBot α
a_1 : α
bot : ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a : WithBot α) → ⊥ ≤ (↑a : WithBot α)
⊢ ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ z → ⊥ ≤ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
z : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → (↑a_1 : WithBot α) ≤ ⊥
coe₁ : ∀ (a : α), (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a : WithBot α)
⊢ (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ z → (↑a_1 : WithBot α) ≤ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
z : WithBot α
a_1 a_2 : α
coe : (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) → (↑a_2 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ ⊥
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
      (↑a_2 : WithBot α) ≤ (↑a : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a : WithBot α)
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) → (↑a_2 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 : α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ (↑a_1 : WithBot α) → ⊥ ≤ (↑a_1 : WithBot α)

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 : α
⊢ ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 a_2 : α
⊢ ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) → ⊥ ≤ (↑a_2 : WithBot α)

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → (↑a_1 : WithBot α) ≤ ⊥

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a_2 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α)

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) → (↑a_2 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ ⊥

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 a_2 a_3 : α
coe : a_1 ≤ a_2 → a_2 ≤ a_3 → a_1 ≤ a_3
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_2 : WithBot α) ≤ (↑a_3 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a_3 : WithBot α)

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 a_2 a_3 : α
⊢ a_1 ≤ a_2 → a_2 ≤ a_3 → a_1 ≤ a_3

Tactic:
simpa using le_trans

Premises used: le_trans
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
x y : WithBot α
bot : ⊥ < y ↔ ⊥ ≤ y ∧ ¬y ≤ ⊥
coe : ∀ (a : α), (↑a : WithBot α) < y ↔ (↑a : WithBot α) ≤ y ∧ ¬y ≤ (↑a : WithBot α)
⊢ x < y ↔ x ≤ y ∧ ¬y ≤ x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
y : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ∧ ¬LE.le.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), ⊥ < (↑a : WithBot α) ↔ ⊥ ≤ (↑a : WithBot α) ∧ ¬(↑a : WithBot α) ≤ ⊥
⊢ ⊥ < y ↔ ⊥ ≤ y ∧ ¬y ≤ ⊥

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
y : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) < ⊥ ↔ (↑a_1 : WithBot α) ≤ ⊥ ∧ ¬⊥ ≤ (↑a_1 : WithBot α)
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithBot α) < (↑a : WithBot α) ↔
      (↑a_1 : WithBot α) ≤ (↑a : WithBot α) ∧ ¬(↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ (↑a_1 : WithBot α) < y ↔ (↑a_1 : WithBot α) ≤ y ∧ ¬y ≤ (↑a_1 : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
⊢ LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ∧ ¬LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 : α
⊢ ⊥ < (↑a_1 : WithBot α) ↔ ⊥ ≤ (↑a_1 : WithBot α) ∧ ¬(↑a_1 : WithBot α) ≤ ⊥

Tactic:
simp [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 : α
⊢ (↑a_1 : WithBot α) < ⊥ ↔ (↑a_1 : WithBot α) ≤ ⊥ ∧ ¬⊥ ≤ (↑a_1 : WithBot α)

Tactic:
simp [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Preorder α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) < (↑a_2 : WithBot α) ↔
    (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) ∧ ¬(↑a_2 : WithBot α) ≤ (↑a_1 : WithBot α)

Tactic:
simp [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
⊢ StrictMono (β := WithBot α) fun (a : α) ↦ (↑a : WithBot α)

Tactic:
fun _ _ => coe_lt_coe.2

Premises used: Iff.mpr, StrictMono, WithBot.coe_lt_coe
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
⊢ Monotone (β := WithBot α) fun (a : α) ↦ (↑a : WithBot α)

Tactic:
fun _ _ => coe_le_coe.2

Premises used: Iff.mpr, Monotone, WithBot.coe_le_coe
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : WithBot α → β
⊢ Monotone f ↔ (Monotone.{u_1, u_2} (β := β) fun (a : α) ↦ f (↑a : WithBot α)) ∧ ∀ (x : α), f ⊥ ≤ f (↑x : WithBot α)

Tactic:
⟨fun h ↦ ⟨h.comp WithBot.coe_mono, fun _ ↦ h bot_le⟩, fun h ↦
    WithBot.forall.2
      ⟨WithBot.forall.2 ⟨fun _ => le_rfl, fun x _ => h.2 x⟩, fun _ =>
        WithBot.forall.2 ⟨fun h => (not_coe_le_bot _ h).elim,
          fun _ hle => h.1 (coe_le_coe.1 hle)⟩⟩⟩

Premises used: Iff.mpr, WithBot.not_coe_le_bot, le_rfl, False.elim, Monotone.comp, WithBot.coe_le_coe, WithBot.forall, And.right, And.left, And.intro, Iff.intro, Iff.mp, WithBot.coe_mono, bot_le
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ ((Monotone.{u_1, u_2} (β := WithBot β) fun (a : α) ↦ map f (↑a : WithBot α)) ∧
      ∀ (x : α), map f ⊥ ≤ map f (↑x : WithBot α)) ↔
    Monotone f

Tactic:
simp [Monotone]

Premises used: Monotone
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : WithBot α → β
⊢ StrictMono f ↔ (StrictMono.{u_1, u_2} (β := β) fun (a : α) ↦ f (↑a : WithBot α)) ∧ ∀ (x : α), f ⊥ < f (↑x : WithBot α)

Tactic:
⟨fun h => ⟨h.comp WithBot.coe_strictMono, fun _ => h (bot_lt_coe _)⟩, fun h =>
    WithBot.forall.2
      ⟨WithBot.forall.2 ⟨flip absurd (lt_irrefl _), fun x _ => h.2 x⟩, fun _ =>
        WithBot.forall.2 ⟨fun h => (not_lt_bot h).elim, fun _ hle => h.1 (coe_lt_coe.1 hle)⟩⟩⟩

Premises used: Iff.mpr, lt_irrefl, False.elim, not_lt_bot, flip, Bot.bot, WithBot.forall, absurd, And.right, And.left, WithBot.coe_lt_coe, And.intro, Iff.intro, WithBot.bot_lt_coe, Iff.mp, StrictMono.comp, WithBot.coe_strictMono
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : WithBot α → β
⊢ StrictAnti f ↔ (StrictAnti.{u_1, u_2} (β := β) fun (a : α) ↦ f (↑a : WithBot α)) ∧ ∀ (x : α), f (↑x : WithBot α) < f ⊥

Tactic:
strictMono_iff (β := βᵒᵈ)

Premises used: WithBot.strictMono_iff, StrictAnti
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ ((StrictMono.{u_1, u_2} (β := WithBot β) fun (a : α) ↦ map f (↑a : WithBot α)) ∧
      ∀ (x : α), map f ⊥ < map f (↑x : WithBot α)) ↔
    StrictMono f

Tactic:
simp [StrictMono, bot_lt_coe]

Premises used: StrictMono, WithBot.bot_lt_coe
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
bot : map f ⊥ ≤ map f y ↔ ⊥ ≤ y
coe : ∀ (a : α), map f (↑a : WithBot α) ≤ map f y ↔ (↑a : WithBot α) ≤ y
⊢ map f x ≤ map f y ↔ x ≤ y

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
bot : map f ⊥ ≤ map f ⊥ ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), map f ⊥ ≤ map f (↑a : WithBot α) ↔ ⊥ ≤ (↑a : WithBot α)
⊢ map f ⊥ ≤ map f y ↔ ⊥ ≤ y

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a : α
coe : map f (↑a : WithBot α) ≤ map f ⊥ ↔ (↑a : WithBot α) ≤ ⊥
coe₁ : ∀ (a_1 : α), map f (↑a : WithBot α) ≤ map f (↑a_1 : WithBot α) ↔ (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ map f (↑a : WithBot α) ≤ map f y ↔ (↑a : WithBot α) ≤ y

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f ⊥ ≤ map f ⊥ ↔ LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [mono_iff]
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a : α
⊢ map f ⊥ ≤ map f (↑a : WithBot α) ↔ ⊥ ≤ (↑a : WithBot α)

Tactic:
simp [mono_iff]
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a : α
⊢ map f (↑a : WithBot α) ≤ map f ⊥ ↔ (↑a : WithBot α) ≤ ⊥

Tactic:
simp [mono_iff]
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a a_1 : α
⊢ map f (↑a : WithBot α) ≤ map f (↑a_1 : WithBot α) ↔ (↑a : WithBot α) ≤ (↑a_1 : WithBot α)

Tactic:
simp [mono_iff]
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
b : α
bot : ⊥ ≤ (↑(unbotD b ⊥) : WithBot α)
coe : ∀ (a : α), (↑a : WithBot α) ≤ (↑(unbotD b (↑a : WithBot α)) : WithBot α)
⊢ x ≤ (↑(unbotD b x) : WithBot α)

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
b : α
⊢ ⊥ ≤ (↑(unbotD b ⊥) : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
b a : α
⊢ (↑a : WithBot α) ≤ (↑(unbotD b (↑a : WithBot α)) : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
inst_1 : OrderBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ (↑⊥ : WithBot α) ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
coe : ∀ (a : α), (↑a : WithBot α) < (↑⊥ : WithBot α) ↔ (↑a : WithBot α) = ⊥
⊢ x < (↑⊥ : WithBot α) ↔ x = ⊥

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
⊢ LT.lt.{u_1} (α := WithBot α) ⊥ (↑⊥ : WithBot α) ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
a : α
⊢ (↑a : WithBot α) < (↑⊥ : WithBot α) ↔ (↑a : WithBot α) = ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
bot : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ↔ ∀ (b : α), ⊥ < (↑b : WithBot α)
coe : ∀ (a : α), (↑a : WithBot α) = ⊥ ↔ ∀ (b : α), (↑a : WithBot α) < (↑b : WithBot α)
⊢ x = ⊥ ↔ ∀ (b : α), x < (↑b : WithBot α)

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ↔ ∀ (b : α), ⊥ < (↑b : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
a : α
coe : ∃ (x : α), ¬a < x
⊢ (↑a : WithBot α) = ⊥ ↔ ∀ (b : α), (↑a : WithBot α) < (↑b : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ ∃ (x : α), ¬a < x

Tactic:
simpa using ⟨_, lt_irrefl _⟩
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
inst_1 : NoBotOrder α
⊢ x = ⊥ → ∀ (b : α), x ≤ (↑b : WithBot α)

Tactic:
simp +contextual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
inst_1 : NoBotOrder α
refine : ∀ (h : ∀ (b : α), x ≤ (↑b : WithBot α)) (y : α), (↑y : WithBot α) ≠ x
⊢ x = ⊥ ↔ ∀ (b : α), x ≤ (↑b : WithBot α)

Tactic:
refine ⟨by simp +contextual, fun h ↦ (x.eq_bot_iff_forall_ne).2 fun y => ?_⟩
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoBotOrder α
y : α
h : ∀ (b : α), (↑y : WithBot α) ≤ (↑b : WithBot α)
⊢ False

Tactic:
not_isBot y fun z => coe_le_coe.1 (h z)

Premises used: WithBot.coe_le_coe, not_isBot, Iff.mp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoBotOrder α
y : α
h : ∀ (b : α), (↑y : WithBot α) ≤ (↑b : WithBot α)
⊢ False

Tactic:
exact not_isBot y fun z => coe_le_coe.1 (h z)

Premises used: WithBot.coe_le_coe, not_isBot, Iff.mp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x y : WithBot α
inst_1 : NoBotOrder α
none : (∀ (a : α), (↑a : WithBot α) ≤ Option.none → (↑a : WithBot α) ≤ y) ↔ Option.none ≤ y
some : ∀ (a : α), (∀ (a_1 : α), (↑a_1 : WithBot α) ≤ Option.some a → (↑a_1 : WithBot α) ≤ y) ↔ Option.some a ≤ y
⊢ (∀ (a : α), (↑a : WithBot α) ≤ x → (↑a : WithBot α) ≤ y) ↔ x ≤ y

Tactic:
obtain _ | a := x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
y : WithBot α
inst_1 : NoBotOrder α
⊢ (∀ (a : α), (↑a : WithBot α) ≤ none → (↑a : WithBot α) ≤ y) ↔ none ≤ y

Tactic:
simpa [WithBot.none_eq_bot, eq_bot_iff_forall_le] using fun a ha ↦ (not_isBot _ ha).elim

Premises used: False.elim, WithBot.eq_bot_iff_forall_le, not_isBot, WithBot.none_eq_bot
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
y : WithBot α
inst_1 : NoBotOrder α
a : α
⊢ (∀ (a_1 : α), (↑a_1 : WithBot α) ≤ Option.some a → (↑a_1 : WithBot α) ≤ y) ↔ Option.some a ≤ y

Tactic:
⟨fun h ↦ h _ le_rfl, fun hay b ↦ hay.trans'⟩

Premises used: le_rfl, Iff.intro, LE.le.trans'
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
y : WithBot α
inst_1 : NoBotOrder α
a : α
⊢ (∀ (a_1 : α), (↑a_1 : WithBot α) ≤ Option.some a → (↑a_1 : WithBot α) ≤ y) ↔ Option.some a ≤ y

Tactic:
exact ⟨fun h ↦ h _ le_rfl, fun hay b ↦ hay.trans'⟩
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x y : WithBot α
inst_1 : NoBotOrder α
none : (∀ (a : α), Option.none ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ Option.none
some : ∀ (y : α), (∀ (a : α), Option.some y ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ Option.some y
⊢ (∀ (a : α), y ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ y

Tactic:
obtain _ | y := y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
inst_1 : NoBotOrder α
⊢ (∀ (a : α), none ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ none

Tactic:
simp [WithBot.none_eq_bot, eq_bot_iff_forall_le]

Premises used: WithBot.eq_bot_iff_forall_le, WithBot.none_eq_bot
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
inst_1 : NoBotOrder α
y : α
⊢ (∀ (a : α), Option.some y ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ Option.some y

Tactic:
⟨fun h ↦ h _ le_rfl, fun hmn a ham ↦ hmn.trans ham⟩

Premises used: le_rfl, Iff.intro, LE.le.trans
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Preorder α
x : WithBot α
inst_1 : NoBotOrder α
y : α
⊢ (∀ (a : α), Option.some y ≤ (↑a : WithBot α) → x ≤ (↑a : WithBot α)) ↔ x ≤ Option.some y

Tactic:
exact ⟨fun h ↦ h _ le_rfl, fun hmn a ham ↦ hmn.trans ham⟩
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : Preorder α
p : WithBot α → Prop
⊢ (∀ (x : WithBot α), (↑a : WithBot α) < x → p x) ↔ ∀ (b : α), a < b → p (↑b : WithBot α)

Tactic:
simp [WithBot.forall]

Premises used: WithBot.forall
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : Preorder α
p : WithBot α → Prop
⊢ (∃ (x : WithBot α), (↑a : WithBot α) < x ∧ p x) ↔ ∃ (b : α), a < b ∧ p (↑b : WithBot α)

Tactic:
simp [WithBot.exists]

Premises used: WithBot.exists
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : Preorder α
p : WithBot α → Prop
⊢ (∀ (x : WithBot α), (↑a : WithBot α) ≤ x → p x) ↔ ∀ (b : α), a ≤ b → p (↑b : WithBot α)

Tactic:
simp [WithBot.forall]

Premises used: WithBot.forall
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : Preorder α
p : WithBot α → Prop
⊢ (∃ (x : WithBot α), (↑a : WithBot α) ≤ x ∧ p x) ↔ ∃ (b : α), a ≤ b ∧ p (↑b : WithBot α)

Tactic:
simp [WithBot.exists]

Premises used: WithBot.exists
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
x y : WithBot α
bot : ⊥ ≤ y → y ≤ ⊥ → ⊥ = y
coe : ∀ (a : α), (↑a : WithBot α) ≤ y → y ≤ (↑a : WithBot α) → (↑a : WithBot α) = y
⊢ x ≤ y → y ≤ x → x = y

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
y : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), ⊥ ≤ (↑a : WithBot α) → (↑a : WithBot α) ≤ ⊥ → ⊥ = (↑a : WithBot α)
⊢ ⊥ ≤ y → y ≤ ⊥ → ⊥ = y

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
y : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = ⊥
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithBot α) ≤ (↑a : WithBot α) →
      (↑a : WithBot α) ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = (↑a : WithBot α)
⊢ (↑a_1 : WithBot α) ≤ y → y ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = y

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
a_1 : α
⊢ ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ ⊥ → ⊥ = (↑a_1 : WithBot α)

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = ⊥

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
a_1 a_2 : α
coe : a_1 ≤ a_2 → a_2 ≤ a_1 → a_1 = a_2
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_2 : WithBot α) ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) = (↑a_2 : WithBot α)

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : PartialOrder α
a_1 a_2 : α
⊢ a_1 ≤ a_2 → a_2 ≤ a_1 → a_1 = a_2

Tactic:
simpa using le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
y : WithBot α
a b : α
hy : (↑b : WithBot α) ≤ y
rwa : y ≠ ⊥
⊢ b ≤ unbotD a y

Tactic:
rwa [le_unbotD_iff]

Premises used: WithBot.le_unbotD_iff
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
y : WithBot α
a b : α
hy : (↑b : WithBot α) ≤ y
⊢ (↑b : WithBot α) ≠ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
y : WithBot α
a b : α
hy : (↑b : WithBot α) ≤ y
⊢ y ≠ ⊥

Tactic:
exact ne_bot_of_le_ne_bot (by simp) hy

Premises used: ne_bot_of_le_ne_bot
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
y : WithBot α
b : α
inst_1 : Nonempty α
hy : (↑b : WithBot α) ≤ y
⊢ b ≤ y.unbotA

Tactic:
le_unbotD hy

Premises used: WithBot.le_unbotD
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Nonempty α
inst_2 : NoTopOrder α
x : WithBot (WithTop α)
⊢ x = ⊤ → ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ x

Tactic:
simp_all
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Nonempty α
inst_2 : NoTopOrder α
x : WithBot (WithTop α)
refine : ∀ (H : ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ x), x = ⊤
⊢ x = ⊤ ↔ ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ x

Tactic:
refine ⟨by simp_all, fun H ↦ ?_⟩
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Nonempty α
inst_2 : NoTopOrder α
x : WithBot (WithTop α)
H : ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ x
bot : ∀ (H : ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ ⊥), Eq.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤
coe :
  ∀ (a : WithTop α) (H : ∀ (a_1 : α), (↑(↑a_1 : WithTop α) : WithBot (WithTop α)) ≤ (↑a : WithBot (WithTop α))),
    (↑a : WithBot (WithTop α)) = ⊤
⊢ x = ⊤

Tactic:
induction x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Nonempty α
inst_2 : NoTopOrder α
H : ∀ (a : α), (↑(↑a : WithTop α) : WithBot (WithTop α)) ≤ ⊥
⊢ Eq.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤

Tactic:
simp at H
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Nonempty α
inst_2 : NoTopOrder α
a : WithTop α
H : ∀ (a_1 : α), (↑(↑a_1 : WithTop α) : WithBot (WithTop α)) ≤ (↑a : WithBot (WithTop α))
⊢ (↑a : WithBot (WithTop α)) = ⊤

Tactic:
simpa [WithTop.eq_top_iff_forall_ge] using H

Premises used: WithTop.eq_top_iff_forall_ge