mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
cases y

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

Tactic:
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✝ ≤ ⊥
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 : WithBot α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 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✝ : 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.Order.WithBot

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

Tactic:
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✝
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 : WithBot α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) y ≤ 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✝ : 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: 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

Tactic:
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
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
cases y

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

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

Tactic:
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
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
cases y

Goal state after:
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: case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ 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✝ : 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✝
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 : WithTop α
a✝ : α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) 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✝ : 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: case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 y ≤ y

Tactic:
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✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
cases y

Goal state after:
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: case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y z : WithZero α
⊢ 0 ≤ y → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
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
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
cases y

Goal state after:
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
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✝ : SemilatticeSup α
y z : WithTop α
⊢ ⊤ ≤ z → y ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y ≤ z

Tactic:
cases y

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

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

Tactic:
cases y

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

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithZero α
⊢ 0 ≤ y ∨ y ≤ 0

Tactic:
cases y

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ 0 ≤ 0 ∨ 0 ≤ 0

case zero.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ 0 ≤ ↑a✝ ∨ ↑a✝ ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithZero α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑a✝

Tactic:
cases y

Goal state after:
case coe.zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ 0 ∨ 0 ≤ ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ∨ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LE α
y : WithZero α
a x : α
h : ↑x ≤ y
⊢ unzeroD a ↑x ≤ unzeroD a y

Tactic:
cases y

Goal state after:
case zero
α : Type u_1
inst✝ : LE α
a x : α
h : ↑x ≤ 0
⊢ unzeroD a ↑x ≤ unzeroD a 0

case coe
α : Type u_1
inst✝ : LE α
a x a✝ : α
h : ↑x ≤ ↑a✝
⊢ unzeroD a ↑x ≤ unzeroD 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✝ : DistribLattice α
y z : WithBot α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ 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✝ : DistribLattice α
z : WithBot α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝ : α
⊢ (⊥ ⊔ ↑a✝) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ↑a✝ ⊓ 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✝ : DistribLattice α
y z : WithBot α
a✝ : α
⊢ (↑a✝ ⊔ y) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ y ⊓ 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✝ : DistribLattice α
z : WithBot α
a✝ : α
⊢ (↑a✝ ⊔ ⊥) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ ⊥ ⊓ z

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ z
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

Tactic:
← le_floor_iff' hn,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑n + 1
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✝ : DistribLattice α
y z : WithTop α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z

Tactic:
cases y

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ z

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝ : α
⊢ (⊤ ⊔ ↑a✝) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ↑a✝ ⊓ 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✝ : DistribLattice α
y z : WithTop α
a✝ : α
⊢ (↑a✝ ⊔ y) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ y ⊓ z

Tactic:
cases y

Goal state after:
case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝ : α
⊢ (↑a✝ ⊔ ⊤) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ ⊤ ⊓ z

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑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 α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithBot α
⊢ ⊥ ≤ 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✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ⊥ ≤ ⊥ ∨ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ⊥ ≤ ↑a✝ ∨ ↑a✝ ≤ ⊥
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✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithBot α
a✝ : α
⊢ ↑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✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ ⊥ ∨ ⊥ ≤ ↑a✝

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

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithTop α
⊢ ⊤ ≤ y ∨ 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✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ⊤ ≤ ⊤ ∨ ⊤ ≤ ⊤

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ⊤ ≤ ↑a✝ ∨ ↑a✝ ≤ ⊤
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✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithTop α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑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✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ ⊤ ∨ ⊤ ≤ ↑a✝

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

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

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 α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
⊢ ⊥ < ⊥ ∨ ⊥ = ⊥ ∨ ⊥ < ⊥

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

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

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

Tactic:
cases y

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

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ⊤ < ↑a✝ ∨ ⊤ = ↑a✝ ∨ ↑a✝ < ⊤
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 α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
y : WithTop α
a✝ : α
⊢ ↑a✝ < y ∨ ↑a✝ = y ∨ y < ↑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✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
a✝ : α
⊢ ↑a✝ < ⊤ ∨ ↑a✝ = ⊤ ∨ ⊤ < ↑a✝

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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

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

Tactic:
cases y

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

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