mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊥ z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z)

pp: case bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z)

pp: case coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊥ z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z)

pp: case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithBot α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝¹) z)

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊥ z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z)

case bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z)

case coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊥ z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z)

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithBot α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝¹) z)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ WithBot.map (⇑e.symm) (WithBot.map ⇑e ⊥) = ⊥

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a✝ : α
⊢ WithBot.map (⇑e.symm) (WithBot.map ⇑e ↑a✝) = ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ WithBot.map (⇑e.symm) (WithBot.map ⇑e ⊥) = ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a✝ : α
⊢ WithBot.map (⇑e.symm) (WithBot.map ⇑e ↑a✝) = ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ WithBot.map (⇑e) (WithBot.map ⇑e.symm ⊥) = ⊥

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a✝ : β
⊢ WithBot.map (⇑e) (WithBot.map ⇑e.symm ↑a✝) = ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ WithBot.map (⇑e) (WithBot.map ⇑e.symm ⊥) = ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a✝ : β
⊢ WithBot.map (⇑e) (WithBot.map ⇑e.symm ↑a✝) = ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
y z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊥ y) ((fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) y z

pp: case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
y z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) (↑a✝) y) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z) → (fun x1 x2 ↦ x1 < x2) y z

Tactic:
<;>

Goal state after:
case bot
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
y z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊥ y) ((fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) y z

case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
y z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) (↑a✝) y) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z) → (fun x1 x2 ↦ x1 < x2) y z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ ⊥ ≤ y ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, y = ↑b ∧ a ≤ b

pp: case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y ↔ ∀ (a : α), ↑a✝ = ↑a → ∃ b, y = ↑b ∧ a ≤ b

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ ⊥ ≤ y ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, y = ↑b ∧ a ≤ b

case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y ↔ ∀ (a : α), ↑a✝ = ↑a → ∃ b, y = ↑b ∧ a ≤ b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LE α
⊢ ⊥ ≤ ⊥ ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, ⊥ = ↑b ∧ a ≤ b

pp: case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ⊥ ≤ ↑a✝ ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, ↑a✝ = ↑b ∧ a ≤ b

pp: case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ↑a✝ ≤ ⊥ ↔ ∀ (a : α), ↑a✝ = ↑a → ∃ b, ⊥ = ↑b ∧ a ≤ b

pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ↔ ∀ (a : α), ↑a✝¹ = ↑a → ∃ b, ↑a✝ = ↑b ∧ a ≤ b

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
inst✝ : LE α
⊢ ⊥ ≤ ⊥ ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, ⊥ = ↑b ∧ a ≤ b

case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ⊥ ≤ ↑a✝ ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, ↑a✝ = ↑b ∧ a ≤ b

case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ↑a✝ ≤ ⊥ ↔ ∀ (a : α), ↑a✝ = ↑a → ∃ b, ⊥ = ↑b ∧ a ≤ b

case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ↔ ∀ (a : α), ↑a✝¹ = ↑a → ∃ b, ↑a✝ = ↑b ∧ a ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊥ ⊥) ((fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) ⊥ z

pp: case bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) (↑a✝) z

pp: case coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z) → (fun x1 x2 ↦ x1 < x2) ⊥ z

pp: case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithBot α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) ((fun x1 x2 ↦ x1 + x2) (↑a✝¹) z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊥ ⊥) ((fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) ⊥ z

case bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) (↑a✝) z

case coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z) → (fun x1 x2 ↦ x1 < x2) ⊥ z

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithBot α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) ((fun x1 x2 ↦ x1 + x2) (↑a✝¹) z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z
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✝¹ : LE α
x y : WithBot α
inst✝ : OrderTop α
⊢ ⊥ ≤ ⊤

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
x y : WithBot α
inst✝ : OrderTop α
a✝ : α
⊢ ↑a✝ ≤ ⊤

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
x y : WithBot α
inst✝ : OrderTop α
⊢ ⊥ ≤ ⊤

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
x y : WithBot α
inst✝ : OrderTop α
a✝ : α
⊢ ↑a✝ ≤ ⊤
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
⊢ ↑a ≤ ⊥ → ⊥ ≤ ↑a

pp: case coe
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
a✝ : α
⊢ ↑a ≤ ↑a✝ → ↑a✝ ≤ ↑a

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
⊢ ↑a ≤ ⊥ → ⊥ ≤ ↑a

case coe
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
a✝ : α
⊢ ↑a ≤ ↑a✝ → ↑a✝ ≤ ↑a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
y z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ y) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) y z

pp: case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
y z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) y) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z) →
    (fun x1 x2 ↦ x1 < x2) y z

Tactic:
<;>

Goal state after:
case bot
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
y z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ y) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) y z

case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
y z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) y) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z) →
    (fun x1 x2 ↦ x1 < x2) y z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) ⊥ z

pp: case bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z

pp: case coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z) →
    (fun x1 x2 ↦ x1 < x2) ⊥ z

pp: case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithBot α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝¹) z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z) → (fun x1 x2 ↦ x1 < x2) ⊥ z

case bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊥ z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z

case coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z) →
    (fun x1 x2 ↦ x1 < x2) ⊥ z

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithBot α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝¹) z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a b : α
inst✝ : LE α
hx : ⊥ = ⊥ → a ≤ b
⊢ unbotD a ⊥ ≤ b ↔ ⊥ ≤ ↑b

pp: case coe
α : Type u_1
a b : α
inst✝ : LE α
a✝ : α
hx : ↑a✝ = ⊥ → a ≤ b
⊢ unbotD a ↑a✝ ≤ b ↔ ↑a✝ ≤ ↑b

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
a b : α
inst✝ : LE α
hx : ⊥ = ⊥ → a ≤ b
⊢ unbotD a ⊥ ≤ b ↔ ⊥ ≤ ↑b

case coe
α : Type u_1
a b : α
inst✝ : LE α
a✝ : α
hx : ↑a✝ = ⊥ → a ≤ b
⊢ unbotD a ↑a✝ ≤ b ↔ ↑a✝ ≤ ↑b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a : α
inst✝ : LE α
x : α
h : ↑x ≤ ⊥
⊢ unbotD a ↑x ≤ unbotD a ⊥

pp: case coe
α : Type u_1
a : α
inst✝ : LE α
x a✝ : α
h : ↑x ≤ ↑a✝
⊢ unbotD a ↑x ≤ unbotD a ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
a : α
inst✝ : LE α
x : α
h : ↑x ≤ ⊥
⊢ unbotD a ↑x ≤ unbotD a ⊥

case coe
α : Type u_1
a : α
inst✝ : LE α
x a✝ : α
h : ↑x ≤ ↑a✝
⊢ unbotD a ↑x ≤ unbotD a ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LT α
y : WithBot α
⊢ ⊥ < y ↔ ∃ b, y = ↑b ∧ ∀ (a : α), ⊥ = ↑a → a < b

pp: case coe
α : Type u_1
inst✝ : LT α
y : WithBot α
a✝ : α
⊢ ↑a✝ < y ↔ ∃ b, y = ↑b ∧ ∀ (a : α), ↑a✝ = ↑a → a < b

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : LT α
y : WithBot α
⊢ ⊥ < y ↔ ∃ b, y = ↑b ∧ ∀ (a : α), ⊥ = ↑a → a < b

case coe
α : Type u_1
inst✝ : LT α
y : WithBot α
a✝ : α
⊢ ↑a✝ < y ↔ ∃ b, y = ↑b ∧ ∀ (a : α), ↑a✝ = ↑a → a < b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LT α
⊢ ⊥ < ⊥ ↔ ∃ b, ⊥ = ↑b ∧ ∀ (a : α), ⊥ = ↑a → a < b

pp: case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ∃ b, ↑a✝ = ↑b ∧ ∀ (a : α), ⊥ = ↑a → a < b

pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ↑a✝ < ⊥ ↔ ∃ b, ⊥ = ↑b ∧ ∀ (a : α), ↑a✝ = ↑a → a < b

pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ↔ ∃ b, ↑a✝ = ↑b ∧ ∀ (a : α), ↑a✝¹ = ↑a → a < b

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
inst✝ : LT α
⊢ ⊥ < ⊥ ↔ ∃ b, ⊥ = ↑b ∧ ∀ (a : α), ⊥ = ↑a → a < b

case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ∃ b, ↑a✝ = ↑b ∧ ∀ (a : α), ⊥ = ↑a → a < b

case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ↑a✝ < ⊥ ↔ ∃ b, ⊥ = ↑b ∧ ∀ (a : α), ↑a✝ = ↑a → a < b

case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ↔ ∃ b, ↑a✝ = ↑b ∧ ∀ (a : α), ↑a✝¹ = ↑a → a < b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LT α
x : WithBot α
⊢ x < ⊥ ↔ ∃ b, ⊥ = ↑b ∧ x < ↑b

pp: case coe
α : Type u_1
inst✝ : LT α
x : WithBot α
a✝ : α
⊢ x < ↑a✝ ↔ ∃ b, ↑a✝ = ↑b ∧ x < ↑b

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : LT α
x : WithBot α
⊢ x < ⊥ ↔ ∃ b, ⊥ = ↑b ∧ x < ↑b

case coe
α : Type u_1
inst✝ : LT α
x : WithBot α
a✝ : α
⊢ x < ↑a✝ ↔ ∃ b, ↑a✝ = ↑b ∧ x < ↑b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot
α : Type u
inst✝² : Add α
z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + ⊥ ≤ ↑x + z → ⊥ ≤ z

pp: case coe
α : Type u
inst✝² : Add α
z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ↑a✝ ≤ ↑x + z → ↑a✝ ≤ z

Tactic:
<;>

Goal state after:
case bot
α : Type u
inst✝² : Add α
z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + ⊥ ≤ ↑x + z → ⊥ ≤ z

case coe
α : Type u
inst✝² : Add α
z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ↑a✝ ≤ ↑x + z → ↑a✝ ≤ z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LT α
⊢ ⊥ < ⊥ ↔ ⊥ ≠ ⊥

pp: case coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ↑a✝ ≠ ⊥

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : LT α
⊢ ⊥ < ⊥ ↔ ⊥ ≠ ⊥

case coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ↑a✝ ≠ ⊥
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + ⊥ ≤ ↑x + ⊥ → ⊥ ≤ ⊥

pp: case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ⊥ ≤ ↑x + ↑a✝ → ⊥ ≤ ↑a✝

pp: case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ↑a✝ ≤ ↑x + ⊥ → ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ ↑x + ↑a✝¹ ≤ ↑x + ↑a✝ → ↑a✝¹ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + ⊥ ≤ ↑x + ⊥ → ⊥ ≤ ⊥

case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ⊥ ≤ ↑x + ↑a✝ → ⊥ ≤ ↑a✝

case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ↑a✝ ≤ ↑x + ⊥ → ↑a✝ ≤ ⊥

case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ ↑x + ↑a✝¹ ≤ ↑x + ↑a✝ → ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a b : α
inst✝ : LT α
hx : ⊥ = ⊥ → a < b
⊢ unbotD a ⊥ < b ↔ ⊥ < ↑b

pp: case coe
α : Type u_1
a b : α
inst✝ : LT α
a✝ : α
hx : ↑a✝ = ⊥ → a < b
⊢ unbotD a ↑a✝ < b ↔ ↑a✝ < ↑b

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
a b : α
inst✝ : LT α
hx : ⊥ = ⊥ → a < b
⊢ unbotD a ⊥ < b ↔ ⊥ < ↑b

case coe
α : Type u_1
a b : α
inst✝ : LT α
a✝ : α
hx : ↑a✝ = ⊥ → a < b
⊢ unbotD a ↑a✝ < b ↔ ↑a✝ < ↑b
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 α
⊢ ⊥ ≤ ⊥

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
⊢ ⊥ ≤ ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ ≤ ↑a✝
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 α
y z : WithBot α
⊢ ⊥ ≤ y → y ≤ z → ⊥ ≤ z

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
y z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y → y ≤ z → ↑a✝ ≤ z

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
y z : WithBot α
⊢ ⊥ ≤ y → y ≤ z → ⊥ ≤ z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
y z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y → y ≤ z → ↑a✝ ≤ z
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 α
z : WithBot α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ z → ⊥ ≤ z

pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
z : WithBot α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ↑a✝ ≤ z → ⊥ ≤ z

pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ⊥ ≤ z → ↑a✝ ≤ z

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
z : WithBot α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝ ≤ z → ↑a✝¹ ≤ z

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
z : WithBot α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ z → ⊥ ≤ z

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
z : WithBot α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ↑a✝ ≤ z → ⊥ ≤ z

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ⊥ ≤ z → ↑a✝ ≤ z

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
z : WithBot α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝ ≤ z → ↑a✝¹ ≤ z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ ⊥ + ↑z ≤ y + ↑z → ⊥ ≤ y

pp: case coe
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝ : α
⊢ ↑a✝ + ↑z ≤ y + ↑z → ↑a✝ ≤ y

Tactic:
<;>

Goal state after:
case bot
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ ⊥ + ↑z ≤ y + ↑z → ⊥ ≤ y

case coe
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝ : α
⊢ ↑a✝ + ↑z ≤ y + ↑z → ↑a✝ ≤ y
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ⊥ → ⊥ ≤ ⊥

pp: case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ↑a✝ → ⊥ ≤ ↑a✝

pp: case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ↑a✝ ≤ ⊥ → ⊥ ≤ ⊥

pp: case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝¹ a✝ : α
⊢ ⊥ ≤ ↑a✝¹ → ↑a✝¹ ≤ ↑a✝ → ⊥ ≤ ↑a✝

pp: case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ⊥ ≤ ⊥ → ↑a✝ ≤ ⊥

pp: case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊥ → ⊥ ≤ ↑a✝ → ↑a✝¹ ≤ ↑a✝

pp: case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝ ≤ ⊥ → ↑a✝¹ ≤ ⊥

pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝¹ ≤ ↑a✝ → ↑a✝² ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ⊥ → ⊥ ≤ ⊥

case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ↑a✝ → ⊥ ≤ ↑a✝

case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ↑a✝ ≤ ⊥ → ⊥ ≤ ⊥

case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝¹ a✝ : α
⊢ ⊥ ≤ ↑a✝¹ → ↑a✝¹ ≤ ↑a✝ → ⊥ ≤ ↑a✝

case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ⊥ ≤ ⊥ → ↑a✝ ≤ ⊥

case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊥ → ⊥ ≤ ↑a✝ → ↑a✝¹ ≤ ↑a✝

case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝ ≤ ⊥ → ↑a✝¹ ≤ ⊥

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝¹ ≤ ↑a✝ → ↑a✝² ≤ ↑a✝
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 α
y : WithBot α
⊢ ⊥ < y ↔ ⊥ ≤ y ∧ ¬y ≤ ⊥

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
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 α
y : WithBot α
⊢ ⊥ < y ↔ ⊥ ≤ y ∧ ¬y ≤ ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
y : WithBot α
a✝ : α
⊢ ↑a✝ < y ↔ ↑a✝ ≤ y ∧ ¬y ≤ ↑a✝