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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
cases x

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

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

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

Tactic:
cases x

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

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
cases x

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

case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
y z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) y) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z) →
    (fun x1 x2 ↦ x1 < x2) y z
Module: Mathlib.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 : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a < b + c → a - b < c

Tactic:
intro h

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b < c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
cases x

Goal state after:
case top
α : Type u
inst✝² : Add α
y : WithTop α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ ⊤ + ↑z ≤ y + ↑z → ⊤ ≤ y

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

Goal state after:
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: α : Type u
inst✝² : Add α
x y : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z

Tactic:
cases x

Goal state after:
case top
α : Type u
inst✝² : Add α
y : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ ⊤ < y → ⊤ + ↑z < y + ↑z

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

Goal state before:
pp: α : Type u
inst✝ : Add α
x : WithBot α
⊢ x + ⊥ = ⊥

Tactic:
cases x

Goal state after:
case bot
α : Type u
inst✝ : Add α
⊢ ⊥ + ⊥ = ⊥

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

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithBot α
⊢ x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

Tactic:
cases x

Goal state after:
case bot
α : Type u
inst✝ : Add α
y : WithBot α
⊢ ⊥ + y = ⊥ ↔ ⊥ = ⊥ ∨ y = ⊥

case coe
α : Type u
inst✝ : Add α
y : WithBot α
a✝ : α
⊢ ↑a✝ + y = ⊥ ↔ ↑a✝ = ⊥ ∨ y = ⊥
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
inst✝ : Add α
⊢ ⊥ + ⊥ = ⊥ ↔ ⊥ = ⊥ ∨ ⊥ = ⊥

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case bot.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊥ + ↑a✝ = ⊥ ↔ ⊥ = ⊥ ∨ ↑a✝ = ⊥

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case coe.bot
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊥ = ⊥ ↔ ↑a✝ = ⊥ ∨ ⊥ = ⊥

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ = ⊥ ↔ ↑a✝¹ = ⊥ ∨ ↑a✝ = ⊥

Tactic:
simp [← coe_add]

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

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithBot α
⊢ x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

Tactic:
cases x

Goal state after:
case bot
α : Type u
inst✝ : Add α
y : WithBot α
⊢ ⊥ + y ≠ ⊥ ↔ ⊥ ≠ ⊥ ∧ y ≠ ⊥

case coe
α : Type u
inst✝ : Add α
y : WithBot α
a✝ : α
⊢ ↑a✝ + y ≠ ⊥ ↔ ↑a✝ ≠ ⊥ ∧ y ≠ ⊥
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot
α : Type u
inst✝ : Add α
⊢ ⊥ + ⊥ ≠ ⊥ ↔ ⊥ ≠ ⊥ ∧ ⊥ ≠ ⊥

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case bot.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊥ + ↑a✝ ≠ ⊥ ↔ ⊥ ≠ ⊥ ∧ ↑a✝ ≠ ⊥

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case coe.bot
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊥ ≠ ⊥ ↔ ↑a✝ ≠ ⊥ ∧ ⊥ ≠ ⊥

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ ≠ ⊥ ↔ ↑a✝¹ ≠ ⊥ ∧ ↑a✝ ≠ ⊥

Tactic:
simp [← coe_add]

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

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y : WithBot α
inst✝ : IsRightCancelAdd α
z : α
⊢ x + ↑z = y + ↑z ↔ x = y

Tactic:
cases x

Goal state after:
case bot
α : Type u
inst✝¹ : Add α
y : WithBot α
inst✝ : IsRightCancelAdd α
z : α
⊢ ⊥ + ↑z = y + ↑z ↔ ⊥ = y

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

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

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case bot.coe
α : Type u
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
z a✝ : α
⊢ ⊥ + ↑z = ↑a✝ + ↑z ↔ ⊥ = ↑a✝

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case coe.bot
α : Type u
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
z a✝ : α
⊢ ↑a✝ + ↑z = ⊥ + ↑z ↔ ↑a✝ = ⊥

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
cases x

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

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
cases x

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

case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
y z : WithBot α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) y) (swap (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
e : α ≃ β
x : WithBot α
⊢ WithBot.map (⇑e.symm) (WithBot.map (⇑e) x) = x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ WithBot.map (⇑e.symm) (WithBot.map ⇑e ⊥) = ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a✝ : α
⊢ WithBot.map (⇑e.symm) (WithBot.map ⇑e ↑a✝) = ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
x : WithBot β
⊢ WithBot.map (⇑e) (WithBot.map (⇑e.symm) x) = x

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
⊢ WithBot.map (⇑e) (WithBot.map ⇑e.symm ⊥) = ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
a✝ : β
⊢ WithBot.map (⇑e) (WithBot.map ⇑e.symm ↑a✝) = ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases x

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

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot α
⊢ x ≤ y ↔ ∀ (a : α), x = ↑a → ∃ b, y = ↑b ∧ a ≤ b

Tactic:
cases x

Goal state after:
case bot
α : Type u_1
inst✝ : LE α
y : WithBot α
⊢ ⊥ ≤ y ↔ ∀ (a : α), ⊥ = ↑a → ∃ b, y = ↑b ∧ a ≤ b

case coe
α : Type u_1
inst✝ : LE α
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y ↔ ∀ (a : α), ↑a✝ = ↑a → ∃ b, y = ↑b ∧ a ≤ b