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 : DistribLattice α
a_1 : α
⊢ ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ ⊥) ≤ (↑a_1 : WithBot α) ⊔ ⊥ ⊓ ⊥

Tactic:
simp [← coe_inf, ← coe_sup]

Premises used: WithBot.coe_inf, WithBot.coe_sup
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 a_2 : α
⊢ ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ≤ (↑a_1 : WithBot α) ⊔ ⊥ ⊓ (↑a_2 : WithBot α)

Tactic:
simp [← coe_inf, ← coe_sup]

Premises used: WithBot.coe_inf, WithBot.coe_sup
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 a_2 : α
⊢ ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ ⊥) ≤ (↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α) ⊓ ⊥

Tactic:
simp [← coe_inf, ← coe_sup]

Premises used: WithBot.coe_inf, WithBot.coe_sup
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 a_2 a_3 : α
coe : (a_1 ⊔ a_2) ⊓ (a_1 ⊔ a_3) ≤ a_1 ⊔ a_2 ⊓ a_3
⊢ ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ (↑a_3 : WithBot α)) ≤
    (↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α) ⊓ (↑a_3 : WithBot α)

Tactic:
simp [← coe_inf, ← coe_sup]

Premises used: WithBot.coe_inf, WithBot.coe_sup
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 a_2 a_3 : α
⊢ (a_1 ⊔ a_2) ⊓ (a_1 ⊔ a_3) ≤ a_1 ⊔ a_2 ⊓ a_3

Tactic:
simpa [← coe_inf, ← coe_sup] using le_sup_inf

Premises used: WithBot.coe_inf, le_sup_inf, WithBot.coe_sup
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
x y z : WithTop α
top : (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z
coe : ∀ (a : α), ((↑a : WithTop α) ⊔ y) ⊓ ((↑a : WithTop α) ⊔ z) ≤ (↑a : WithTop α) ⊔ y ⊓ z
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
y z : WithTop α
top : (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ z
top₁ : ∀ (a : α), (⊤ ⊔ (↑a : WithTop α)) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ (↑a : WithTop α) ⊓ z
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z

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

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
z : WithTop α
top : LE.le.{u_1} (α := WithTop α) ((⊤ ⊔ ⊤) ⊓ (⊤ ⊔ ⊤)) (⊤ ⊔ ⊤ ⊓ ⊤)
top₁ : ∀ (a : α), (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ (↑a : WithTop α)) ≤ ⊤ ⊔ ⊤ ⊓ (↑a : WithTop α)
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ 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 : DistribLattice α
z : WithTop α
a_1 : α
top : (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ (↑a_1 : WithTop α) ⊓ ⊤
top₁ : ∀ (a : α), (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ (↑a : WithTop α)) ≤ ⊤ ⊔ (↑a_1 : WithTop α) ⊓ (↑a : WithTop α)
⊢ (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ (↑a_1 : WithTop α) ⊓ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
z : WithTop α
a_1 : α
coe : ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ ⊤) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ ⊤
coe₁ :
  ∀ (a : α),
    ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ (↑a : WithTop α)) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ (↑a : WithTop α)
⊢ ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ z

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

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
⊢ LE.le.{u_1} (α := WithTop α) ((⊤ ⊔ ⊤) ⊓ (⊤ ⊔ ⊤)) (⊤ ⊔ ⊤ ⊓ ⊤)

Tactic:
simp [← WithTop.coe_inf, ← WithTop.coe_sup]

Premises used: WithTop.coe_sup, WithTop.coe_inf
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 : α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ (↑a_1 : WithTop α)) ≤ ⊤ ⊔ ⊤ ⊓ (↑a_1 : WithTop α)

Tactic:
simp [← WithTop.coe_inf, ← WithTop.coe_sup]

Premises used: WithTop.coe_sup, WithTop.coe_inf
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 : α
⊢ (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ (↑a_1 : WithTop α) ⊓ ⊤

Tactic:
simp [← WithTop.coe_inf, ← WithTop.coe_sup]

Premises used: WithTop.coe_sup, WithTop.coe_inf
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 a_2 : α
⊢ (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ (↑a_2 : WithTop α)) ≤ ⊤ ⊔ (↑a_1 : WithTop α) ⊓ (↑a_2 : WithTop α)

Tactic:
simp [← WithTop.coe_inf, ← WithTop.coe_sup]

Premises used: WithTop.coe_sup, WithTop.coe_inf
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 : α
⊢ ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ ⊤) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ ⊤

Tactic:
simp [← WithTop.coe_inf, ← WithTop.coe_sup]

Premises used: WithTop.coe_sup, WithTop.coe_inf
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 a_2 : α
⊢ ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α)) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ (↑a_2 : WithTop α)

Tactic:
simp [← WithTop.coe_inf, ← WithTop.coe_sup]

Premises used: WithTop.coe_sup, WithTop.coe_inf
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 a_2 : α
⊢ ((↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α)) ⊓ ((↑a_1 : WithTop α) ⊔ ⊤) ≤ (↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α) ⊓ ⊤

Tactic:
simp [← WithTop.coe_inf, ← WithTop.coe_sup]

Premises used: WithTop.coe_sup, WithTop.coe_inf
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 a_2 a_3 : α
coe : (a_1 ⊔ a_2) ⊓ (a_1 ⊔ a_3) ≤ a_1 ⊔ a_2 ⊓ a_3
⊢ ((↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α)) ⊓ ((↑a_1 : WithTop α) ⊔ (↑a_3 : WithTop α)) ≤
    (↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α) ⊓ (↑a_3 : WithTop α)

Tactic:
simp [← WithTop.coe_inf, ← WithTop.coe_sup]

Premises used: WithTop.coe_sup, WithTop.coe_inf
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : DecidableLE α
x : WithBot α
⊢ ⊥ ≤ x

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a_1 b : α
inst : LE α
inst_1 : DecidableLE α
a : α
⊢ ¬(↑a : WithBot α) ≤ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LT α
inst_1 : DecidableLT α
x : WithBot α
⊢ ¬x < ⊥

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 : DecidableLT α
a : α
⊢ ⊥ < (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : WithBot α
bot : ⊥ ≤ y ∨ y ≤ ⊥
coe : ∀ (a : α), (↑a : WithBot α) ≤ y ∨ y ≤ (↑a : WithBot α)
⊢ 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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ∨ LE.le.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), ⊥ ≤ (↑a : WithBot α) ∨ (↑a : WithBot α) ≤ ⊥
⊢ ⊥ ≤ 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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ ∨ ⊥ ≤ (↑a_1 : WithBot α)
coe₁ : ∀ (a : α), (↑a_1 : WithBot α) ≤ (↑a : WithBot α) ∨ (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ (↑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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ∨ LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a_1 : α
⊢ ⊥ ≤ (↑a_1 : WithBot α) ∨ (↑a_1 : WithBot α) ≤ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ ⊥ ∨ ⊥ ≤ (↑a_1 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a_1 a_2 : α
coe : a_1 ≤ a_2 ∨ a_2 ≤ a_1
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) ∨ (↑a_2 : WithBot α) ≤ (↑a_1 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a_1 a_2 : α
⊢ a_1 ≤ a_2 ∨ a_2 ≤ a_1

Tactic:
simpa using Std.Total.total ..

Premises used: Std.Total.total
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : WithTop α
top : ⊤ ≤ y ∨ y ≤ ⊤
coe : ∀ (a : α), (↑a : WithTop α) ≤ y ∨ y ≤ (↑a : WithTop α)
⊢ 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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithTop α
top : LE.le.{u_1} (α := WithTop α) ⊤ ⊤ ∨ LE.le.{u_1} (α := WithTop α) ⊤ ⊤
top₁ : ∀ (a : α), ⊤ ≤ (↑a : WithTop α) ∨ (↑a : WithTop α) ≤ ⊤
⊢ ⊤ ≤ 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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithTop α
a_1 : α
coe : (↑a_1 : WithTop α) ≤ ⊤ ∨ ⊤ ≤ (↑a_1 : WithTop α)
coe₁ : ∀ (a : α), (↑a_1 : WithTop α) ≤ (↑a : WithTop α) ∨ (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
⊢ (↑a_1 : WithTop α) ≤ y ∨ y ≤ (↑a_1 : WithTop α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ LE.le.{u_1} (α := WithTop α) ⊤ ⊤ ∨ LE.le.{u_1} (α := WithTop α) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a_1 : α
⊢ ⊤ ≤ (↑a_1 : WithTop α) ∨ (↑a_1 : WithTop α) ≤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a_1 : α
⊢ (↑a_1 : WithTop α) ≤ ⊤ ∨ ⊤ ≤ (↑a_1 : WithTop α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a_1 a_2 : α
coe : a_1 ≤ a_2 ∨ a_2 ≤ a_1
⊢ (↑a_1 : WithTop α) ≤ (↑a_2 : WithTop α) ∨ (↑a_2 : WithTop α) ≤ (↑a_1 : WithTop α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LT α
inst_1 : WellFoundedLT α
⊢ ∀ (y : WithBot α), y < ⊥ → Acc (fun (x1 x2 : WithBot α) ↦ x1 < x2) y

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 : WellFoundedLT α
a x : α
h : ∀ (y : α), y < x → Acc (fun (x1 x2 : α) ↦ x1 < x2) y
ih : ∀ (y : α), y < x → Acc (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑y : WithBot α)
h_1 : ⊥ < (↑x : WithBot α)
⊢ ∀ (y : WithBot α), y < ⊥ → Acc (fun (x1 x2 : WithBot α) ↦ x1 < x2) y

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 : WellFoundedGT α
a x : α
h : ∀ (y : α), x < y → Acc (fun (x1 x2 : α) ↦ x2 < x1) y
ih : ∀ (y : α), x < y → Acc (fun (x1 x2 : WithBot α) ↦ x1 > x2) (↑y : WithBot α)
⊢ ∀ (y : WithBot α), y > (↑x : WithBot α) → Acc (fun (x1 x2 : WithBot α) ↦ x1 > x2) y

Tactic:
simpa [WithBot.forall]

Premises used: WithBot.forall
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LT α
inst_1 : WellFoundedGT α
acc_some : ∀ (a : α), Acc (fun (x1 x2 : WithBot α) ↦ x1 > x2) (↑a : WithBot α)
⊢ ∀ (y : WithBot α), ⊥ < y → Acc (fun (x1 x2 : WithBot α) ↦ x2 < x1) y

Tactic:
simpa [WithBot.forall]

Premises used: WithBot.forall
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
mp : DenselyOrdered.{u_1} (WithBot α) → DenselyOrdered α
mpr : DenselyOrdered α → DenselyOrdered.{u_1} (WithBot α)
⊢ DenselyOrdered.{u_1} (WithBot α) ↔ DenselyOrdered α

Tactic:
constructor
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
mp : ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂
⊢ DenselyOrdered α

Tactic:
constructor
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered α
mpr : ∀ (a₁ a₂ : WithBot α), a₁ < a₂ → ∃ (a : WithBot α), a₁ < a ∧ a < a₂
⊢ DenselyOrdered.{u_1} (WithBot α)

Tactic:
constructor
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
a b : α
hab : a < b
mp : ∀ (c : WithBot α) (hc : (↑a : WithBot α) < c ∧ c < (↑b : WithBot α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c, hc⟩ := exists_between (WithBot.coe_lt_coe.mpr hab)

Premises used: Iff.mpr, exists_between, WithBot.coe_lt_coe
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
a b : α
hab : a < b
hc : (↑a : WithBot α) < ⊥ ∧ ⊥ < (↑b : WithBot α)
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
simp at hc
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
a b : α
hab : a < b
c : α
hc : (↑a : WithBot α) < (↑c : WithBot α) ∧ (↑c : WithBot α) < (↑b : WithBot α)
⊢ a < c ∧ c < b

Tactic:
simpa using hc
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
a b : α
hab : a < b
c : α
hc : (↑a : WithBot α) < (↑c : WithBot α) ∧ (↑c : WithBot α) < (↑b : WithBot α)
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
exact ⟨c, by simpa using hc⟩
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered.{u_1} (WithBot α)
a b : α
hab : a < b
c : WithBot α
hc : (↑a : WithBot α) < c ∧ c < (↑b : WithBot α)
mp : ∀ (hc : (↑a : WithBot α) < ⊥ ∧ ⊥ < (↑b : WithBot α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
mp₁ :
  ∀ (c : α) (hc : (↑a : WithBot α) < (↑c : WithBot α) ∧ (↑c : WithBot α) < (↑b : WithBot α)),
    ∃ (a_1 : α), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
induction c with
    | bot => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩

Premises used: WithBot.coe, WithBot.bot
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithBot α), a₁ < a₂ → ∃ (a : WithBot α), a₁ < a ∧ a < a₂

Tactic:
simpa [WithBot.exists, WithBot.forall, exists_lt] using DenselyOrdered.dense

Premises used: WithBot.exists, WithBot.forall, NoMinOrder.exists_lt, DenselyOrdered.dense
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
mp : DenselyOrdered.{u_1} (WithTop α) → DenselyOrdered α
mpr : DenselyOrdered α → DenselyOrdered.{u_1} (WithTop α)
⊢ DenselyOrdered.{u_1} (WithTop α) ↔ DenselyOrdered α

Tactic:
constructor
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
mp : ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂
⊢ DenselyOrdered α

Tactic:
constructor
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered α
mpr : ∀ (a₁ a₂ : WithTop α), a₁ < a₂ → ∃ (a : WithTop α), a₁ < a ∧ a < a₂
⊢ DenselyOrdered.{u_1} (WithTop α)

Tactic:
constructor
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
a b : α
hab : a < b
mp : ∀ (c : WithTop α) (hc : (↑a : WithTop α) < c ∧ c < (↑b : WithTop α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c, hc⟩ := exists_between (WithTop.coe_lt_coe.mpr hab)

Premises used: Iff.mpr, exists_between, WithTop.coe_lt_coe
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
a b : α
hab : a < b
hc : (↑a : WithTop α) < ⊤ ∧ ⊤ < (↑b : WithTop α)
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
simp at hc
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
a b : α
hab : a < b
c : α
hc : (↑a : WithTop α) < (↑c : WithTop α) ∧ (↑c : WithTop α) < (↑b : WithTop α)
⊢ a < c ∧ c < b

Tactic:
simpa using hc
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
a b : α
hab : a < b
c : α
hc : (↑a : WithTop α) < (↑c : WithTop α) ∧ (↑c : WithTop α) < (↑b : WithTop α)
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
exact ⟨c, by simpa using hc⟩
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered.{u_1} (WithTop α)
a b : α
hab : a < b
c : WithTop α
hc : (↑a : WithTop α) < c ∧ c < (↑b : WithTop α)
mp : ∀ (hc : (↑a : WithTop α) < ⊤ ∧ ⊤ < (↑b : WithTop α)), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
mp₁ :
  ∀ (c : α) (hc : (↑a : WithTop α) < (↑c : WithTop α) ∧ (↑c : WithTop α) < (↑b : WithTop α)),
    ∃ (a_1 : α), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
induction c with
    | top => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩

Premises used: WithBot.coe
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMaxOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithTop α), a₁ < a₂ → ∃ (a : WithTop α), a₁ < a ∧ a < a₂

Tactic:
simpa [WithTop.exists, WithTop.forall, exists_gt] using DenselyOrdered.dense

Premises used: WithTop.forall, NoMaxOrder.exists_gt, DenselyOrdered.dense, WithTop.exists
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LT α
inst_1 : DenselyOrdered α
inst_2 : NoMinOrder α
⊢ DenselyOrdered.{u_1} (WithBot α)

Tactic:
denselyOrdered_iff.mpr inferInstance

Premises used: Iff.mpr, inferInstance, WithBot.denselyOrdered_iff
-- 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
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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
y : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∨ LT.lt.{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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
⊢ LT.lt.{u_1} (α := WithBot α) ⊥ ⊥ ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∨ LT.lt.{u_1} (α := WithBot α) ⊥ ⊥

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_1 : WithBot α) ∨ ⊥ = (↑a_1 : WithBot α) ∨ (↑a_1 : WithBot α) < ⊥

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_1 : WithBot α) < ⊥ ∨ (↑a_1 : WithBot α) = ⊥ ∨ ⊥ < (↑a_1 : WithBot α)

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 : WithBot α) < (↑a_2 : WithBot α) ∨
    (↑a_1 : WithBot α) = (↑a_2 : WithBot α) ∨ (↑a_2 : WithBot α) < (↑a_1 : WithBot α)

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
x y : WithTop α
top : ⊤ < y ∨ ⊤ = y ∨ y < ⊤
coe : ∀ (a : α), (↑a : WithTop α) < y ∨ (↑a : WithTop α) = y ∨ y < (↑a : WithTop α)
⊢ 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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
y : WithTop α
top : LT.lt.{u_1} (α := WithTop α) ⊤ ⊤ ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ LT.lt.{u_1} (α := WithTop α) ⊤ ⊤
top₁ : ∀ (a : α), ⊤ < (↑a : WithTop α) ∨ ⊤ = (↑a : WithTop α) ∨ (↑a : WithTop α) < ⊤
⊢ ⊤ < 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 α
inst_1 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
y : WithTop α
a_1 : α
coe : (↑a_1 : WithTop α) < ⊤ ∨ (↑a_1 : WithTop α) = ⊤ ∨ ⊤ < (↑a_1 : WithTop α)
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithTop α) < (↑a : WithTop α) ∨
      (↑a_1 : WithTop α) = (↑a : WithTop α) ∨ (↑a : WithTop α) < (↑a_1 : WithTop α)
⊢ (↑a_1 : WithTop α) < y ∨ (↑a_1 : WithTop α) = y ∨ y < (↑a_1 : WithTop α)

Tactic:
cases y
-- 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
⊢ LT.lt.{u_1} (α := WithTop α) ⊤ ⊤ ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ LT.lt.{u_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_1 : WithTop α) ∨ ⊤ = (↑a_1 : WithTop α) ∨ (↑a_1 : WithTop α) < ⊤

Tactic:
simp [trichotomous]

Premises used: trichotomous