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

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

Tactic:
cases x

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: α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
x : WithBot α
⊢ ↑a ≤ x → x ≤ ↑a

Tactic:
cases x

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝² + a✝¹ < a✝² + a✝ → a✝¹ < a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases x

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.Order.WithBot

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

Tactic:
cases x

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: α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ x < y ↔ ∃ b, y = ↑b ∧ ∀ (a : α), x = ↑a → a < b

Tactic:
cases x

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: α : Type u_1
inst✝ : LT α
x : WithBot α
⊢ ⊥ < x ↔ x ≠ ⊥

Tactic:
cases x

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 + ⊥ → ⊥ ≤ ⊥

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
cases x

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.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
x : WithBot α
⊢ x ≤ x

Tactic:
cases x

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

Tactic:
cases x

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.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases x

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

Tactic:
cases x

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✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ ⊥ < ⊥ → ↑x + ⊥ < ↑x + ⊥

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ⊥ < ↑a✝ → ↑x + ⊥ < ↑x + ↑a✝

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ↑a✝ < ⊥ → ↑x + ↑a✝ < ↑x + ⊥

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z

Tactic:
cases x

Goal state after:
case bot
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ ⊥ < y → ⊥ + ↑z < y + ↑z

case coe
α : Type u
inst✝² : Add α
y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ↑a✝ < y → ↑a✝ + ↑z < y + ↑z
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f x ≤ map f y ↔ x ≤ y

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f ⊥ ≤ map f y ↔ ⊥ ≤ y

case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝ : α
⊢ map f ↑a✝ ≤ map f y ↔ ↑a✝ ≤ y
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ ⊥ < ⊥ → ⊥ + ↑z < ⊥ + ↑z

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ⊥ < ↑a✝ → ⊥ + ↑z < ↑a✝ + ↑z

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ↑a✝ < ⊥ → ↑a✝ + ↑z < ⊥ + ↑z

Tactic:
simp [← coe_add]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithBot α
b : α
⊢ x ≤ ↑(unbotD b x)

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : Preorder α
b : α
⊢ ⊥ ≤ ↑(unbotD b ⊥)

case coe
α : Type u_1
inst✝ : Preorder α
b a✝ : α
⊢ ↑a✝ ≤ ↑(unbotD b ↑a✝)
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : OrderBot α
⊢ x < ↑⊥ ↔ x = ⊥

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ ⊥ < ↑⊥ ↔ ⊥ = ⊥

case coe
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
a✝ : α
⊢ ↑a✝ < ↑⊥ ↔ ↑a✝ = ⊥
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithBot α
⊢ x = ⊥ ↔ ∀ (b : α), x < ↑b

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : Preorder α
⊢ ⊥ = ⊥ ↔ ∀ (b : α), ⊥ < ↑b

case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ = ⊥ ↔ ∀ (b : α), ↑a✝ < ↑b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
x y : WithBot α
⊢ x ≤ y → y ≤ x → x = y

Tactic:
cases x

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

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y → y ≤ ↑a✝ → ↑a✝ = y
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithBot α
⊢ x ≤
    match x, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithBot α
⊢ ⊥ ≤
    match ⊥, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤
    match ↑a✝, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithBot α
⊢ y ≤
    match x, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithBot α
⊢ y ≤
    match ⊥, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithBot α
a✝ : α
⊢ y ≤
    match ↑a✝, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ∃ c, ↑a✝ = ↑a✝¹ + c

Tactic:
intro h

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝¹ a✝ : α
h : ↑a✝¹ ≤ ↑a✝
⊢ ∃ c, ↑a✝ = ↑a✝¹ + c
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y z : WithBot α
⊢ x ≤ z →
    y ≤ z →
      (match x, y with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        z

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y z : WithBot α
⊢ ⊥ ≤ z →
    y ≤ z →
      (match ⊥, y with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ z →
    y ≤ z →
      (match ↑a✝, y with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        z
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithTop α
⊢ (match x, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    x

Tactic:
cases x

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y : WithTop α
⊢ (match ⊤, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    ⊤

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y : WithTop α
a✝ : α
⊢ (match ↑a✝, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithTop α
⊢ (match x, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    y

Tactic:
cases x

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y : WithTop α
⊢ (match ⊤, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    y

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y : WithTop α
a✝ : α
⊢ (match ↑a✝, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    y
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y z : WithTop α
⊢ x ≤ y →
    x ≤ z →
      x ≤
        match y, z with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

Tactic:
cases x

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y z : WithTop α
⊢ ⊤ ≤ y →
    ⊤ ≤ z →
      ⊤ ≤
        match y, z with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y z : WithTop α
a✝ : α
⊢ ↑a✝ ≤ y →
    ↑a✝ ≤ z →
      ↑a✝ ≤
        match y, z with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
x y : WithZero α
⊢ x ≤
    match x, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
y : WithZero α
⊢ 0 ≤
    match 0, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
y : WithZero α
a✝ : α
⊢ ↑a✝ ≤
    match ↑a✝, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
x y : WithZero α
⊢ y ≤
    match x, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
y : WithZero α
⊢ y ≤
    match 0, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
y : WithZero α
a✝ : α
⊢ y ≤
    match ↑a✝, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithBot α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y : WithBot α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ y ≤ ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y : WithBot α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithBot α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ y

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y : WithBot α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ y ≤ y

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y : WithBot α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) y ≤ y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
x y z : WithZero α
⊢ x ≤ z →
    y ≤ z →
      (match x, y with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        z

Tactic:
cases x

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
y z : WithZero α
⊢ 0 ≤ z →
    y ≤ z →
      (match 0, y with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        z

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
y z : WithZero α
a✝ : α
⊢ ↑a✝ ≤ z →
    y ≤ z →
      (match ↑a✝, y with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        z
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y z : WithBot α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y z : WithBot α
⊢ ⊥ ≤ y → ⊥ ≤ z → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
floor : α → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
a : α
z : ℤ
⊢ -↑z ≤ -a ↔ a ≤ ↑z

Tactic:
neg_le_neg_iff

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
floor : α → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
a : α
z : ℤ
⊢ a ≤ ↑z ↔ a ≤ ↑z