mathlib-initiative/mathlib-tactics huggingface dataset:
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

Tactic:
cases y

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

Goal state before:
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:
cases y

Goal state after:
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: α : Type u_1
a : α
inst✝ : LE α
y : WithBot α
x : α
h : ↑x ≤ y
⊢ unbotD a ↑x ≤ unbotD a y

Tactic:
cases y

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

Tactic:
cases y

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
Module: Mathlib.Order.WithBot

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

Tactic:
cases y

Goal state after:
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: α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ x < y ↔ ∃ b, y = ↑b ∧ x < ↑b

Tactic:
cases y

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: α : Type u
inst✝² : Add α
y z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z

Tactic:
cases y

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

Tactic:
cases y

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
Module: Mathlib.Order.WithBot

Goal state before:
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:
cases y

Goal state after:
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

Tactic:
cases y

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

case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝ : α
⊢ ⊥ + ↑z ≤ ↑a✝ + ↑z → ⊥ ≤ ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑z ≤ ↑a✝ + ↑z → ↑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 ≤ ⊥

Tactic:
cases y

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

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ⊥ ≤ ↑a✝ ∧ ¬↑a✝ ≤ ⊥
Module: Mathlib.Order.WithBot

Goal state before:
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:
cases y

Goal state after:
case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ < ⊥ ↔ ↑a✝ ≤ ⊥ ∧ ¬⊥ ≤ ↑a✝

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

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

Tactic:
cases y

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

case coe
α : Type u
inst✝² : Add α
z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ↑a✝ < z → ↑x + ↑a✝ < ↑x + z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

case bot.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝ : α
⊢ ⊥ < ↑a✝ → ⊥ + ↑z < ↑a✝ + ↑z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases y

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

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

Goal state before:
pp: 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

Tactic:
cases y

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

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

Goal state before:
pp: 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

Tactic:
cases y

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

case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a✝¹ a✝ : α
⊢ map f ↑a✝¹ ≤ map f ↑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✝ : PartialOrder α
y : WithBot α
⊢ ⊥ ≤ y → y ≤ ⊥ → ⊥ = y

Tactic:
cases y

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

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

Goal state before:
pp: 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

Tactic:
cases y

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
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✝ : 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)

Tactic:
cases y

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

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊥ ≤
    match ⊥, ↑a✝ 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: 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)

Tactic:
cases y

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤
    match ↑a✝¹, ↑a✝ 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: 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)

Tactic:
cases y

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

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤
    match ⊥, ↑a✝ 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: 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)

Tactic:
cases y

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝ ≤
    match ↑a✝¹, ↑a✝ 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: 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

Tactic:
cases y

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

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithBot α
a✝ : α
⊢ ⊥ ≤ z →
    ↑a✝ ≤ z →
      (match ⊥, ↑a✝ 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: 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

Tactic:
cases y

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

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ b
⊢ ofAdd (toAdd (unzero ha)) ≤ ofAdd b

Tactic:
ofAdd_le

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ b
⊢ toAdd (unzero ha) ≤ b
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✝ : 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)) ≤
    ⊤

Tactic:
cases y

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

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ (match ⊤, ↑a✝ 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: 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✝

Tactic:
cases y

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ (match ↑a✝¹, ↑a✝ 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: 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

Tactic:
cases y

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

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ (match ⊤, ↑a✝ 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: 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

Tactic:
cases y

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ (match ↑a✝¹, ↑a✝ 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: 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)

Tactic:
cases y

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

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithTop α
a✝ : α
⊢ ⊤ ≤ ↑a✝ →
    ⊤ ≤ z →
      ⊤ ≤
        match ↑a✝, z 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: 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)

Tactic:
cases y

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithTop α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ →
    ↑a✝¹ ≤ z →
      ↑a✝¹ ≤
        match ↑a✝, 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: 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)

Tactic:
cases y

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

case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤
    match 0, ↑a✝ 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: 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)

Tactic:
cases y

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

case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤
    match ↑a✝¹, ↑a✝ 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: 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)

Tactic:
cases y

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

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