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 : α
x : { y : WithBot α // y ≠ ⊥ }
⊢ (fun (x : α) ↦ (Subtype.mk (p := fun (y : WithBot α) ↦ y ≠ ⊥) (↑x : WithBot α) ⋯ : { y : WithBot α // y ≠ ⊥ }))
      ((fun (x : { y : WithBot α // y ≠ ⊥ }) ↦
          (match (motive := { y : WithBot α // y ≠ ⊥ } → α) x with
            | ⟨x, h⟩ => x.unbot h :
            α))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b x : α
⊢ (fun (x : { y : WithBot α // y ≠ ⊥ }) ↦
        (match (motive := { y : WithBot α // y ≠ ⊥ } → α) x with
          | ⟨x, h⟩ => x.unbot h :
          α))
      ((fun (x : α) ↦ (Subtype.mk (p := fun (y : WithBot α) ↦ y ≠ ⊥) (↑x : WithBot α) ⋯ : { y : WithBot α // y ≠ ⊥ }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Nonempty α
ha : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ unbotA ⊥ = unbot ⊥ ha

Tactic:
contradiction
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Nonempty α
a : α
ha : (↑a : WithBot α) ≠ ⊥
⊢ (↑a : WithBot α).unbotA = (↑a : WithBot α).unbot ha

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Nonempty α
a : WithBot α
ha : a ≠ ⊥
bot : ∀ (ha : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥), unbotA ⊥ = unbot ⊥ ha
coe : ∀ (a : α) (ha : (↑a : WithBot α) ≠ ⊥), (↑a : WithBot α).unbotA = (↑a : WithBot α).unbot ha
⊢ a.unbotA = a.unbot ha

Tactic:
cases a with
  | bot => contradiction
  | coe a => simp

Premises used: WithBot.coe, WithBot.bot
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
x : WithBot α
bot :
  Eq.{u_1 + 1} (α := WithBot α)
    (WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) ⊥)) ⊥
coe :
  ∀ (a : α),
    WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map (⇑e : (a : α) → β) (↑a : WithBot α)) =
      (↑a : WithBot α)
⊢ WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map (⇑e : (a : α) → β) x) = x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ Eq.{u_1 + 1} (α := WithBot α)
    (WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) ⊥)) ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a : α
⊢ WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map (⇑e : (a : α) → β) (↑a : WithBot α)) =
    (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
x : WithBot β
bot :
  Eq.{u_2 + 1} (α := WithBot β)
    (WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) ⊥)) ⊥
coe :
  ∀ (a : β),
    WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map (⇑e.symm : (a : β) → α) (↑a : WithBot β)) =
      (↑a : WithBot β)
⊢ WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map (⇑e.symm : (a : β) → α) x) = x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ Eq.{u_2 + 1} (α := WithBot β)
    (WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) ⊥)) ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a : β
⊢ WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map (⇑e.symm : (a : β) → α) (↑a : WithBot β)) =
    (↑a : WithBot β)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
⊢ (Equiv.refl α).withBotCongr = Equiv.refl (WithBot α)

Tactic:
Equiv.ext <| congr_fun WithBot.map_id

Premises used: Equiv.ext, congr_fun, WithBot.map_id
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ e.symm.withBotCongr = e.withBotCongr.symm

Tactic:
rfl

Premises used: WithBot, Equiv.withBotCongr, Equiv.symm, WithBot.map, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
H :
  ∀ (x : WithBot α),
    Eq.{u_3 + 1} (α := WithBot γ) (((e₁.trans e₂).withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
      ((e₁.withBotCongr.trans e₂.withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
ext x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
x : WithBot α
⊢ Eq.{u_3 + 1} (α := WithBot γ) (((e₁.trans e₂).withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
    ((e₁.withBotCongr.trans e₂.withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x y : WithBot α
⊢ x ≤ y ↔ x = ⊥ ∨ ∃ (a : α), ∃ (b : α), a ≤ b ∧ x = (↑a : WithBot α) ∧ y = (↑b : WithBot α)

Tactic:
le_def_aux ..

Premises used: WithBot.le_def_aux
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x y : WithTop α
⊢ x ≤ y ↔ y = ⊤ ∨ ∃ (b : α), ∃ (a : α), a ≤ b ∧ y = (↑b : WithTop α) ∧ x = (↑a : WithTop α)

Tactic:
WithBot.le_def

Premises used: WithTop.some, OrderDual, WithBot.le_def, WithTop
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x y : WithTop α
⊢ x ≤ y ↔ y = ⊤ ∨ ∃ (a : α), ∃ (b : α), a ≤ b ∧ x = (↑a : WithTop α) ∧ y = (↑b : WithTop α)

Tactic:
grind [WithTop.le_def']

Premises used: WithTop.le_def'
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
⊢ ((∃ (b : α), x = ⊥ ∧ y = (↑b : WithBot α)) ∨
      ∃ (a : α), ∃ (b : α), a < b ∧ x = (↑a : WithBot α) ∧ y = (↑b : WithBot α)) ↔
    (x = ⊥ ∧ ∃ (b : α), y = (↑b : WithBot α)) ∨
      ∃ (a : α), ∃ (b : α), a < b ∧ x = (↑a : WithBot α) ∧ y = (↑b : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x y : WithTop α
⊢ x < y ↔
    (y = ⊤ ∧ ∃ (a : α), x = (↑a : WithTop α)) ∨
      ∃ (b : α), ∃ (a : α), a < b ∧ y = (↑b : WithTop α) ∧ x = (↑a : WithTop α)

Tactic:
WithBot.lt_def

Premises used: WithBot.lt_def, WithTop.some, OrderDual, WithTop
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x y : WithTop α
⊢ x < y ↔
    (∃ (a : α), x = (↑a : WithTop α)) ∧ y = ⊤ ∨
      ∃ (a : α), ∃ (b : α), a < b ∧ x = (↑a : WithTop α) ∧ y = (↑b : WithTop α)

Tactic:
grind [WithTop.lt_def']

Premises used: WithTop.lt_def'
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x y : WithBot α
bot : ⊥ ≤ y ↔ ∀ (a : α), ⊥ = (↑a : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a ≤ b
coe :
  ∀ (a : α),
    (↑a : WithBot α) ≤ y ↔
      ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a_1 ≤ b
⊢ x ≤ y ↔ ∀ (a : α), x = (↑a : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a ≤ b

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

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
y : WithBot α
a : α
coe :
  (↑a : WithBot α) ≤ ⊥ ↔ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ a_1 ≤ b
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithBot α) ≤ (↑a_1 : WithBot α) ↔
      ∀ (a_2 : α), (↑a : WithBot α) = (↑a_2 : WithBot α) → ∃ (b : α), (↑a_1 : WithBot α) = (↑b : WithBot α) ∧ a_2 ≤ b
⊢ (↑a : WithBot α) ≤ y ↔ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a_1 ≤ b

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ↔ ∀ (a : α), ⊥ = (↑a : WithBot α) → ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ a ≤ b

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ ⊥ ≤ (↑a : WithBot α) ↔ ∀ (a_1 : α), ⊥ = (↑a_1 : WithBot α) → ∃ (b : α), (↑a : WithBot α) = (↑b : WithBot α) ∧ a_1 ≤ b

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ (↑a : WithBot α) ≤ ⊥ ↔ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ a_1 ≤ b

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a a_1 : α
⊢ (↑a : WithBot α) ≤ (↑a_1 : WithBot α) ↔
    ∀ (a_2 : α), (↑a : WithBot α) = (↑a_2 : WithBot α) → ∃ (b : α), (↑a_1 : WithBot α) = (↑b : WithBot α) ∧ a_2 ≤ b

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LE α
⊢ (↑a : WithBot α) ≤ (↑b : WithBot α) ↔ a ≤ b

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ ¬(↑a : 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 : LE α
x y : WithBot α
⊢ ∀ (a : WithBot α), ⊥ ≤ a

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 : LE α
x_1 y : WithBot α
inst_1 : OrderTop α
x : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊤
coe : ∀ (a : α), (↑a : WithBot α) ≤ ⊤
⊢ x ≤ ⊤

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
x y : WithBot α
inst_1 : OrderTop α
⊢ 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 : LE α
x y : WithBot α
inst_1 : OrderTop α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ ⊤

Tactic:
simp [le_def]

Premises used: WithBot.le_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ (↑a : WithBot α) ≤ ⊥ ↔ (↑a : WithBot α) = ⊥

Tactic:
simp [not_coe_le_bot]

Premises used: WithBot.not_coe_le_bot
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
⊢ (↑a : WithBot α) ≤ x ↔ ∃ (b : α), x = (↑b : WithBot α) ∧ a ≤ b

Tactic:
simp [le_iff_forall]

Premises used: WithBot.le_iff_forall
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
b : α
inst : LE α
x : WithBot α
⊢ x ≤ (↑b : WithBot α) ↔ ∀ (a : α), x = (↑a : WithBot α) → a ≤ b

Tactic:
simp [le_iff_forall]

Premises used: WithBot.le_iff_forall
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
h : IsMax a
x : WithBot α
bot : (↑a : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a : WithBot α)
coe : ∀ (a_1 : α), (↑a : WithBot α) ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a : WithBot α)
⊢ (↑a : WithBot α) ≤ x → x ≤ (↑a : WithBot α)

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
h : IsMax a
⊢ (↑a : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
h : IsMax a
a_1 : α
coe : a ≤ a_1 → a_1 ≤ a
⊢ (↑a : WithBot α) ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
h : IsMax a
a_1 : α
⊢ a ≤ a_1 → a_1 ≤ a

Tactic:
simpa using @h _
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ x ≠ ⊥

Tactic:
hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
hx : x ≠ ⊥
lift : ∀ (x : α) (hx : (↑x : WithBot α) ≠ ⊥), a ≤ (↑x : WithBot α).unbot hx ↔ (↑a : WithBot α) ≤ (↑x : WithBot α)
⊢ a ≤ x.unbot hx ↔ (↑a : WithBot α) ≤ x

Tactic:
lift x to α using hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : α
hx : (↑x : WithBot α) ≠ ⊥
⊢ a ≤ (↑x : WithBot α).unbot hx ↔ (↑a : WithBot α) ≤ (↑x : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
hx : x ≠ ⊥
lift : ∀ (x : α) (hx : (↑x : WithBot α) ≠ ⊥), (↑x : WithBot α).unbot hx ≤ a ↔ (↑x : WithBot α) ≤ (↑a : WithBot α)
⊢ x.unbot hx ≤ a ↔ x ≤ (↑a : WithBot α)

Tactic:
lift x to α using hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : α
hx : (↑x : WithBot α) ≠ ⊥
⊢ (↑x : WithBot α).unbot hx ≤ a ↔ (↑x : WithBot α) ≤ (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x y : WithBot α
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x.unbot hx ≤ y.unbot hy ↔ x ≤ y

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ x ≠ ⊥

Tactic:
hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LE α
x : WithBot α
hx : x ≠ ⊥
lift : ∀ (x : α), b ≤ unbotD a (↑x : WithBot α) ↔ (↑b : WithBot α) ≤ (↑x : WithBot α)
⊢ b ≤ unbotD a x ↔ (↑b : WithBot α) ≤ x

Tactic:
lift x to α using hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LE α
x : α
⊢ b ≤ unbotD a (↑x : WithBot α) ↔ (↑b : WithBot α) ≤ (↑x : WithBot α)

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

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LE α
hx : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ → a ≤ b
⊢ unbotD a ⊥ ≤ b ↔ ⊥ ≤ (↑b : WithBot α)

Tactic:
simp [hx]
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LE α
a_1 : α
hx : (↑a_1 : WithBot α) = ⊥ → a ≤ b
⊢ unbotD a (↑a_1 : WithBot α) ≤ b ↔ (↑a_1 : WithBot α) ≤ (↑b : WithBot α)

Tactic:
simp [hx]
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x y : WithBot α
hx : x ≠ ⊥
h : x ≤ y
⊢ x ≠ ⊥

Tactic:
hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x y : WithBot α
hx : x ≠ ⊥
h : x ≤ y
lift : ∀ (x : α) (h : (↑x : WithBot α) ≤ y), unbotD a (↑x : WithBot α) ≤ unbotD a y
⊢ unbotD a x ≤ unbotD a y

Tactic:
lift x to α using hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
y : WithBot α
x : α
h : (↑x : WithBot α) ≤ y
bot : ∀ (h : (↑x : WithBot α) ≤ ⊥), unbotD a (↑x : WithBot α) ≤ unbotD a ⊥
coe : ∀ (a_1 : α) (h : (↑x : WithBot α) ≤ (↑a_1 : WithBot α)), unbotD a (↑x : WithBot α) ≤ unbotD a (↑a_1 : WithBot α)
⊢ unbotD a (↑x : WithBot α) ≤ unbotD a y

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : α
h : (↑x : WithBot α) ≤ ⊥
⊢ unbotD a (↑x : WithBot α) ≤ unbotD a ⊥

Tactic:
simp_all
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x a_1 : α
h : (↑x : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ unbotD a (↑x : WithBot α) ≤ unbotD a (↑a_1 : WithBot α)

Tactic:
simp_all
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
inst_1 : Nonempty α
hx : x ≠ ⊥
⊢ a ≤ x.unbotA ↔ (↑a : WithBot α) ≤ x

Tactic:
le_unbotD_iff hx

Premises used: WithBot.le_unbotD_iff
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
inst_1 : Nonempty α
hx : x ≠ ⊥
⊢ x ≠ ⊥

Tactic:
hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
inst_1 : Nonempty α
hx : x ≠ ⊥
lift : ∀ (x : α), (↑x : WithBot α).unbotA ≤ a ↔ (↑x : WithBot α) ≤ (↑a : WithBot α)
⊢ x.unbotA ≤ a ↔ x ≤ (↑a : WithBot α)

Tactic:
lift x to α using hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LE α
inst_1 : Nonempty α
x : α
⊢ (↑x : WithBot α).unbotA ≤ a ↔ (↑x : WithBot α) ≤ (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LE α
x y : WithBot α
inst_1 : Nonempty α
hy : x ≠ ⊥
h : x ≤ y
⊢ x.unbotA ≤ y.unbotA

Tactic:
unbotD_mono hy h

Premises used: WithBot.unbotD_mono
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
bot : ⊥ < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
coe :
  ∀ (a : α),
    (↑a : WithBot α) < y ↔
      ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → a_1 < b
⊢ x < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a : α), x = (↑a : WithBot α) → a < b

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
y : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
bot₁ :
  ∀ (a : α),
    ⊥ < (↑a : WithBot α) ↔ ∃ (b : α), (↑a : WithBot α) = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b
⊢ ⊥ < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
y : WithBot α
a : α
coe :
  (↑a : WithBot α) < ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → a_1 < b
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithBot α) < (↑a_1 : WithBot α) ↔
      ∃ (b : α), (↑a_1 : WithBot α) = (↑b : WithBot α) ∧ ∀ (a_2 : α), (↑a : WithBot α) = (↑a_2 : WithBot α) → a_2 < b
⊢ (↑a : WithBot α) < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → a_1 < b

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
⊢ LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b

Tactic:
simp [lt_def]

Premises used: WithBot.lt_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
⊢ ⊥ < (↑a : WithBot α) ↔ ∃ (b : α), (↑a : WithBot α) = (↑b : WithBot α) ∧ ∀ (a : α), ⊥ = (↑a : WithBot α) → a < b

Tactic:
simp [lt_def]

Premises used: WithBot.lt_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
⊢ (↑a : WithBot α) < ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → a_1 < b

Tactic:
simp [lt_def]

Premises used: WithBot.lt_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a a_1 : α
⊢ (↑a : WithBot α) < (↑a_1 : WithBot α) ↔
    ∃ (b : α), (↑a_1 : WithBot α) = (↑b : WithBot α) ∧ ∀ (a_2 : α), (↑a : WithBot α) = (↑a_2 : WithBot α) → a_2 < b

Tactic:
simp [lt_def]

Premises used: WithBot.lt_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LT α
⊢ (↑a : WithBot α) < (↑b : WithBot α) ↔ a < b

Tactic:
simp [lt_def]

Premises used: WithBot.lt_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
⊢ ⊥ < (↑a : WithBot α)

Tactic:
simp [lt_def]

Premises used: WithBot.lt_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : WithBot α
⊢ ¬a < ⊥

Tactic:
simp [lt_def]

Premises used: WithBot.lt_def
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
bot : x < ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ x < (↑b : WithBot α)
coe : ∀ (a : α), x < (↑a : WithBot α) ↔ ∃ (b : α), (↑a : WithBot α) = (↑b : WithBot α) ∧ x < (↑b : WithBot α)
⊢ x < y ↔ ∃ (b : α), y = (↑b : WithBot α) ∧ x < (↑b : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x : WithBot α
⊢ x < ⊥ ↔ ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ x < (↑b : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x : WithBot α
a : α
⊢ x < (↑a : WithBot α) ↔ ∃ (b : α), (↑a : WithBot α) = (↑b : WithBot α) ∧ x < (↑b : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
b : α
inst : LT α
x : WithBot α
⊢ x < (↑b : WithBot α) ↔ ∀ (a : α), x = (↑a : WithBot α) → a < b

Tactic:
simp [lt_iff_exists]

Premises used: WithBot.lt_iff_exists
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ↔ Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥
coe : ∀ (a : α), ⊥ < (↑a : WithBot α) ↔ (↑a : WithBot α) ≠ ⊥
⊢ ⊥ < x ↔ x ≠ ⊥

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

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
⊢ ⊥ < (↑a : WithBot α) ↔ (↑a : WithBot α) ≠ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ x ≠ ⊥

Tactic:
hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LT α
x : WithBot α
hx : x ≠ ⊥
lift : ∀ (x : α) (hx : (↑x : WithBot α) ≠ ⊥), a < (↑x : WithBot α).unbot hx ↔ (↑a : WithBot α) < (↑x : WithBot α)
⊢ a < x.unbot hx ↔ (↑a : WithBot α) < x

Tactic:
lift x to α using hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LT α
x : α
hx : (↑x : WithBot α) ≠ ⊥
⊢ a < (↑x : WithBot α).unbot hx ↔ (↑a : WithBot α) < (↑x : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
b : α
inst : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ x ≠ ⊥

Tactic:
hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
b : α
inst : LT α
x : WithBot α
hx : x ≠ ⊥
lift : ∀ (x : α) (hx : (↑x : WithBot α) ≠ ⊥), (↑x : WithBot α).unbot hx < b ↔ (↑x : WithBot α) < (↑b : WithBot α)
⊢ x.unbot hx < b ↔ x < (↑b : WithBot α)

Tactic:
lift x to α using hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
b : α
inst : LT α
x : α
hx : (↑x : WithBot α) ≠ ⊥
⊢ (↑x : WithBot α).unbot hx < b ↔ (↑x : WithBot α) < (↑b : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x y : WithBot α
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x.unbot hx < y.unbot hy ↔ x < y

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ x ≠ ⊥

Tactic:
hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LT α
x : WithBot α
hx : x ≠ ⊥
lift : ∀ (x : α), b < unbotD a (↑x : WithBot α) ↔ (↑b : WithBot α) < (↑x : WithBot α)
⊢ b < unbotD a x ↔ (↑b : WithBot α) < x

Tactic:
lift x to α using hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LT α
x : α
⊢ b < unbotD a (↑x : WithBot α) ↔ (↑b : WithBot α) < (↑x : WithBot α)

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

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LT α
hx : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ → a < b
⊢ unbotD a ⊥ < b ↔ ⊥ < (↑b : WithBot α)

Tactic:
simp [hx]
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
inst : LT α
a_1 : α
hx : (↑a_1 : WithBot α) = ⊥ → a < b
⊢ unbotD a (↑a_1 : WithBot α) < b ↔ (↑a_1 : WithBot α) < (↑b : WithBot α)

Tactic:
simp [hx]
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LT α
x : WithBot α
inst_1 : Nonempty α
hx : x ≠ ⊥
⊢ a < x.unbotA ↔ (↑a : WithBot α) < x

Tactic:
lt_unbotD_iff hx

Premises used: WithBot.lt_unbotD_iff
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LT α
x : WithBot α
inst_1 : Nonempty α
hx : x ≠ ⊥
⊢ x ≠ ⊥

Tactic:
hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LT α
x : WithBot α
inst_1 : Nonempty α
hx : x ≠ ⊥
lift : ∀ (x : α), (↑x : WithBot α).unbotA < a ↔ (↑x : WithBot α) < (↑a : WithBot α)
⊢ x.unbotA < a ↔ x < (↑a : WithBot α)

Tactic:
lift x to α using hx
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
inst : LT α
inst_1 : Nonempty α
x : α
⊢ (↑x : WithBot α).unbotA < a ↔ (↑x : WithBot α) < (↑a : WithBot α)

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

Tactic:
cases x