awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithTop α
top : HAdd.hAdd (α := WithTop α) ⊤ ⊤ = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ Eq.{u + 1} (α := WithTop α) ⊤ ⊤
top₁ : ∀ (a : α), ⊤ + (↑a : WithTop α) = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ (↑a : WithTop α) = ⊤
⊢ ⊤ + y = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ y = ⊤

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithTop α
a : α
coe : (↑a : WithTop α) + ⊤ = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ Eq.{u + 1} (α := WithTop α) ⊤ ⊤
coe₁ : ∀ (a_1 : α), (↑a : WithTop α) + (↑a_1 : WithTop α) = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ (↑a_1 : WithTop α) = ⊤
⊢ (↑a : WithTop α) + y = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ y = ⊤

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
⊢ HAdd.hAdd (α := WithTop α) ⊤ ⊤ = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ Eq.{u + 1} (α := WithTop α) ⊤ ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
⊢ ⊤ + (↑a : WithTop α) = ⊤ ↔ Eq.{u + 1} (α := WithTop α) ⊤ ⊤ ∨ (↑a : WithTop α) = ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
⊢ (↑a : WithTop α) + ⊤ = ⊤ ↔ (↑a : WithTop α) = ⊤ ∨ Eq.{u + 1} (α := WithTop α) ⊤ ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a a_1 : α
⊢ (↑a : 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 α
x y : WithTop α
top : ⊤ + y ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ y ≠ ⊤
coe : ∀ (a : α), (↑a : WithTop α) + y ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithTop α
top : HAdd.hAdd (α := WithTop α) ⊤ ⊤ ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne.{u + 1} (α := WithTop α) ⊤ ⊤
top₁ : ∀ (a : α), ⊤ + (↑a : WithTop α) ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ (↑a : WithTop α) ≠ ⊤
⊢ ⊤ + y ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ y ≠ ⊤

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithTop α
a : α
coe : (↑a : WithTop α) + ⊤ ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ Ne.{u + 1} (α := WithTop α) ⊤ ⊤
coe₁ : ∀ (a_1 : α), (↑a : WithTop α) + (↑a_1 : WithTop α) ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ (↑a_1 : WithTop α) ≠ ⊤
⊢ (↑a : WithTop α) + y ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ y ≠ ⊤

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
⊢ HAdd.hAdd (α := WithTop α) ⊤ ⊤ ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne.{u + 1} (α := WithTop α) ⊤ ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
⊢ ⊤ + (↑a : WithTop α) ≠ ⊤ ↔ Ne.{u + 1} (α := WithTop α) ⊤ ⊤ ∧ (↑a : WithTop α) ≠ ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
⊢ (↑a : WithTop α) + ⊤ ≠ ⊤ ↔ (↑a : WithTop α) ≠ ⊤ ∧ Ne.{u + 1} (α := WithTop α) ⊤ ⊤

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a a_1 : α
⊢ (↑a : 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 α
x y : WithTop α
inst_1 : LT α
simp_rw : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
⊢ x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤

Tactic:
simp_rw [WithTop.lt_top_iff_ne_top, add_ne_top]

Premises used: WithTop.add_ne_top, WithTop.lt_top_iff_ne_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
b : WithTop α
c : α
⊢ ⊤ + b = (↑c : WithTop α) ↔ ∃ (a' : α), ∃ (b' : α), (↑a' : WithTop α) = ⊤ ∧ (↑b' : WithTop α) = b ∧ a' + b' = c

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a c : α
⊢ (↑a : WithTop α) + ⊤ = (↑c : WithTop α) ↔
    ∃ (a' : α), ∃ (b' : α), (↑a' : WithTop α) = (↑a : WithTop α) ∧ (↑b' : WithTop α) = ⊤ ∧ a' + b' = c

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a b c : α
norm_cast : a + b = c ↔ ∃ (a' : α), ∃ (b' : α), a' = a ∧ b' = b ∧ a' + b' = c
⊢ (↑a : WithTop α) + (↑b : WithTop α) = (↑c : WithTop α) ↔
    ∃ (a' : α), ∃ (b' : α), (↑a' : WithTop α) = (↑a : WithTop α) ∧ (↑b' : WithTop α) = (↑b : WithTop α) ∧ a' + b' = c

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a b c : α
⊢ a + b = c ↔ ∃ (a' : α), ∃ (b' : α), a' = a ∧ b' = b ∧ a' + b' = c

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x : WithTop α
b : α
⊢ x + (↑b : WithTop α) = ⊤ ↔ x = ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithTop α
a : α
⊢ (↑a : WithTop α) + y = ⊤ ↔ y = ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddLeftRegular a
⊢ Eq.{u + 1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) + x) none)
      ((fun (x : WithTop α) ↦ (↑a : WithTop α) + x) none) →
    Eq.{u + 1} (α := WithTop α) none none

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Premises used: Function.Injective.eq_iff, WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddLeftRegular a
c : α
⊢ Eq.{u + 1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) + x) none)
      ((fun (x : WithTop α) ↦ (↑a : WithTop α) + x) (Option.some c)) →
    none = Option.some c

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Premises used: Function.Injective.eq_iff, WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddLeftRegular a
b : α
⊢ Eq.{u + 1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) + x) (Option.some b))
      ((fun (x : WithTop α) ↦ (↑a : WithTop α) + x) none) →
    Option.some b = none

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Premises used: Function.Injective.eq_iff, WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ Eq.{u + 1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) + x) (Option.some b))
      ((fun (x : WithTop α) ↦ (↑a : WithTop α) + x) (Option.some c)) →
    Option.some b = Option.some c

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Premises used: Function.Injective.eq_iff, WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddRightRegular a
⊢ Eq.{u + 1} (α := WithTop α) ((fun (x : WithTop α) ↦ x + (↑a : WithTop α)) none)
      ((fun (x : WithTop α) ↦ x + (↑a : WithTop α)) none) →
    Eq.{u + 1} (α := WithTop α) none none

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Premises used: Function.Injective.eq_iff, WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddRightRegular a
c : α
⊢ Eq.{u + 1} (α := WithTop α) ((fun (x : WithTop α) ↦ x + (↑a : WithTop α)) none)
      ((fun (x : WithTop α) ↦ x + (↑a : WithTop α)) (Option.some c)) →
    none = Option.some c

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Premises used: Function.Injective.eq_iff, WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddRightRegular a
b : α
⊢ Eq.{u + 1} (α := WithTop α) ((fun (x : WithTop α) ↦ x + (↑a : WithTop α)) (Option.some b))
      ((fun (x : WithTop α) ↦ x + (↑a : WithTop α)) none) →
    Option.some b = none

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Premises used: Function.Injective.eq_iff, WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ Eq.{u + 1} (α := WithTop α) ((fun (x : WithTop α) ↦ x + (↑a : WithTop α)) (Option.some b))
      ((fun (x : WithTop α) ↦ x + (↑a : WithTop α)) (Option.some c)) →
    Option.some b = Option.some c

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Premises used: Function.Injective.eq_iff, WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
inst_1 : LE α
ha : AddLECancellable a
⊢ (↑a : WithTop α) + none ≤ (↑a : WithTop α) + none → LE.le.{u} (α := WithTop α) none none

Tactic:
simp [none_eq_top]

Premises used: WithTop.none_eq_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
inst_1 : LE α
ha : AddLECancellable a
c : α
⊢ (↑a : WithTop α) + none ≤ (↑a : WithTop α) + Option.some c → none ≤ Option.some c

Tactic:
simp [none_eq_top]

Premises used: WithTop.none_eq_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
inst_1 : LE α
ha : AddLECancellable a
b : α
⊢ (↑a : WithTop α) + Option.some b ≤ (↑a : WithTop α) + none → Option.some b ≤ none

Tactic:
simp [some_eq_coe, ← coe_add, none_eq_top]

Premises used: WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
inst_1 : LE α
ha : AddLECancellable a
b c : α
⊢ (↑a : WithTop α) + Option.some b ≤ (↑a : WithTop α) + Option.some c → Option.some b ≤ Option.some c

Tactic:
simpa [none_eq_top, some_eq_coe, ← coe_add] using fun a ↦ ha a

Premises used: WithTop.some_eq_coe, WithTop.none_eq_top, WithTop.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : IsRightCancelAdd α
hz : z ≠ ⊤
⊢ z ≠ ⊤

Tactic:
hz
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : IsRightCancelAdd α
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 : IsRightCancelAdd α
z : α
⊢ x + (↑z : WithTop α) = y + (↑z : WithTop α) ↔ x = y

Tactic:
(IsAddRightRegular.all _).withTop.eq_iff

Premises used: Function.Injective.eq_iff, IsAddRightRegular.all, IsAddRightRegular.withTop
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y : WithTop α
inst_1 : IsRightCancelAdd α
z : α
⊢ x + (↑z : WithTop α) = y + (↑z : WithTop α) ↔ x = y

Tactic:
exact (IsAddRightRegular.all _).withTop.eq_iff

Premises used: Function.Injective.eq_iff, IsAddRightRegular.all, IsAddRightRegular.withTop
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : IsRightCancelAdd α
hz : z ≠ ⊤
h : x + z = y + z
⊢ x = y

Tactic:
(WithTop.add_right_inj hz).1 h

Premises used: WithTop.add_right_inj, Iff.mp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : IsLeftCancelAdd α
hx : x ≠ ⊤
⊢ x ≠ ⊤

Tactic:
hx
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : IsLeftCancelAdd α
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 : IsLeftCancelAdd α
x : α
⊢ (↑x : WithTop α) + y = (↑x : WithTop α) + z ↔ y = z

Tactic:
(IsAddLeftRegular.all _).withTop.eq_iff

Premises used: Function.Injective.eq_iff, IsAddLeftRegular.all, IsAddLeftRegular.withTop
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y z : WithTop α
inst_1 : IsLeftCancelAdd α
x : α
⊢ (↑x : WithTop α) + y = (↑x : WithTop α) + z ↔ y = z

Tactic:
exact (IsAddLeftRegular.all _).withTop.eq_iff

Premises used: Function.Injective.eq_iff, IsAddLeftRegular.all, IsAddLeftRegular.withTop
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : IsLeftCancelAdd α
hx : x ≠ ⊤
h : x + y = x + z
⊢ y = z

Tactic:
(WithTop.add_left_inj hx).1 h

Premises used: Iff.mp, WithTop.add_left_inj
-- 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 : AddLeftMono α
x y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
coe :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) y z →
      (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)

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 : AddLeftMono α
y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z)
top₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a : WithTop α) z →
      (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) y z →
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((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 : AddLeftMono α
y z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) ⊤ z →
    (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)
coe₁ :
  ∀ (a : α),
    (fun (x1 x2 : WithTop α) ↦ x1 ≤ x2) (↑a : WithTop α) z →
      (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) y 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)

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

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

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

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

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 : AddLeftMono α
a_1 a_2 a_3 : α
⊢ a_2 ≤ a_3 → a_1 + a_2 ≤ a_1 + a_3

Tactic:
simpa using fun _ ↦ by gcongr