mathlib-initiative/mathlib-tactics huggingface dataset:
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 + ⊤ → ⊤ ≤ ⊤

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

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

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

Tactic:
<;>

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✝

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.Monoid.Unbundled.WithTop

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

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

Tactic:
<;>

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 → ⊤ ≤ ⊤

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

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

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

Tactic:
<;>

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

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

case coe.top
α : 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.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

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

Tactic:
<;>

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

case coe
α : Type u
inst✝² : Add α
z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝ : α
⊢ ↑a✝ < z → ↑x + ↑a✝ < ↑x + z
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 + ⊤

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

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

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

Tactic:
<;>

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✝

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

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

Tactic:
<;>

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

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

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

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

Tactic:
<;>

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

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

case coe.top
α : 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.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝ : AddMonoid α
⊢ (match ⊤, 0 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    0

pp: case coe
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
⊢ (match ↑a✝, 0 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    0

Tactic:
<;>

Goal state after:
case top
α : Type u
β : Type v
inst✝ : AddMonoid α
⊢ (match ⊤, 0 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    0

case coe
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
⊢ (match ↑a✝, 0 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
⊢ (match ⊤, n + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, n with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

pp: case coe
α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
a✝ : α
⊢ (match ↑a✝, n + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, n with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝

Tactic:
<;>

Goal state after:
case top
α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
⊢ (match ⊤, n + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, n with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

case coe
α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
a✝ : α
⊢ (match ↑a✝, n + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, n with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.zero
α : Type u
β : Type v
inst✝ : AddMonoid α
⊢ (match ⊤, 0 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, 0 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

pp: case top.succ
α : Type u
β : Type v
inst✝ : AddMonoid α
n✝ : ℕ
⊢ (match ⊤, n✝ + 1 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, n✝ + 1 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

pp: case coe.zero
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
⊢ (match ↑a✝, 0 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, 0 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝

pp: case coe.succ
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
n✝ : ℕ
⊢ (match ↑a✝, n✝ + 1 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, n✝ + 1 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝

Tactic:
<;>

Goal state after:
case top.zero
α : Type u
β : Type v
inst✝ : AddMonoid α
⊢ (match ⊤, 0 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, 0 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

case top.succ
α : Type u
β : Type v
inst✝ : AddMonoid α
n✝ : ℕ
⊢ (match ⊤, n✝ + 1 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, n✝ + 1 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

case coe.zero
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
⊢ (match ↑a✝, 0 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, 0 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝

case coe.succ
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
n✝ : ℕ
⊢ (match ↑a✝, n✝ + 1 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, n✝ + 1 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

pp: case coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊥ = ⊥

Tactic:
<;>

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: case bot
α : Type u
inst✝ : Add α
y : WithBot α
⊢ ⊥ + y = ⊥ ↔ ⊥ = ⊥ ∨ y = ⊥

pp: case coe
α : Type u
inst✝ : Add α
y : WithBot α
a✝ : α
⊢ ↑a✝ + y = ⊥ ↔ ↑a✝ = ⊥ ∨ y = ⊥

Tactic:
<;>

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.Sub.Basic

Goal state before:
pp: case neg.mp
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
⊢ 0 ≤ c → a ≤ c + b

pp: case neg.mpr
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
⊢ a ≤ c + b → 0 ≤ c

Tactic:
<;>

Goal state after:
case neg.mp
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
⊢ 0 ≤ c → a ≤ c + b

case neg.mpr
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
⊢ a ≤ c + b → 0 ≤ c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

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

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

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

Tactic:
<;>

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

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

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

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

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

pp: case coe
α : Type u
inst✝ : Add α
y : WithBot α
a✝ : α
⊢ ↑a✝ + y ≠ ⊥ ↔ ↑a✝ ≠ ⊥ ∧ y ≠ ⊥

Tactic:
<;>

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 α
⊢ ⊥ + ⊥ ≠ ⊥ ↔ ⊥ ≠ ⊥ ∧ ⊥ ≠ ⊥

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

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

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

Tactic:
<;>

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

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

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

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

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

pp: case coe
α : Type u
inst✝¹ : Add α
y : WithBot α
inst✝ : IsRightCancelAdd α
z a✝ : α
⊢ ↑a✝ + ↑z = y + ↑z ↔ ↑a✝ = y

Tactic:
<;>

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 ↔ ⊥ = ⊥

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

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

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

Tactic:
<;>

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

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

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

case coe.coe
α : Type u
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
z a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑z = ↑a✝ + ↑z ↔ ↑a✝¹ = ↑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

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

Tactic:
<;>

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

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

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

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

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

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

Tactic:
<;>

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✝

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

pp: 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)

Tactic:
<;>

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

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)

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)

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

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

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)

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)

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

Goal state before:
pp: case bot
α : Type u_1
d y : α
⊢ unbotD d ⊥ = y ↔ ⊥ = ↑y ∨ ⊥ = ⊥ ∧ y = d

pp: case coe
α : Type u_1
d y a✝ : α
⊢ unbotD d ↑a✝ = y ↔ ↑a✝ = ↑y ∨ ↑a✝ = ⊥ ∧ y = d

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
d y : α
⊢ unbotD d ⊥ = y ↔ ⊥ = ↑y ∨ ⊥ = ⊥ ∧ y = d

case coe
α : Type u_1
d y a✝ : α
⊢ unbotD d ↑a✝ = y ↔ ↑a✝ = ↑y ∨ ↑a✝ = ⊥ ∧ y = d
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
d : α
x : WithBot α
⊢ unbotD d x = unbotD d ⊥ ↔ x = ⊥ ∨ x = ↑d ∧ ⊥ = ⊥ ∨ x = ⊥ ∧ ⊥ = ↑d

pp: case coe
α : Type u_1
d : α
x : WithBot α
a✝ : α
⊢ unbotD d x = unbotD d ↑a✝ ↔ x = ↑a✝ ∨ x = ↑d ∧ ↑a✝ = ⊥ ∨ x = ⊥ ∧ ↑a✝ = ↑d

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
d : α
x : WithBot α
⊢ unbotD d x = unbotD d ⊥ ↔ x = ⊥ ∨ x = ↑d ∧ ⊥ = ⊥ ∨ x = ⊥ ∧ ⊥ = ↑d

case coe
α : Type u_1
d : α
x : WithBot α
a✝ : α
⊢ unbotD d x = unbotD d ↑a✝ ↔ x = ↑a✝ ∨ x = ↑d ∧ ↑a✝ = ⊥ ∨ x = ⊥ ∧ ↑a✝ = ↑d
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
d : α
x y : WithBot α
⊢ unbotD d x = unbotD d y ↔ x = y ∨ x = ↑d ∧ y = ⊥ ∨ x = ⊥ ∧ y = ↑d

Tactic:
by
  induction y <;> simp [unbotD_eq_iff, or_comm]

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

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

pp: 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)

Tactic:
<;>

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: case bot
α : Type u_1
β : Type u_2
f : α → β
y : β
⊢ ↑y = map f ⊥ ↔ ∃ x, ⊥ = ↑x ∧ f x = y

pp: case coe
α : Type u_1
β : Type u_2
f : α → β
y : β
a✝ : α
⊢ ↑y = map f ↑a✝ ↔ ∃ x, ↑a✝ = ↑x ∧ f x = y

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
f : α → β
y : β
⊢ ↑y = map f ⊥ ↔ ∃ x, ⊥ = ↑x ∧ f x = y

case coe
α : Type u_1
β : Type u_2
f : α → β
y : β
a✝ : α
⊢ ↑y = map f ↑a✝ ↔ ∃ x, ↑a✝ = ↑x ∧ f x = y
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f ⊥ ⊥ = ⊥

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a✝ : α
⊢ map₂ f ↑a✝ ⊥ = ⊥

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f ⊥ ⊥ = ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a✝ : α
⊢ map₂ f ↑a✝ ⊥ = ⊥
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
⊢ map₂ f ⊥ ↑b = map (fun x ↦ f x b) ⊥

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
a✝ : α
⊢ map₂ f ↑a✝ ↑b = map (fun x ↦ f x b) ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
⊢ map₂ f ⊥ ↑b = map (fun x ↦ f x b) ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
a✝ : α
⊢ map₂ f ↑a✝ ↑b = map (fun x ↦ f x b) ↑a✝