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 : LE α
inst_2 : AddRightMono α
x y z : WithTop α
top :
  (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) ⊤ y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
coe :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
      (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2)
        (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) y)
        (swap (φ := fun (a a_2 : 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)

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 : LE α
inst_2 : AddRightMono α
y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ z →
    (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)
top₁ :
  ∀ (a : α),
    (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 : WithTop α))
        (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ 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) ⊤ y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ 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 : LE α
inst_2 : AddRightMono α
y z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ z →
    (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)
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a : WithTop α) z →
      (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2)
        (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
          (↑a : WithTop α))
        (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z)
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y 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)

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 : LE α
inst_2 : AddRightMono α
z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ ⊤ →
    (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) ⊤ ⊤)
top₁ :
  ∀ (a : α),
    (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) ⊤ ⊤)
        (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α))
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ z →
    (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)

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 : LE α
inst_2 : AddRightMono α
z : WithTop α
a_1 : α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_1 : 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) ⊤ ⊤)
top₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_1 : 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 α))
        (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α))
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_1 : WithTop α) z →
    (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)

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 : LE α
inst_2 : AddRightMono α
z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ ⊤ →
    (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 α) ⊤)
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ (↑a : WithTop α) →
      (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 : WithTop α))
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ z →
    (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)

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 : LE α
inst_2 : AddRightMono α
z : WithTop α
a_1 a_2 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_2 : 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 α) ⊤)
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_2 : WithTop α) (↑a : WithTop α) →
      (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 : WithTop α))
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_2 : WithTop α) z →
    (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)

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 : LE α
inst_2 : AddRightMono α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ ⊤ →
    (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) ⊤ ⊤)

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 : LE α
inst_2 : AddRightMono α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ (↑a_1 : WithTop α) →
    (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 α))

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 : LE α
inst_2 : AddRightMono α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_1 : 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) ⊤ ⊤)

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 : LE α
inst_2 : AddRightMono α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α) →
    (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 α))

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 : LE α
inst_2 : AddRightMono α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ ⊤ →
    (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 α) ⊤)

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 : LE α
inst_2 : AddRightMono α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ (↑a_2 : WithTop α) →
    (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 α))

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 : LE α
inst_2 : AddRightMono α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_2 : 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 α) ⊤)

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 : LE α
inst_2 : AddRightMono α
a_1 a_2 a_3 : α
coe : a_2 ≤ a_3 → a_2 + a_1 ≤ a_3 + a_1
⊢ (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a_2 : WithTop α) (↑a_3 : WithTop α) →
    (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 α))

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 : LE α
inst_2 : AddRightMono α
a_1 a_2 a_3 : α
h : a_2 ≤ a_3
⊢ a_2 + a_1 ≤ a_3 + a_1

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LE α
inst_2 : AddRightMono α
a_1 a_2 a_3 : α
⊢ a_2 ≤ a_3 → a_2 + a_1 ≤ a_3 + a_1

Tactic:
simpa using fun _ ↦ by gcongr
-- 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 : AddLeftReflectLT α
x y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
coe :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) y)
        ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) z) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) x y)
      ((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 : AddLeftReflectLT α
y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
top₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α))
        ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a : WithTop α) z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((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 : AddLeftReflectLT α
y z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : 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) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a : 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) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) y)
      ((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 : AddLeftReflectLT α
z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
top₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
        ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α)) →
      (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a : WithTop α)
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((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 : AddLeftReflectLT α
z : WithTop α
a_1 : α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) ⊤
top₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : 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) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : 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 : AddLeftReflectLT α
z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : 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) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : 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 : AddLeftReflectLT α
z : WithTop α
a_1 a_2 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : 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) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : 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) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : 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 : AddLeftReflectLT α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤

Tactic:
simp [← coe_add]

Premises used: 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 : AddLeftReflectLT α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a_1 : WithTop α)

Tactic:
simp [← coe_add]

Premises used: 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 : AddLeftReflectLT α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) ⊤

Tactic:
simp [← coe_add]

Premises used: 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 : AddLeftReflectLT α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : 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]

Premises used: 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 : AddLeftReflectLT α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤

Tactic:
simp [← coe_add]

Premises used: 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 : AddLeftReflectLT α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : 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]

Premises used: 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 : AddLeftReflectLT α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) ⊤

Tactic:
simp [← coe_add]

Premises used: 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 : AddLeftReflectLT α
a_1 a_2 a_3 : α
coe : a_1 + a_2 < a_1 + a_3 → a_2 < a_3
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : 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]

Premises used: 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 : AddLeftReflectLT α
a_1 a_2 a_3 : α
⊢ a_1 + a_2 < a_1 + a_3 → a_2 < a_3

Tactic:
simpa using lt_of_add_lt_add_left

Premises used: lt_of_add_lt_add_left