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

Goal state before:
pp: case coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z)

Tactic:
cases z

Goal state after:
case coe.top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ ⊤ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤) ((fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤)

case coe.top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ ↑a✝ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊤) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases z

Goal state after:
case coe.coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝ ⊤ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊤)

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

Goal state after:
case top.top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
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) ⊤ ⊤

case top.top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
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✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases z

Goal state after:
case top.coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
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✝ ⊤

case top.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
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✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases z

Goal state after:
case coe.top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
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) ⊤ ⊤

case coe.top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
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✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases z

Goal state after:
case coe.coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
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✝ ⊤

case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
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✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases z

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

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

Goal state before:
pp: case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithTop α
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

Tactic:
cases z

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

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

Goal state before:
pp: case coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
z : WithTop α
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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

Goal state before:
pp: case top
α : Type u
inst✝² : Add α
z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + ⊤ ≤ ↑x + z → ⊤ ≤ z

Tactic:
cases z

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

case top.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ⊤ ≤ ↑x + ↑a✝ → ⊤ ≤ ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases z

Goal state after:
case coe.top
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ↑a✝ ≤ ↑x + ⊤ → ↑a✝ ≤ ⊤

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b

Tactic:
exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)

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

Goal state before:
pp: case top
α : Type u
inst✝² : Add α
z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ ⊤ < z → ↑x + ⊤ < ↑x + z

Tactic:
cases z

Goal state after:
case top.top
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ ⊤ < ⊤ → ↑x + ⊤ < ↑x + ⊤

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

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

Tactic:
cases z

Goal state after:
case coe.top
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ↑a✝ < ⊤ → ↑x + ↑a✝ < ↑x + ⊤

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

Goal state before:
pp: case bot
α : Type u
inst✝¹ : Add α
z : WithBot α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + ⊥ = ↑x + z ↔ ⊥ = z

Tactic:
cases z

Goal state after:
case bot.bot
α : Type u
inst✝¹ : Add α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + ⊥ = ↑x + ⊥ ↔ ⊥ = ⊥

case bot.coe
α : Type u
inst✝¹ : Add α
inst✝ : IsLeftCancelAdd α
x a✝ : α
⊢ ↑x + ⊥ = ↑x + ↑a✝ ↔ ⊥ = ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
inst✝¹ : Add α
z : WithBot α
inst✝ : IsLeftCancelAdd α
x a✝ : α
⊢ ↑x + ↑a✝ = ↑x + z ↔ ↑a✝ = z

Tactic:
cases z

Goal state after:
case coe.bot
α : Type u
inst✝¹ : Add α
inst✝ : IsLeftCancelAdd α
x a✝ : α
⊢ ↑x + ↑a✝ = ↑x + ⊥ ↔ ↑a✝ = ⊥

case coe.coe
α : Type u
inst✝¹ : Add α
inst✝ : IsLeftCancelAdd α
x a✝¹ a✝ : α
⊢ ↑x + ↑a✝¹ = ↑x + ↑a✝ ↔ ↑a✝¹ = ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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

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

Tactic:
cases z

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

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✝