mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ⊤ ≤ ⊤ ∨ ⊤ ≤ ⊤

pp: case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ⊤ ≤ ↑a✝ ∨ ↑a✝ ≤ ⊤

pp: case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ ⊤ ∨ ⊤ ≤ ↑a✝

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ∨ ↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ⊤ ≤ ⊤ ∨ ⊤ ≤ ⊤

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ⊤ ≤ ↑a✝ ∨ ↑a✝ ≤ ⊤

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ ⊤ ∨ ⊤ ≤ ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ∨ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
⊢ DenselyOrdered (WithBot α) → DenselyOrdered α

pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
⊢ DenselyOrdered α → DenselyOrdered (WithBot α)

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
⊢ DenselyOrdered (WithBot α) → DenselyOrdered α

case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
⊢ DenselyOrdered α → DenselyOrdered (WithBot α)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
⊢ DenselyOrdered α

pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ DenselyOrdered (WithBot α)

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
⊢ DenselyOrdered α

case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ DenselyOrdered (WithBot α)
Module: Mathlib.Order.Directed

Goal state before:
pp: case inr.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
w : α
hws : w ∈ s
hwr : r y w ∧ r x w
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

Tactic:
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered (WithTop α) → DenselyOrdered α

pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered α → DenselyOrdered (WithTop α)

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered (WithTop α) → DenselyOrdered α

case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered α → DenselyOrdered (WithTop α)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
⊢ DenselyOrdered α

pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ DenselyOrdered (WithTop α)

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
⊢ DenselyOrdered α

case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ DenselyOrdered (WithTop α)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithBot α
⊢ ⊥ < y ∨ ⊥ = y ∨ y < ⊥

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithBot α
a✝ : α
⊢ ↑a✝ < y ∨ ↑a✝ = y ∨ y < ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithBot α
⊢ ⊥ < y ∨ ⊥ = y ∨ y < ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithBot α
a✝ : α
⊢ ↑a✝ < y ∨ ↑a✝ = y ∨ y < ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
⊢ ⊥ < ⊥ ∨ ⊥ = ⊥ ∨ ⊥ < ⊥

pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ⊥ < ↑a✝ ∨ ⊥ = ↑a✝ ∨ ↑a✝ < ⊥

pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ↑a✝ < ⊥ ∨ ↑a✝ = ⊥ ∨ ⊥ < ↑a✝

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ∨ ↑a✝¹ = ↑a✝ ∨ ↑a✝ < ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
⊢ ⊥ < ⊥ ∨ ⊥ = ⊥ ∨ ⊥ < ⊥

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ⊥ < ↑a✝ ∨ ⊥ = ↑a✝ ∨ ↑a✝ < ⊥

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ↑a✝ < ⊥ ∨ ↑a✝ = ⊥ ∨ ⊥ < ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ∨ ↑a✝¹ = ↑a✝ ∨ ↑a✝ < ↑a✝¹
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0

pp: case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0

Tactic:
<;>

Goal state after:
case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0

case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithTop α
⊢ ⊤ < y ∨ ⊤ = y ∨ y < ⊤

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithTop α
a✝ : α
⊢ ↑a✝ < y ∨ ↑a✝ = y ∨ y < ↑a✝

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithTop α
⊢ ⊤ < y ∨ ⊤ = y ∨ y < ⊤

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithTop α
a✝ : α
⊢ ↑a✝ < y ∨ ↑a✝ = y ∨ y < ↑a✝
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a

pp: case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a

Tactic:
<;>

Goal state after:
case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a

case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
⊢ ⊤ < ⊤ ∨ ⊤ = ⊤ ∨ ⊤ < ⊤

pp: case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ⊤ < ↑a✝ ∨ ⊤ = ↑a✝ ∨ ↑a✝ < ⊤

pp: case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ↑a✝ < ⊤ ∨ ↑a✝ = ⊤ ∨ ⊤ < ↑a✝

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ∨ ↑a✝¹ = ↑a✝ ∨ ↑a✝ < ↑a✝¹

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
⊢ ⊤ < ⊤ ∨ ⊤ = ⊤ ∨ ⊤ < ⊤

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ⊤ < ↑a✝ ∨ ⊤ = ↑a✝ ∨ ↑a✝ < ⊤

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ↑a✝ < ⊤ ∨ ↑a✝ = ⊤ ∨ ⊤ < ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ∨ ↑a✝¹ = ↑a✝ ∨ ↑a✝ < ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ⊥ < ↑z → y ≤ ↑z) ↔ y ≤ ⊥

pp: case coe
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑a✝ < ↑z → y ≤ ↑z) ↔ y ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ⊥ < ↑z → y ≤ ↑z) ↔ y ≤ ⊥

case coe
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑a✝ < ↑z → y ≤ ↑z) ↔ y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ⊥ < ↑z → ⊥ ≤ ↑z) ↔ ⊥ ≤ ⊥

pp: case bot.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ⊥ < ↑z → ↑a✝ ≤ ↑z) ↔ ↑a✝ ≤ ⊥

pp: case coe.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑a✝ < ↑z → ⊥ ≤ ↑z) ↔ ⊥ ≤ ↑a✝

pp: case coe.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝¹ a✝ : α
⊢ (∀ (z : α), ↑a✝¹ < ↑z → ↑a✝ ≤ ↑z) ↔ ↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ⊥ < ↑z → ⊥ ≤ ↑z) ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ⊥ < ↑z → ↑a✝ ≤ ↑z) ↔ ↑a✝ ≤ ⊥

case coe.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑a✝ < ↑z → ⊥ ≤ ↑z) ↔ ⊥ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝¹ a✝ : α
⊢ (∀ (z : α), ↑a✝¹ < ↑z → ↑a✝ ≤ ↑z) ↔ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ y) ↔ ⊥ ≤ y

pp: case coe
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝ → ↑z ≤ y) ↔ ↑a✝ ≤ y

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ y) ↔ ⊥ ≤ y

case coe
α : Type u_1
inst✝² : LinearOrder α
y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝ → ↑z ≤ y) ↔ ↑a✝ ≤ y
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ ⊥) ↔ ⊥ ≤ ⊥

pp: case bot.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ ↑a✝) ↔ ⊥ ≤ ↑a✝

pp: case coe.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝ → ↑z ≤ ⊥) ↔ ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝¹ a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝¹ → ↑z ≤ ↑a✝) ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ ⊥) ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ ↑a✝) ↔ ⊥ ≤ ↑a✝

case coe.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝ → ↑z ≤ ⊥) ↔ ↑a✝ ≤ ⊥

case coe.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝¹ a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝¹ → ↑z ≤ ↑a✝) ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LE α
y : WithTop αᵒᵈ
⊢ WithBot.toDual ⊥ ≤ y ↔ WithTop.ofDual y ≤ ⊥

pp: case coe
α : Type u_1
inst✝ : LE α
y : WithTop αᵒᵈ
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ y ↔ WithTop.ofDual y ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithTop αᵒᵈ
⊢ WithBot.toDual ⊥ ≤ y ↔ WithTop.ofDual y ≤ ⊥

case coe
α : Type u_1
inst✝ : LE α
y : WithTop αᵒᵈ
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ y ↔ WithTop.ofDual y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.top
α : Type u_1
inst✝ : LE α
⊢ WithBot.toDual ⊥ ≤ ⊤ ↔ WithTop.ofDual ⊤ ≤ ⊥

pp: case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.toDual ⊥ ≤ ↑a✝ ↔ WithTop.ofDual ↑a✝ ≤ ⊥

pp: case coe.top
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ ⊤ ↔ WithTop.ofDual ⊤ ≤ ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : α
a✝ : αᵒᵈ
⊢ WithBot.toDual ↑a✝¹ ≤ ↑a✝ ↔ WithTop.ofDual ↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.top
α : Type u_1
inst✝ : LE α
⊢ WithBot.toDual ⊥ ≤ ⊤ ↔ WithTop.ofDual ⊤ ≤ ⊥

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.toDual ⊥ ≤ ↑a✝ ↔ WithTop.ofDual ↑a✝ ≤ ⊥

case coe.top
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ ⊤ ↔ WithTop.ofDual ⊤ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : α
a✝ : αᵒᵈ
⊢ WithBot.toDual ↑a✝¹ ≤ ↑a✝ ↔ WithTop.ofDual ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ y.mulLeft ↑(-x) = -y.mulLeft ↑x

Tactic:
apply AddUnits.ext

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑(y.mulLeft ↑(-x)) = ↑(-y.mulLeft ↑x)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ ⊤ ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual ⊤

pp: case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : αᵒᵈ
⊢ ↑a✝ ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual ↑a✝

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ ⊤ ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual ⊤

case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : αᵒᵈ
⊢ ↑a✝ ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.bot
α : Type u_1
inst✝ : LE α
⊢ ⊤ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ WithTop.ofDual ⊤

pp: case top.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ⊤ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ WithTop.ofDual ⊤

pp: case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ ↑a✝ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ WithTop.ofDual ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : αᵒᵈ
a✝ : α
⊢ ↑a✝¹ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ WithTop.ofDual ↑a✝¹

Tactic:
<;>

Goal state after:
case top.bot
α : Type u_1
inst✝ : LE α
⊢ ⊤ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ WithTop.ofDual ⊤

case top.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ⊤ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ WithTop.ofDual ⊤

case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ ↑a✝ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ WithTop.ofDual ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : αᵒᵈ
a✝ : α
⊢ ↑a✝¹ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ WithTop.ofDual ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual y ↔ y ≤ ⊥

pp: case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ WithBot.toDual y ↔ y ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual y ↔ y ≤ ⊥

case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ WithBot.toDual y ↔ y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LE α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ ⊥

pp: case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ ⊥

pp: case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : α
⊢ WithBot.toDual ↑a✝¹ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
inst✝ : LE α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ ⊥

case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : α
⊢ WithBot.toDual ↑a✝¹ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LE α
y : WithTop α
⊢ WithBot.ofDual ⊥ ≤ y ↔ WithTop.toDual y ≤ ⊥

pp: case coe
α : Type u_1
inst✝ : LE α
y : WithTop α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ y ↔ WithTop.toDual y ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithTop α
⊢ WithBot.ofDual ⊥ ≤ y ↔ WithTop.toDual y ≤ ⊥

case coe
α : Type u_1
inst✝ : LE α
y : WithTop α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ y ↔ WithTop.toDual y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.top
α : Type u_1
inst✝ : LE α
⊢ WithBot.ofDual ⊥ ≤ ⊤ ↔ WithTop.toDual ⊤ ≤ ⊥

pp: case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.ofDual ⊥ ≤ ↑a✝ ↔ WithTop.toDual ↑a✝ ≤ ⊥

pp: case coe.top
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ ⊤ ↔ WithTop.toDual ⊤ ≤ ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : αᵒᵈ
a✝ : α
⊢ WithBot.ofDual ↑a✝¹ ≤ ↑a✝ ↔ WithTop.toDual ↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.top
α : Type u_1
inst✝ : LE α
⊢ WithBot.ofDual ⊥ ≤ ⊤ ↔ WithTop.toDual ⊤ ≤ ⊥

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.ofDual ⊥ ≤ ↑a✝ ↔ WithTop.toDual ↑a✝ ≤ ⊥

case coe.top
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ ⊤ ↔ WithTop.toDual ⊤ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : αᵒᵈ
a✝ : α
⊢ WithBot.ofDual ↑a✝¹ ≤ ↑a✝ ↔ WithTop.toDual ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
⊢ ⊤ ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual ⊤

pp: case coe
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
a✝ : α
⊢ ↑a✝ ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual ↑a✝

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
⊢ ⊤ ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual ⊤

case coe
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
a✝ : α
⊢ ↑a✝ ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.bot
α : Type u_1
inst✝ : LE α
⊢ ⊤ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ WithTop.toDual ⊤

pp: case top.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ ⊤ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ WithTop.toDual ⊤

pp: case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ↑a✝ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ WithTop.toDual ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : α
a✝ : αᵒᵈ
⊢ ↑a✝¹ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ WithTop.toDual ↑a✝¹

Tactic:
<;>

Goal state after:
case top.bot
α : Type u_1
inst✝ : LE α
⊢ ⊤ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ WithTop.toDual ⊤

case top.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ ⊤ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ WithTop.toDual ⊤

case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ↑a✝ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ WithTop.toDual ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : α
a✝ : αᵒᵈ
⊢ ↑a✝¹ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ WithTop.toDual ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual y ↔ y ≤ ⊥

pp: case coe
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ WithBot.ofDual y ↔ y ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual y ↔ y ≤ ⊥

case coe
α : Type u_1
inst✝ : LE α
y : WithBot αᵒᵈ
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ WithBot.ofDual y ↔ y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LE α
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ ⊥

pp: case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ ⊥

pp: case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝¹ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
inst✝ : LE α
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ ⊥

case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ ↑a✝

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝¹ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LT α
y : WithTop αᵒᵈ
⊢ WithBot.toDual ⊥ < y ↔ WithTop.ofDual y < ⊥

pp: case coe
α : Type u_1
inst✝ : LT α
y : WithTop αᵒᵈ
a✝ : α
⊢ WithBot.toDual ↑a✝ < y ↔ WithTop.ofDual y < ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : LT α
y : WithTop αᵒᵈ
⊢ WithBot.toDual ⊥ < y ↔ WithTop.ofDual y < ⊥

case coe
α : Type u_1
inst✝ : LT α
y : WithTop αᵒᵈ
a✝ : α
⊢ WithBot.toDual ↑a✝ < y ↔ WithTop.ofDual y < ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.top
α : Type u_1
inst✝ : LT α
⊢ WithBot.toDual ⊥ < ⊤ ↔ WithTop.ofDual ⊤ < ⊥

pp: case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.toDual ⊥ < ↑a✝ ↔ WithTop.ofDual ↑a✝ < ⊥

pp: case coe.top
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ↑a✝ < ⊤ ↔ WithTop.ofDual ⊤ < ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : α
a✝ : αᵒᵈ
⊢ WithBot.toDual ↑a✝¹ < ↑a✝ ↔ WithTop.ofDual ↑a✝ < ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.top
α : Type u_1
inst✝ : LT α
⊢ WithBot.toDual ⊥ < ⊤ ↔ WithTop.ofDual ⊤ < ⊥

case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.toDual ⊥ < ↑a✝ ↔ WithTop.ofDual ↑a✝ < ⊥

case coe.top
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ↑a✝ < ⊤ ↔ WithTop.ofDual ⊤ < ↑a✝

case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : α
a✝ : αᵒᵈ
⊢ WithBot.toDual ↑a✝¹ < ↑a✝ ↔ WithTop.ofDual ↑a✝ < ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top
α : Type u_1
inst✝ : LT α
y : WithBot α
⊢ ⊤ < WithBot.toDual y ↔ y < WithTop.ofDual ⊤

pp: case coe
α : Type u_1
inst✝ : LT α
y : WithBot α
a✝ : αᵒᵈ
⊢ ↑a✝ < WithBot.toDual y ↔ y < WithTop.ofDual ↑a✝

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝ : LT α
y : WithBot α
⊢ ⊤ < WithBot.toDual y ↔ y < WithTop.ofDual ⊤

case coe
α : Type u_1
inst✝ : LT α
y : WithBot α
a✝ : αᵒᵈ
⊢ ↑a✝ < WithBot.toDual y ↔ y < WithTop.ofDual ↑a✝