awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a a_1 : α
coe : x + a ≤ x + a_1 → 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 : LE α
inst_2 : AddRightReflectLE α
hz : z ≠ ⊥
⊢ z ≠ ⊥

Tactic:
hz
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithBot α
inst_1 : LE α
inst_2 : AddRightReflectLE α
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 : LE α
inst_2 : AddRightReflectLE α
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 : LE α
inst_2 : AddRightReflectLE α
z : α
bot : ⊥ + (↑z : WithBot α) ≤ ⊥ + (↑z : WithBot α) → LE.le.{u} (α := 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 : LE α
inst_2 : AddRightReflectLE α
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 : LE α
inst_2 : AddRightReflectLE α
z : α
⊢ ⊥ + (↑z : WithBot α) ≤ ⊥ + (↑z : 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 : AddRightReflectLE α
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 : LE α
inst_2 : AddRightReflectLE α
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 : LE α
inst_2 : AddRightReflectLE α
z a a_1 : α
coe : a + z ≤ a_1 + 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 : LT α
inst_2 : AddLeftStrictMono α
hx : x ≠ ⊥
⊢ x ≠ ⊥

Tactic:
hx
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithBot α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
hx : x ≠ ⊥
lift : ∀ (x : α), y < z → (↑x : WithBot α) + y < (↑x : WithBot α) + z
⊢ y < z → x + y < x + z

Tactic:
lift x to α using hx
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
y z : WithBot α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x : α
bot : ⊥ < z → (↑x : WithBot α) + ⊥ < (↑x : WithBot α) + z
coe : ∀ (a : α), (↑a : WithBot α) < z → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : WithBot α) + z
⊢ y < z → (↑x : WithBot α) + y < (↑x : WithBot α) + z

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

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

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

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a : α
⊢ ⊥ < (↑a : WithBot α) → (↑x : 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 : LT α
inst_2 : AddLeftStrictMono α
x a : α
⊢ (↑a : WithBot α) < ⊥ → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : WithBot α) + ⊥

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a a_1 : α
coe : a < a_1 → x + a < x + a_1
⊢ (↑a : WithBot α) < (↑a_1 : WithBot α) → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : 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 : LT α
inst_2 : AddRightStrictMono α
hz : z ≠ ⊥
⊢ z ≠ ⊥

Tactic:
hz
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y z : WithBot α
inst_1 : LT α
inst_2 : AddRightStrictMono α
hz : z ≠ ⊥
lift : ∀ (z : α), x < y → x + (↑z : WithBot α) < y + (↑z : WithBot α)
⊢ x < y → x + z < y + z

Tactic:
lift z to α using hz
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
x y : WithBot α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z : α
bot : ⊥ < y → ⊥ + (↑z : WithBot α) < y + (↑z : WithBot α)
coe : ∀ (a : α), (↑a : WithBot α) < y → (↑a : WithBot α) + (↑z : WithBot α) < y + (↑z : WithBot α)
⊢ x < y → x + (↑z : WithBot α) < y + (↑z : WithBot α)

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

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

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} (α := WithBot α) ⊥ ⊥ → ⊥ + (↑z : WithBot α) < ⊥ + (↑z : WithBot α)

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z a : α
⊢ ⊥ < (↑a : WithBot α) → ⊥ + (↑z : WithBot α) < (↑a : WithBot α) + (↑z : WithBot α)

Tactic:
simp [← coe_add]

Premises used: WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z a : α
⊢ (↑a : WithBot α) < ⊥ → (↑a : WithBot α) + (↑z : WithBot α) < ⊥ + (↑z : WithBot α)

Tactic:
simp [← coe_add]

Premises used: WithBot.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 : WithBot α) < (↑a_1 : WithBot α) → (↑a : WithBot α) + (↑z : WithBot α) < (↑a_1 : WithBot α) + (↑z : 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 : 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 : WithBot α
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 : WithBot α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
inst_3 : AddLeftReflectLT α
hx : x ≠ ⊥
⊢ x + y < x + z ↔ y < z

Tactic:
⟨lt_of_add_lt_add_left, WithBot.add_lt_add_left hx⟩

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

Tactic:
⟨lt_of_add_lt_add_right, WithBot.add_lt_add_right hz⟩

Premises used: Iff.intro, WithBot.add_lt_add_right, lt_of_add_lt_add_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
w x y z : WithBot α
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 : WithBot α
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 : WithBot α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
hx : x ≠ ⊥
⊢ AddLECancellable x

Tactic:
fun _b _c ↦ WithBot.le_of_add_le_add_left hx

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

Tactic:
addLECancellable_of_ne_bot hx.ne

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

Tactic:
addLECancellable_of_ne_bot coe_ne_bot

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

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} (α := WithBot α) ⊥
⊢ False

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

Premises used: LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
bot : ⊥ + c ≤ b + c ↔ ⊥ ≤ b
coe : ∀ (a : WithTop α), (↑a : WithBot (WithTop α)) + c ≤ b + c ↔ (↑a : WithBot (WithTop α)) ≤ b
⊢ a + c ≤ b + c ↔ a ≤ b

Tactic:
induction a
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
bot : ⊥ + c ≤ ⊥ + c ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
bot₁ : ∀ (a : WithTop α), ⊥ + c ≤ (↑a : WithBot (WithTop α)) + c ↔ ⊥ ≤ (↑a : WithBot (WithTop α))
⊢ ⊥ + c ≤ b + c ↔ ⊥ ≤ b

Tactic:
induction b
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a : WithTop α
coe : (↑a : WithBot (WithTop α)) + c ≤ ⊥ + c ↔ (↑a : WithBot (WithTop α)) ≤ ⊥
coe₁ :
  ∀ (a_1 : WithTop α),
    (↑a : WithBot (WithTop α)) + c ≤ (↑a_1 : WithBot (WithTop α)) + c ↔
      (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
⊢ (↑a : WithBot (WithTop α)) + c ≤ b + c ↔ (↑a : WithBot (WithTop α)) ≤ b

Tactic:
induction b
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
bot :
  ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
    HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔
      LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
bot₁ :
  ∀ (a : WithTop α) (hc : (↑a : WithBot (WithTop α)) ≠ ⊥) (hc' : (↑a : WithBot (WithTop α)) ≠ ⊤),
    ⊥ + (↑a : WithBot (WithTop α)) ≤ ⊥ + (↑a : WithBot (WithTop α)) ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
⊢ ⊥ + c ≤ ⊥ + c ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥

Tactic:
induction c
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a : WithTop α
bot :
  ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
    HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ (↑a : WithBot (WithTop α)) + ⊥ ↔ ⊥ ≤ (↑a : WithBot (WithTop α))
bot₁ :
  ∀ (a_1 : WithTop α) (hc : (↑a_1 : WithBot (WithTop α)) ≠ ⊥) (hc' : (↑a_1 : WithBot (WithTop α)) ≠ ⊤),
    ⊥ + (↑a_1 : WithBot (WithTop α)) ≤ (↑a : WithBot (WithTop α)) + (↑a_1 : WithBot (WithTop α)) ↔
      ⊥ ≤ (↑a : WithBot (WithTop α))
⊢ ⊥ + c ≤ (↑a : WithBot (WithTop α)) + c ↔ ⊥ ≤ (↑a : WithBot (WithTop α))

Tactic:
induction c
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a : WithTop α
coe :
  ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
    (↑a : WithBot (WithTop α)) + ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔ (↑a : WithBot (WithTop α)) ≤ ⊥
coe₁ :
  ∀ (a_1 : WithTop α) (hc : (↑a_1 : WithBot (WithTop α)) ≠ ⊥) (hc' : (↑a_1 : WithBot (WithTop α)) ≠ ⊤),
    (↑a : WithBot (WithTop α)) + (↑a_1 : WithBot (WithTop α)) ≤ ⊥ + (↑a_1 : WithBot (WithTop α)) ↔
      (↑a : WithBot (WithTop α)) ≤ ⊥
⊢ (↑a : WithBot (WithTop α)) + c ≤ ⊥ + c ↔ (↑a : WithBot (WithTop α)) ≤ ⊥

Tactic:
induction c
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a a_1 : WithTop α
coe :
  ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
    (↑a : WithBot (WithTop α)) + ⊥ ≤ (↑a_1 : WithBot (WithTop α)) + ⊥ ↔
      (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
coe₁ :
  ∀ (a_2 : WithTop α) (hc : (↑a_2 : WithBot (WithTop α)) ≠ ⊥) (hc' : (↑a_2 : WithBot (WithTop α)) ≠ ⊤),
    (↑a : WithBot (WithTop α)) + (↑a_2 : WithBot (WithTop α)) ≤
        (↑a_1 : WithBot (WithTop α)) + (↑a_2 : WithBot (WithTop α)) ↔
      (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
⊢ (↑a : WithBot (WithTop α)) + c ≤ (↑a_1 : WithBot (WithTop α)) + c ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))

Tactic:
induction c
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥
hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤
bot bot₁ bot₂ bot₃ :
  HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔
    LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
⊢ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔
    LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a : WithTop α
hc : (↑a : WithBot (WithTop α)) ≠ ⊥
hc' : (↑a : WithBot (WithTop α)) ≠ ⊤
bot bot₁ bot₂ bot₃ :
  ∀ (hc' : ¬a = ⊤),
    ⊥ + (↑a : WithBot (WithTop α)) ≤ ⊥ + (↑a : WithBot (WithTop α)) ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
⊢ ⊥ + (↑a : WithBot (WithTop α)) ≤ ⊥ + (↑a : WithBot (WithTop α)) ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a : WithTop α
hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥
hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤
bot bot₁ bot₂ bot₃ :
  HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ (↑a : WithBot (WithTop α)) + ⊥ ↔ ⊥ ≤ (↑a : WithBot (WithTop α))
⊢ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ (↑a : WithBot (WithTop α)) + ⊥ ↔ ⊥ ≤ (↑a : WithBot (WithTop α))

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 : WithTop α
hc : (↑a_1 : WithBot (WithTop α)) ≠ ⊥
hc' : (↑a_1 : WithBot (WithTop α)) ≠ ⊤
⊢ ¬a_1 = ⊤

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a : WithTop α
hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥
hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤
coe coe₁ coe₂ coe₃ :
  (↑a : WithBot (WithTop α)) + ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔ (↑a : WithBot (WithTop α)) ≤ ⊥
⊢ (↑a : WithBot (WithTop α)) + ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔ (↑a : WithBot (WithTop α)) ≤ ⊥

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 : WithTop α
hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥
hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤
coe coe₁ coe₂ coe₃ : (↑a : WithBot (WithTop α)) + ⊥ ≤ (↑a_1 : WithBot (WithTop α)) + ⊥ ↔ a ≤ a_1
⊢ (↑a : WithBot (WithTop α)) + ⊥ ≤ (↑a_1 : WithBot (WithTop α)) + ⊥ ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 a_2 : WithTop α
hc : (↑a_2 : WithBot (WithTop α)) ≠ ⊥
hc' : (↑a_2 : WithBot (WithTop α)) ≠ ⊤
coe : ∀ (hc' : ¬a_2 = ⊤), a + a_2 ≤ a_1 + a_2 ↔ a ≤ a_1
⊢ (↑a : WithBot (WithTop α)) + (↑a_2 : WithBot (WithTop α)) ≤
      (↑a_1 : WithBot (WithTop α)) + (↑a_2 : WithBot (WithTop α)) ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 : WithTop α
hc : ¬(↑a_1 : WithBot (WithTop α)) = ⊥
hc' : ¬a_1 = ⊤
⊢ ⊥ + (↑a_1 : WithBot (WithTop α)) ≤ (↑(a + a_1) : WithBot (WithTop α)) ↔ ⊥ ≤ (↑a : WithBot (WithTop α))

Tactic:
aesop (add simp WithTop.add_le_add_iff_right)

Premises used: WithTop.add_le_add_iff_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 : WithTop α
hc : ¬(↑a_1 : WithBot (WithTop α)) = ⊥
hc' : ¬a_1 = ⊤
⊢ (↑(a + a_1) : WithBot (WithTop α)) ≤ ⊥ + (↑a_1 : WithBot (WithTop α)) ↔ (↑a : WithBot (WithTop α)) ≤ ⊥

Tactic:
aesop (add simp WithTop.add_le_add_iff_right)

Premises used: WithTop.add_le_add_iff_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 a_2 : WithTop α
hc : ¬(↑a_2 : WithBot (WithTop α)) = ⊥
hc' : ¬a_2 = ⊤
⊢ a + a_2 ≤ a_1 + a_2 ↔ a ≤ a_1

Tactic:
aesop (add simp WithTop.add_le_add_iff_right)

Premises used: WithTop.add_le_add_iff_right
-- 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 : WithBot α
bot :
  map (⇑f : (a : α) → β) (⊥ + b) =
    HAdd.hAdd (α := WithBot β) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊥) (map (⇑f : (a : α) → β) b)
coe :
  ∀ (a : α),
    map (⇑f : (a : α) → β) ((↑a : WithBot α) + b) =
      HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map (⇑f : (a : α) → β) b)
⊢ map (⇑f : (a : α) → β) (a + b) = HAdd.hAdd (α := WithBot β) (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 : WithBot α
⊢ map (⇑f : (a : α) → β) (⊥ + b) =
    HAdd.hAdd (α := WithBot β) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊥) (map (⇑f : (a : α) → β) b)

Tactic:
(bot_add _).symm

Premises used: WithBot.bot_add, Eq.symm, WithBot.map
-- 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 : WithBot α
⊢ map (⇑f : (a : α) → β) (⊥ + b) =
    HAdd.hAdd (α := WithBot β) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊥) (map (⇑f : (a : α) → β) b)

Tactic:
exact (bot_add _).symm

Premises used: WithBot.bot_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 : WithBot α
a : α
coe :
  map (⇑f : (a : α) → β) ((↑a : WithBot α) + ⊥) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊥)
coe₁ :
  ∀ (a_1 : α),
    map (⇑f : (a : α) → β) ((↑a : WithBot α) + (↑a_1 : WithBot α)) =
      HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map (⇑f : (a : α) → β) (↑a_1 : WithBot α))
⊢ map (⇑f : (a : α) → β) ((↑a : WithBot α) + b) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (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 : WithBot α) + ⊥) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊥)

Tactic:
(add_bot _).symm

Premises used: WithBot.add_bot, Eq.symm, WithBot.map