awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z a : α
coe : (↑a : WithTop α) < ⊤ → (↑a : WithTop α) + (↑z : WithTop α) < ⊤ + (↑z : WithTop α)
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithTop α) < (↑a_1 : WithTop α) → (↑a : WithTop α) + (↑z : WithTop α) < (↑a_1 : WithTop α) + (↑z : WithTop α)
⊢ (↑a : WithTop α) < y → (↑a : WithTop α) + (↑z : WithTop α) < y + (↑z : WithTop α)

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z : α
⊢ LT.lt.{u} (α := WithTop α) ⊤ ⊤ → ⊤ + (↑z : WithTop α) < ⊤ + (↑z : 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 : AddRightStrictMono α
z a : α
⊢ ⊤ < (↑a : WithTop α) → ⊤ + (↑z : WithTop α) < (↑a : WithTop α) + (↑z : 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 : AddRightStrictMono α
z a : α
⊢ (↑a : WithTop α) < ⊤ → (↑a : WithTop α) + (↑z : WithTop α) < ⊤ + (↑z : 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 : AddRightStrictMono α
z a a_1 : α
coe : a < a_1 → a + z < a_1 + z
⊢ (↑a : WithTop α) < (↑a_1 : WithTop α) → (↑a : WithTop α) + (↑z : WithTop α) < (↑a_1 : WithTop α) + (↑z : 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 : AddRightStrictMono α
z a a_1 : α
h : a < a_1
⊢ a + z < a_1 + z

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

Tactic:
simpa using fun _ ↦ by gcongr
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
w x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftStrictMono α
inst_3 : AddRightStrictMono α
xz : x < z
yw : y < w
apply : x + w ≤ z + w
⊢ x + y < z + w

Tactic:
apply (WithTop.add_lt_add_left xz.ne_top yw).trans_le

Premises used: LT.lt.ne_top, LT.lt.trans_le, WithTop.add_lt_add_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
w x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftStrictMono α
inst_3 : AddRightStrictMono α
xz : x < z
yw : y < w
top : ∀ (yw : y < ⊤), x + ⊤ ≤ z + ⊤
coe : ∀ (a : α) (yw : y < (↑a : WithTop α)), x + (↑a : WithTop α) ≤ z + (↑a : WithTop α)
⊢ x + w ≤ z + w

Tactic:
cases w
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftStrictMono α
inst_3 : AddRightStrictMono α
xz : x < z
yw : y < ⊤
⊢ x + ⊤ ≤ z + ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftStrictMono α
inst_3 : AddRightStrictMono α
xz : x < z
a : α
yw : y < (↑a : WithTop α)
⊢ x + (↑a : WithTop α) ≤ z + (↑a : WithTop α)

Tactic:
(WithTop.add_lt_add_right coe_ne_top xz).le

Premises used: WithTop.add_lt_add_right, LT.lt.le, WithTop.coe_ne_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftStrictMono α
inst_3 : AddRightStrictMono α
xz : x < z
a : α
yw : y < (↑a : WithTop α)
⊢ x + (↑a : WithTop α) ≤ z + (↑a : WithTop α)

Tactic:
exact (WithTop.add_lt_add_right coe_ne_top xz).le

Premises used: WithTop.add_lt_add_right, LT.lt.le, WithTop.coe_ne_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LE α
inst_2 : AddLeftMono α
inst_3 : AddLeftReflectLE α
hx : x ≠ ⊤
h : y ≤ z
⊢ x + y ≤ x + z

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
hz : z ≠ ⊤
h : x ≤ y
⊢ x + z ≤ y + z

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
inst_3 : AddLeftReflectLT α
hx : x ≠ ⊤
⊢ x + y < x + z ↔ y < z

Tactic:
⟨lt_of_add_lt_add_left, WithTop.add_lt_add_left hx⟩

Premises used: Iff.intro, WithTop.add_lt_add_left, lt_of_add_lt_add_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
inst_3 : AddRightReflectLT α
hz : z ≠ ⊤
⊢ x + z < y + z ↔ x < y

Tactic:
⟨lt_of_add_lt_add_right, WithTop.add_lt_add_right hz⟩

Premises used: WithTop.add_lt_add_right, Iff.intro, lt_of_add_lt_add_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
w x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftStrictMono α
inst_3 : AddRightMono α
hw : w ≠ ⊤
hwy : w ≤ y
hxz : x < z
⊢ w + z ≤ y + z

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
w x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftMono α
inst_3 : AddRightStrictMono α
hx : x ≠ ⊤
hwy : w < y
hxz : x ≤ z
⊢ y + x ≤ y + z

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
hx : x ≠ ⊤
⊢ AddLECancellable x

Tactic:
fun _b _c ↦ WithTop.le_of_add_le_add_left hx

Premises used: WithTop.le_of_add_le_add_left, AddLECancellable
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftReflectLE α
hx : x < ⊤
⊢ AddLECancellable x

Tactic:
addLECancellable_of_ne_top hx.ne

Premises used: WithTop.addLECancellable_of_ne_top, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
a : α
⊢ AddLECancellable (↑a : WithTop α)

Tactic:
addLECancellable_of_ne_top coe_ne_top

Premises used: WithTop.coe_ne_top, WithTop.addLECancellable_of_ne_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : AddLeftReflectLE α
h : AddLECancellable.{u} (α := WithTop α) ⊤
⊢ HAdd.hAdd (α := WithTop α) ⊤ ⊤ ≤ ⊤ + (↑(Classical.arbitrary α) : WithTop α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : AddLeftReflectLE α
h : AddLECancellable.{u} (α := WithTop α) ⊤
⊢ False

Tactic:
exact (coe_lt_top <| Classical.arbitrary _).not_ge <| h <| by simp

Premises used: LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a b : WithTop α
top :
  map (⇑f : (a : α) → β) (⊤ + b) =
    HAdd.hAdd (α := WithTop β) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤) (map (⇑f : (a : α) → β) b)
coe :
  ∀ (a : α),
    map (⇑f : (a : α) → β) ((↑a : WithTop α) + b) =
      HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map (⇑f : (a : α) → β) b)
⊢ map (⇑f : (a : α) → β) (a + b) = HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) a) (map (⇑f : (a : α) → β) b)

Tactic:
induction a
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
b : WithTop α
⊢ map (⇑f : (a : α) → β) (⊤ + b) =
    HAdd.hAdd (α := WithTop β) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤) (map (⇑f : (a : α) → β) b)

Tactic:
(top_add _).symm

Premises used: WithTop.map, WithTop.top_add, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
b : WithTop α
⊢ map (⇑f : (a : α) → β) (⊤ + b) =
    HAdd.hAdd (α := WithTop β) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤) (map (⇑f : (a : α) → β) b)

Tactic:
exact (top_add _).symm

Premises used: WithTop.top_add, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
b : WithTop α
a : α
coe :
  map (⇑f : (a : α) → β) ((↑a : WithTop α) + ⊤) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤)
coe₁ :
  ∀ (a_1 : α),
    map (⇑f : (a : α) → β) ((↑a : WithTop α) + (↑a_1 : WithTop α)) =
      HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map (⇑f : (a : α) → β) (↑a_1 : WithTop α))
⊢ map (⇑f : (a : α) → β) ((↑a : WithTop α) + b) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map (⇑f : (a : α) → β) b)

Tactic:
induction b
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a : α
⊢ map (⇑f : (a : α) → β) ((↑a : WithTop α) + ⊤) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤)

Tactic:
(add_top _).symm

Premises used: WithTop.map, WithTop.add_top, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a : α
⊢ map (⇑f : (a : α) → β) ((↑a : WithTop α) + ⊤) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤)

Tactic:
exact (add_top _).symm

Premises used: WithTop.add_top, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a a_1 : α
coe :
  Eq.{v + 1} (α := WithTop β) (map (⇑f : (a : α) → β) (↑(a + a_1) : WithTop α) : WithTop β)
    ((↑((f : (a : α) → β) (a + a_1)) : WithTop β) : WithTop β)
⊢ map (⇑f : (a : α) → β) ((↑a : WithTop α) + (↑a_1 : WithTop α)) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map (⇑f : (a : α) → β) (↑a_1 : WithTop α))

Tactic:
rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]

Premises used: map_add, WithTop.coe_add, WithTop.map_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a a_1 : α
⊢ Eq.{v + 1} (α := WithTop β) (map (⇑f : (a : α) → β) (↑(a + a_1) : WithTop α) : WithTop β)
    ((↑((f : (a : α) → β) (a + a_1)) : WithTop β) : WithTop β)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
a : WithTop α
top :
  Eq.{u + 1} (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (0 : WithTop α)
coe :
  ∀ (a : α),
    Eq (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (0 : WithTop α)
⊢ Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (0 : WithTop α)

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
⊢ Eq.{u + 1} (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (0 : WithTop α)

Tactic:
simp [zero_nsmul]

Premises used: zero_nsmul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
a : α
⊢ Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (0 : WithTop α)

Tactic:
simp [zero_nsmul]

Premises used: zero_nsmul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
n : ℕ
a : WithTop α
top :
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, n with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)
coe :
  ∀ (a : α),
    (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n + 1 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤) =
      HAdd.hAdd (α := WithTop α)
        (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n with
          | Option.some a, n => (↑(n • a) : WithTop α)
          | none, 0 => 0
          | none, _n.succ => ⊤ :
          WithTop α)
        (↑a : WithTop α)
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      a

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
n : ℕ
top :
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)
top₁ :
  ∀ (n : ℕ),
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 + 1 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤) =
      HAdd.hAdd (α := WithTop α) (β := WithTop α)
        (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 with
          | Option.some a, n => (↑(n • a) : WithTop α)
          | none, 0 => 0
          | none, _n.succ => ⊤ :
          WithTop α)
        (⊤ : WithTop α)
⊢ (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, n with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)

Tactic:
cases n
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
n : ℕ
a : α
coe :
  (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (↑a : WithTop α)
coe₁ :
  ∀ (n : ℕ),
    (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n + 1 + 1 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤) =
      HAdd.hAdd (α := WithTop α)
        (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n + 1 with
          | Option.some a, n => (↑(n • a) : WithTop α)
          | none, 0 => 0
          | none, _n.succ => ⊤ :
          WithTop α)
        (↑a : WithTop α)
⊢ (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (↑a : WithTop α)

Tactic:
cases n
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
⊢ (match (motive := WithTop α → ℕ → WithTop α) ⊤, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)

Tactic:
simp [succ_nsmul, coe_add]

Premises used: WithTop.coe_add, succ_nsmul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
n : ℕ
⊢ (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)

Tactic:
simp [succ_nsmul, coe_add]

Premises used: WithTop.coe_add, succ_nsmul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
a : α
⊢ (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (↑a : WithTop α)

Tactic:
simp [succ_nsmul, coe_add]

Premises used: WithTop.coe_add, succ_nsmul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoid α
a : α
n : ℕ
⊢ (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n + 1 + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n + 1 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (↑a : WithTop α)

Tactic:
simp [succ_nsmul, coe_add]

Premises used: WithTop.coe_add, succ_nsmul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoid α
a : α
n : ℕ
⊢ (↑(n • a) : WithTop α) = n • (↑a : WithTop α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoid α
⊢ Eq.{u + 1} (α := (a : α) → WithTop α) (⇑addHom : (a : α) → WithTop α) some

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
⊢ Eq.{u + 1} (α := WithTop α) (↑0) 0

Tactic:
simp [NatCast.natCast]

Premises used: NatCast.natCast
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
n : ℕ
⊢ ↑(n + 1) = HAdd.hAdd (α := WithTop α) (↑n) 1

Tactic:
simp [NatCast.natCast]

Premises used: NatCast.natCast
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := WithTop α) (↑(↑n : α) : WithTop α) (↑n : WithTop α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Ne.{u + 1} (α := WithTop α) ⊤ (↑n : WithTop α)

Tactic:
top_ne_coe

Premises used: WithTop.top_ne_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Ne.{u + 1} (α := WithTop α) (↑n : WithTop α) ⊤

Tactic:
coe_ne_top

Premises used: WithTop.coe_ne_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
inst_1 : LT α
n : ℕ
⊢ LT.lt.{u} (α := WithTop α) (↑n : WithTop α) ⊤

Tactic:
coe_lt_top _

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := WithTop α) (↑(OfNat.ofNat n) : WithTop α) (OfNat.ofNat n)

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
m : α
⊢ (↑m : WithTop α) = OfNat.ofNat n ↔ m = OfNat.ofNat n

Tactic:
coe_eq_coe

Premises used: WithTop.coe_eq_coe, WithTop.some
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
m : α
⊢ OfNat.ofNat n = (↑m : WithTop α) ↔ OfNat.ofNat n = m

Tactic:
coe_eq_coe

Premises used: WithTop.coe_eq_coe, WithTop.some
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Ne.{u + 1} (α := WithTop α) (OfNat.ofNat n) ⊤

Tactic:
natCast_ne_top n

Premises used: WithTop.natCast_ne_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Ne.{u + 1} (α := WithTop α) ⊤ (OfNat.ofNat n)

Tactic:
top_ne_natCast n

Premises used: WithTop.top_ne_natCast
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : α → β
n : ℕ
inst_1 : n.AtLeastTwo
⊢ map f (OfNat.ofNat n) = (↑(f (OfNat.ofNat n)) : WithTop β)

Tactic:
map_coe f n

Premises used: Nat.cast, WithTop.some, WithTop.map_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : α → β
n : ℕ
⊢ map f (↑n : WithTop α) = (↑(f (↑n : α)) : WithTop β)

Tactic:
map_coe f n

Premises used: Nat.cast, WithTop.map_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : β → α
n : ℕ
inst_1 : n.AtLeastTwo
a : WithTop β
⊢ map f a = OfNat.ofNat n ↔ ∃ (x : β), a = (↑x : WithTop β) ∧ f x = (↑n : α)

Tactic:
map_eq_some_iff

Premises used: WithTop.some, WithTop.map_eq_some_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : β → α
n : ℕ
inst_1 : n.AtLeastTwo
a : WithTop β
⊢ OfNat.ofNat n = map f a ↔ ∃ (x : β), a = (↑x : WithTop β) ∧ f x = (↑n : α)

Tactic:
some_eq_map_iff

Premises used: WithTop.some, WithTop.some_eq_map_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : β → α
n : ℕ
a : WithTop β
⊢ map f a = (↑n : WithTop α) ↔ ∃ (x : β), a = (↑x : WithTop β) ∧ f x = (↑n : α)

Tactic:
map_eq_some_iff

Premises used: WithTop.map_eq_some_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : β → α
n : ℕ
a : WithTop β
⊢ (↑n : WithTop α) = map f a ↔ ∃ (x : β), a = (↑x : WithTop β) ∧ f x = (↑n : α)

Tactic:
some_eq_map_iff

Premises used: WithTop.some_eq_map_iff