awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x_1 y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
x y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
coe :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2)
        (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) y)
        (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) z) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) x y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) x z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
top₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2)
        (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α))
        (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a : WithTop α) z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
y z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2)
        (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
          (↑a : WithTop α))
        (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a : WithTop α) z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) y)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
top₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2)
        (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
        (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α)) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a : WithTop α)
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
a_1 : α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) ⊤
top₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2)
        (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
        (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α)) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) (↑a : WithTop α)
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2)
        (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
        (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
          (↑a : WithTop α)) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a : WithTop α)
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
a_1 a_2 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a_2 : WithTop α))
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) ⊤
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2)
        (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
          (↑a_2 : WithTop α))
        (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
          (↑a : WithTop α)) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) (↑a : WithTop α)
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a_2 : WithTop α))
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a_1 : WithTop α)

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) ⊤

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_2 : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α)

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a_2 : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a_2 : WithTop α)

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a_2 : WithTop α))
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) ⊤

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
a_1 a_2 a_3 : α
coe : a_2 + a_1 < a_3 + a_1 → a_2 < a_3
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_4 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a_2 : WithTop α))
      (swap (φ := fun (a a_4 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a_3 : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) (↑a_3 : WithTop α)

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
a_1 a_2 a_3 : α
⊢ a_2 + a_1 < a_3 + a_1 → a_2 < a_3

Tactic:
simpa using lt_of_add_lt_add_right

Premises used: lt_of_add_lt_add_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
hx : x ≠ ⊤
⊢ x ≠ ⊤

Tactic:
hx
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
hx : x ≠ ⊤
lift : ∀ (x : α), (↑x : WithTop α) + y ≤ (↑x : WithTop α) + z → y ≤ z
⊢ x + y ≤ x + z → y ≤ z

Tactic:
lift x to α using hx
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x : α
top : (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + z → ⊤ ≤ z
coe : ∀ (a : α), (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + z → (↑a : WithTop α) ≤ z
⊢ (↑x : WithTop α) + y ≤ (↑x : WithTop α) + z → y ≤ z

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x : α
top : (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + ⊤ → LE.le.{u} (α := WithTop α) ⊤ ⊤
top₁ : ∀ (a : α), (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + (↑a : WithTop α) → ⊤ ≤ (↑a : WithTop α)
⊢ (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + z → ⊤ ≤ z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a : α
coe : (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + ⊤ → (↑a : WithTop α) ≤ ⊤
coe₁ :
  ∀ (a_1 : α),
    (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + (↑a_1 : WithTop α) → (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
⊢ (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + z → (↑a : WithTop α) ≤ z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x : α
⊢ (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + ⊤ → LE.le.{u} (α := WithTop α) ⊤ ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a : α
⊢ (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + (↑a : WithTop α) → ⊤ ≤ (↑a : WithTop α)

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a : α
⊢ (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + ⊤ → (↑a : WithTop α) ≤ ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a a_1 : α
coe : x + a ≤ x + a_1 → a ≤ a_1
⊢ (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + (↑a_1 : WithTop α) → (↑a : WithTop α) ≤ (↑a_1 : WithTop α)

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a a_1 : α
⊢ x + a ≤ x + a_1 → a ≤ a_1

Tactic:
simpa using le_of_add_le_add_left

Premises used: le_of_add_le_add_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
hz : z ≠ ⊤
⊢ z ≠ ⊤

Tactic:
hz
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
hz : z ≠ ⊤
lift : ∀ (z : α), x + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → x ≤ y
⊢ x + z ≤ y + z → x ≤ y

Tactic:
lift z to α using hz
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z : α
top : ⊤ + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → ⊤ ≤ y
coe : ∀ (a : α), (↑a : WithTop α) + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → (↑a : WithTop α) ≤ y
⊢ x + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → x ≤ y

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z : α
top : ⊤ + (↑z : WithTop α) ≤ ⊤ + (↑z : WithTop α) → LE.le.{u} (α := WithTop α) ⊤ ⊤
top₁ : ∀ (a : α), ⊤ + (↑z : WithTop α) ≤ (↑a : WithTop α) + (↑z : WithTop α) → ⊤ ≤ (↑a : WithTop α)
⊢ ⊤ + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → ⊤ ≤ y

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z a : α
coe : (↑a : WithTop α) + (↑z : WithTop α) ≤ ⊤ + (↑z : WithTop α) → (↑a : WithTop α) ≤ ⊤
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithTop α) + (↑z : WithTop α) ≤ (↑a_1 : WithTop α) + (↑z : WithTop α) → (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
⊢ (↑a : WithTop α) + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → (↑a : WithTop α) ≤ y

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z : α
⊢ ⊤ + (↑z : WithTop α) ≤ ⊤ + (↑z : WithTop α) → LE.le.{u} (α := WithTop α) ⊤ ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z a : α
⊢ ⊤ + (↑z : WithTop α) ≤ (↑a : WithTop α) + (↑z : WithTop α) → ⊤ ≤ (↑a : WithTop α)

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z a : α
⊢ (↑a : WithTop α) + (↑z : WithTop α) ≤ ⊤ + (↑z : WithTop α) → (↑a : WithTop α) ≤ ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z a a_1 : α
coe : a + z ≤ a_1 + z → a ≤ a_1
⊢ (↑a : WithTop α) + (↑z : WithTop α) ≤ (↑a_1 : WithTop α) + (↑z : WithTop α) → (↑a : WithTop α) ≤ (↑a_1 : WithTop α)

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z a a_1 : α
⊢ a + z ≤ a_1 + z → a ≤ a_1

Tactic:
simpa using le_of_add_le_add_right

Premises used: le_of_add_le_add_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
hx : x ≠ ⊤
⊢ x ≠ ⊤

Tactic:
hx
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
hx : x ≠ ⊤
lift : ∀ (x : α), y < z → (↑x : WithTop α) + y < (↑x : WithTop α) + z
⊢ y < z → x + y < x + z

Tactic:
lift x to α using hx
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x : α
top : ⊤ < z → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + z
coe : ∀ (a : α), (↑a : WithTop α) < z → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + z
⊢ y < z → (↑x : WithTop α) + y < (↑x : WithTop α) + z

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x : α
top : LT.lt.{u} (α := WithTop α) ⊤ ⊤ → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + ⊤
top₁ : ∀ (a : α), ⊤ < (↑a : WithTop α) → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + (↑a : WithTop α)
⊢ ⊤ < z → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a : α
coe : (↑a : WithTop α) < ⊤ → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + ⊤
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithTop α) < (↑a_1 : WithTop α) → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + (↑a_1 : WithTop α)
⊢ (↑a : WithTop α) < z → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x : α
⊢ LT.lt.{u} (α := WithTop α) ⊤ ⊤ → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a : α
⊢ ⊤ < (↑a : WithTop α) → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + (↑a : WithTop α)

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a : α
⊢ (↑a : WithTop α) < ⊤ → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a a_1 : α
coe : a < a_1 → x + a < x + a_1
⊢ (↑a : WithTop α) < (↑a_1 : WithTop α) → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + (↑a_1 : WithTop α)

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a a_1 : α
h : a < a_1
⊢ x + a < x + a_1

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a a_1 : α
⊢ a < a_1 → x + a < x + a_1

Tactic:
simpa using fun _ ↦ by gcongr
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
hz : z ≠ ⊤
⊢ z ≠ ⊤

Tactic:
hz
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
hz : z ≠ ⊤
lift : ∀ (z : α), x < y → x + (↑z : WithTop α) < y + (↑z : WithTop α)
⊢ x < y → x + z < y + z

Tactic:
lift z to α using hz
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z : α
top : ⊤ < y → ⊤ + (↑z : WithTop α) < y + (↑z : WithTop α)
coe : ∀ (a : α), (↑a : WithTop α) < y → (↑a : WithTop α) + (↑z : WithTop α) < y + (↑z : WithTop α)
⊢ x < y → x + (↑z : WithTop α) < y + (↑z : WithTop α)

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z : α
top : LT.lt.{u} (α := WithTop α) ⊤ ⊤ → ⊤ + (↑z : WithTop α) < ⊤ + (↑z : WithTop α)
top₁ : ∀ (a : α), ⊤ < (↑a : WithTop α) → ⊤ + (↑z : WithTop α) < (↑a : WithTop α) + (↑z : WithTop α)
⊢ ⊤ < y → ⊤ + (↑z : WithTop α) < y + (↑z : WithTop α)

Tactic:
cases y