awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
inst_1 : CharZero α
⊢ CharZero.{u} (WithTop α)

Tactic:
{ cast_injective := Function.Injective.comp (f := Nat.cast (R := α))
      (fun _ _ => WithTop.coe_eq_coe.1) Nat.cast_injective }

Premises used: WithTop.coe_eq_coe, Function.Injective.comp, Iff.mp, CharZero.mk, Nat.cast_injective
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : LE α
inst_1 : Add α
inst_2 : ExistsAddOfLE α
a b : WithTop α
⊢ LE.le.{u} (α := WithTop α) ⊤ ⊤ → ∃ (c : WithTop α), ⊤ = ⊤ + c

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : LE α
inst_1 : Add α
inst_2 : ExistsAddOfLE α
a_1 b_1 : WithTop α
a b : α
h : (↑a : WithTop α) ≤ (↑b : WithTop α)
obtain :
  ∀ (c : α) (h : (↑a : WithTop α) ≤ (↑(a + c) : WithTop α)),
    ∃ (c_1 : WithTop α), (↑(a + c) : WithTop α) = (↑a : WithTop α) + c_1
⊢ ∃ (c : WithTop α), (↑b : WithTop α) = (↑a : WithTop α) + c

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le (WithTop.coe_le_coe.1 h)

Premises used: ExistsAddOfLE.exists_add_of_le, Iff.mp, WithTop.coe_le_coe, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : LE α
inst_1 : Add α
inst_2 : ExistsAddOfLE α
a_1 b : WithTop α
a c : α
h : (↑a : WithTop α) ≤ (↑(a + c) : WithTop α)
⊢ ∃ (c_1 : WithTop α), (↑(a + c) : WithTop α) = (↑a : WithTop α) + c_1

Tactic:
⟨c, rfl⟩

Premises used: WithTop.some, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : LE α
inst_1 : Add α
inst_2 : ExistsAddOfLE α
a_1 b : WithTop α
a c : α
h : (↑a : WithTop α) ≤ (↑(a + c) : WithTop α)
⊢ ∃ (c_1 : WithTop α), (↑(a + c) : WithTop α) = (↑a : WithTop α) + c_1

Tactic:
exact ⟨c, rfl⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
inst_1 : LT α
⊢ LT.lt.{u} (α := WithTop α) 1 ⊤

Tactic:
coe_lt_top _

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst : One M
inst_1 : One N
f : OneHom M N
rw : Eq.{u_2 + 1} (α := WithTop N) ((↑((f : (a : M) → N) 1) : WithTop N) : WithTop N) (1 : WithTop N)
rw₁ : Eq.{u_2 + 1} (α := WithTop N) (↑1 : WithTop N) 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := WithTop N) 1 1
⊢ Eq.{u_2 + 1} (α := WithTop N) (map.{u_1, u_2} (α := M) (⇑f : (a : M) → N) 1) 1

Tactic:
rw [WithTop.map_one, map_one, coe_one]

Premises used: WithTop.coe_one, map_one, WithTop.map_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
⊢ Eq.{u + 1} (α := WithBot α) (↑1 : WithBot α) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
a : α
⊢ (↑a : WithBot α) = 1 ↔ a = 1

Tactic:
coe_eq_coe

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
a : α
⊢ 1 = (↑a : WithBot α) ↔ a = 1

Tactic:
eq_comm.trans coe_eq_one

Premises used: WithBot.coe_eq_one, eq_comm, Iff.trans
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
⊢ Ne.{u + 1} (α := WithBot α) ⊥ 1

Tactic:
bot_ne_coe

Premises used: WithBot.bot_ne_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
⊢ Ne.{u + 1} (α := WithBot α) 1 ⊥

Tactic:
coe_ne_bot

Premises used: WithBot.coe_ne_bot
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
⊢ Eq.{u + 1} (α := α) (unbot 1 ⋯) 1

Tactic:
rfl

Premises used: WithBot.unbot, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
d : α
⊢ unbotD d 1 = 1

Tactic:
rfl

Premises used: WithBot.recBotCoe, WithBot.unbotD, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
a : α
inst_1 : LE α
⊢ 1 ≤ (↑a : WithBot α) ↔ 1 ≤ a

Tactic:
coe_le_coe

Premises used: WithBot.coe_le_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
a : α
inst_1 : LE α
⊢ (↑a : WithBot α) ≤ 1 ↔ a ≤ 1

Tactic:
coe_le_coe

Premises used: WithBot.coe_le_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
a : α
inst_1 : LT α
⊢ 1 < (↑a : WithBot α) ↔ 1 < a

Tactic:
coe_lt_coe

Premises used: WithBot.coe_lt_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
a : α
inst_1 : LT α
⊢ (↑a : WithBot α) < 1 ↔ a < 1

Tactic:
coe_lt_coe

Premises used: WithBot.coe_lt_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
inst_1 : LT α
⊢ LT.lt.{u} (α := WithBot α) ⊥ 1

Tactic:
bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : One α
β : Type u_1
f : α → β
⊢ map f 1 = (↑(f 1) : WithBot β)

Tactic:
rfl

Premises used: WithBot.some, WithBot.map, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
β : Type v
α : Type u_1
f : α → β
v : WithBot α
inst : One β
⊢ map f v = 1 ↔ ∃ (x : α), v = (↑x : WithBot α) ∧ f x = 1

Tactic:
map_eq_some_iff

Premises used: WithBot.map_eq_some_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
β : Type v
α : Type u_1
f : α → β
v : WithBot α
inst : One β
⊢ 1 = map f v ↔ ∃ (x : α), v = (↑x : WithBot α) ∧ f x = 1

Tactic:
some_eq_map_iff

Premises used: WithBot.some_eq_map_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : One α
a : α
inst_1 : Zero α
inst_2 : LE α
inst_3 : ZeroLEOneClass α
⊢ ZeroLEOneClass.{u} (WithBot α)

Tactic:
⟨coe_le_coe.2 zero_le_one⟩

Premises used: Iff.mpr, ZeroLEOneClass.mk, WithBot.coe_le_coe, zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a b : α
⊢ (↑(a + b) : WithBot α) = (↑a : WithBot α) + (↑b : WithBot α)

Tactic:
rfl

Premises used: WithBot.some, WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x : WithBot α
⊢ ⊥ + x = ⊥

Tactic:
rfl

Premises used: WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x : WithBot α
bot : HAdd.hAdd (α := WithBot α) ⊥ ⊥ = ⊥
coe : ∀ (a : α), (↑a : WithBot α) + ⊥ = ⊥
⊢ x + ⊥ = ⊥

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
⊢ HAdd.hAdd (α := WithBot α) ⊥ ⊥ = ⊥

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
⊢ (↑a : WithBot α) + ⊥ = ⊥

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y : WithBot α
bot : ⊥ + y = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ y = ⊥
coe : ∀ (a : α), (↑a : WithBot α) + y = ⊥ ↔ (↑a : WithBot α) = ⊥ ∨ y = ⊥
⊢ x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithBot α
bot : HAdd.hAdd (α := WithBot α) ⊥ ⊥ = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), ⊥ + (↑a : WithBot α) = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ (↑a : WithBot α) = ⊥
⊢ ⊥ + y = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ y = ⊥

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

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

Tactic:
simp [← coe_add]

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

Tactic:
simp [← coe_add]

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

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a a_1 : α
⊢ (↑a : WithBot α) + (↑a_1 : WithBot α) = ⊥ ↔ (↑a : WithBot α) = ⊥ ∨ (↑a_1 : WithBot α) = ⊥

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y : WithBot α
bot : ⊥ + y ≠ ⊥ ↔ Ne.{u + 1} (α := WithBot α) ⊥ ⊥ ∧ y ≠ ⊥
coe : ∀ (a : α), (↑a : WithBot α) + y ≠ ⊥ ↔ (↑a : WithBot α) ≠ ⊥ ∧ y ≠ ⊥
⊢ x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

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

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

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

Tactic:
simp [← coe_add]

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

Tactic:
simp [← coe_add]

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

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a a_1 : α
⊢ (↑a : WithBot α) + (↑a_1 : WithBot α) ≠ ⊥ ↔ (↑a : WithBot α) ≠ ⊥ ∧ (↑a_1 : WithBot α) ≠ ⊥

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y : WithBot α
inst_1 : LT α
simp_rw : x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Tactic:
simp_rw [WithBot.bot_lt_iff_ne_bot, add_ne_bot]

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

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a c : α
⊢ (↑a : WithBot α) + ⊥ = (↑c : WithBot α) ↔
    ∃ (a' : α), ∃ (b' : α), (↑a' : WithBot α) = (↑a : WithBot α) ∧ (↑b' : WithBot α) = ⊥ ∧ 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 : WithBot α) + (↑b : WithBot α) = (↑c : WithBot α) ↔
    ∃ (a' : α), ∃ (b' : α), (↑a' : WithBot α) = (↑a : WithBot α) ∧ (↑b' : WithBot α) = (↑b : WithBot α) ∧ a' + b' = c

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

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

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

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

Premises used: WithBot.some_eq_coe, WithBot.coe_add, WithBot.none_eq_bot
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ a + b = a + c → b = c

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

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

Premises used: WithBot.some_eq_coe, WithBot.coe_add, WithBot.none_eq_bot
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ b + a = c + a → b = c

Tactic:
simpa using @ha _ _
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
a : α
inst_1 : LE α
ha : AddLECancellable a
⊢ (↑a : WithBot α) + none ≤ (↑a : WithBot α) + none → LE.le.{u} (α := WithBot α) none none

Tactic:
simp [none_eq_bot]

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

Tactic:
simp [none_eq_bot]

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

Tactic:
simp [some_eq_coe, ← coe_add, none_eq_bot]

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

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

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

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

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithBot α
inst_1 : IsRightCancelAdd α
z : α
bot : ⊥ + (↑z : WithBot α) = ⊥ + (↑z : WithBot α) ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
bot₁ : ∀ (a : α), ⊥ + (↑z : WithBot α) = (↑a : WithBot α) + (↑z : WithBot α) ↔ ⊥ = (↑a : WithBot α)
⊢ ⊥ + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ ⊥ = y

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y : WithBot α
inst_1 : IsRightCancelAdd α
z a : α
coe : (↑a : WithBot α) + (↑z : WithBot α) = ⊥ + (↑z : WithBot α) ↔ (↑a : WithBot α) = ⊥
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithBot α) + (↑z : WithBot α) = (↑a_1 : WithBot α) + (↑z : WithBot α) ↔ (↑a : WithBot α) = (↑a_1 : WithBot α)
⊢ (↑a : WithBot α) + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ (↑a : WithBot α) = y

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : IsRightCancelAdd α
z : α
⊢ ⊥ + (↑z : WithBot α) = ⊥ + (↑z : WithBot α) ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : IsRightCancelAdd α
z a : α
⊢ ⊥ + (↑z : WithBot α) = (↑a : WithBot α) + (↑z : 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 : IsRightCancelAdd α
z a : α
⊢ (↑a : WithBot α) + (↑z : WithBot α) = ⊥ + (↑z : 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 : IsRightCancelAdd α
z a a_1 : α
⊢ (↑a : WithBot α) + (↑z : WithBot α) = (↑a_1 : WithBot α) + (↑z : WithBot α) ↔ (↑a : WithBot α) = (↑a_1 : WithBot α)

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithBot α
inst_1 : IsRightCancelAdd α
hz : z ≠ ⊥
h : x + z = y + z
⊢ x = y

Tactic:
(WithBot.add_right_inj hz).1 h

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

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

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : IsLeftCancelAdd α
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 : IsLeftCancelAdd α
x a : α
⊢ (↑x : WithBot α) + (↑a : WithBot α) = (↑x : 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 : IsLeftCancelAdd α
x a a_1 : α
⊢ (↑x : WithBot α) + (↑a : WithBot α) = (↑x : WithBot α) + (↑a_1 : WithBot α) ↔ (↑a : WithBot α) = (↑a_1 : WithBot α)

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithBot α
inst_1 : IsLeftCancelAdd α
hx : x ≠ ⊥
h : x + y = x + z
⊢ y = z

Tactic:
(WithBot.add_left_inj hx).1 h

Premises used: Iff.mp, WithBot.add_left_inj
-- 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 : LE α
inst_2 : AddLeftMono α
x y z : WithBot α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z)
coe :
  ∀ (a : α),
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
      (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a : WithBot α) y)
        ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a : WithBot α) z)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) x y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) x z)

Tactic:
cases x