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✝ : Preorder α
x y z : WithBot α
⊢ x ≤ y → y ≤ z → x ≤ z

Tactic:
cases x <;> 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

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

Tactic:
cases x <;> 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✝

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: α : 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 <;> 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✝ ≤ ⊥

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 α
x y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z

Tactic:
cases x <;> 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

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: α : 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 <;> 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✝

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: α : 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 <;> 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✝

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: α : 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 <;> 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)

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: α : 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 <;> 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)

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: α : 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 <;> 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

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.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 <;> 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)) ≤
    ⊤

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: α : 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 <;> 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✝

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: α : 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 <;> 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)

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: α : 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 <;> 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)

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.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 <;> cases y

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

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

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝¹
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 <;> 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)

case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤
    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.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 <;> cases y

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

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

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝
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 <;> cases y

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

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

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

case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
z : WithZero α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ z →
    ↑a✝ ≤ z →
      (match ↑a✝¹, ↑a✝ 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 <;> cases y

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

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

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

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithBot α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ z → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z
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 : WithTop α
⊢ x ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y

Tactic:
cases x <;> cases y

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ x

Tactic:
cases x <;> cases y

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0 ≤ 0

case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝ ≤ 0

case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0 ≤ ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑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✝ : SemilatticeSup α
x y : WithTop α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y

Tactic:
cases x <;> cases y

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ y

Tactic:
cases x <;> cases y

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0 ≤ 0

case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝ ≤ ↑a✝

case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0 ≤ 0

case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y z : WithZero α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
cases x <;> cases y

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
⊢ 0 ≤ 0 → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 z

case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝ : α
⊢ 0 ≤ ↑a✝ → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z

case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝ : α
⊢ ↑a✝ ≤ 0 → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 z

case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ z → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z