awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
y z : WithBot α
a_1 : α
coe :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ z
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) (↑a : WithBot α))
        ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a : WithBot α) z
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z) →
    (fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithBot α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ ⊥
bot₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
        ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a : WithBot α)) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ (↑a : WithBot α)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z) →
    (fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithBot α
a_1 : α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α))
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_1 : WithBot α) ⊥
bot₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α))
        ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a : WithBot α)) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_1 : WithBot α) (↑a : WithBot α)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α))
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_1 : WithBot α) z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithBot α
a_1 : α
coe :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ ⊥
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥)
        ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) (↑a : WithBot α)) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ (↑a : WithBot α)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z) →
    (fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithBot α
a_1 a_2 : α
coe :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) (↑a_2 : WithBot α))
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_2 : WithBot α) ⊥
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) (↑a_2 : WithBot α))
        ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) (↑a : WithBot α)) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_2 : WithBot α) (↑a : WithBot α)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) (↑a_2 : WithBot α))
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_2 : WithBot α) z

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

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
a_1 : α
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α)) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ (↑a_1 : WithBot α)

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
a_1 : α
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α))
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_1 : WithBot α) ⊥

Tactic:
simp [← coe_add]

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

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
a_1 : α
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ ⊥

Tactic:
simp [← coe_add]

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

Tactic:
simp [← coe_add]

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

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithBot α
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 : WithBot α) ↦ x1 < x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) (↑a_2 : WithBot α))
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) (↑a_3 : WithBot α)) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_2 : WithBot α) (↑a_3 : WithBot α)

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithBot α
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
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x_1 y_1 z_1 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
x y z : WithBot α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ y)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) y z
coe :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2)
        (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a : WithBot α) y)
        (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a : WithBot α) z) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) y z
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) x y)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) x z) →
    (fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
y z : WithBot α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ z
bot₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2)
        (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a : WithBot α))
        (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a : WithBot α) z
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ y)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z) →
    (fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
y z : WithBot α
a_1 : α
coe :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥)
      (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ z
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2)
        (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α)
          (↑a : WithBot α))
        (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a : WithBot α) z
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) y)
      (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z) →
    (fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithBot α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ ⊥
bot₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2)
        (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
        (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a : WithBot α)) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) ⊥ (↑a : WithBot α)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      (swap (φ := fun (a a_1 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z) →
    (fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithBot α
a_1 : α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α))
      (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_1 : WithBot α) ⊥
bot₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 < x2)
        (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α))
        (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a : WithBot α)) →
      (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_1 : WithBot α) (↑a : WithBot α)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α))
      (swap (φ := fun (a a_2 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_1 : WithBot α) z

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

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

Tactic:
simp [← coe_add, swap]

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

Tactic:
simp [← coe_add, swap]

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

Tactic:
simp [← coe_add, swap]

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

Tactic:
simp [← coe_add, swap]

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

Tactic:
simp [← coe_add, swap]

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

Tactic:
simp [← coe_add, swap]

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

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithBot α
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 : WithBot α) ↦ x1 < x2)
      (swap (φ := fun (a a_4 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α)
        (↑a_2 : WithBot α))
      (swap (φ := fun (a a_4 : WithBot α) ↦ WithBot α) (fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α)
        (↑a_3 : WithBot α)) →
    (fun (x1 x2 : WithBot α) ↦ x1 < x2) (↑a_2 : WithBot α) (↑a_3 : WithBot α)

Tactic:
simp [← coe_add, swap]

Premises used: Function.swap, WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithBot α
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 : WithBot α
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 : WithBot α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
hx : x ≠ ⊥
lift : ∀ (x : α), (↑x : WithBot α) + y ≤ (↑x : WithBot α) + 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 : WithBot α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x : α
bot : (↑x : WithBot α) + ⊥ ≤ (↑x : WithBot α) + z → ⊥ ≤ z
coe : ∀ (a : α), (↑x : WithBot α) + (↑a : WithBot α) ≤ (↑x : WithBot α) + z → (↑a : WithBot α) ≤ z
⊢ (↑x : WithBot α) + y ≤ (↑x : WithBot α) + z → y ≤ z

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

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

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

Tactic:
simp [← coe_add]

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

Tactic:
simp [← coe_add]

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

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add