awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithBot α
hb : ¬b = 0
a : α
ha : ¬(↑a : WithBot α) = 0
neg :
  ∀ (hb : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0), unbotD 0 ((↑a : WithBot α) * ⊥) = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
neg₁ :
  ∀ (a_1 : α) (hb : ¬(↑a_1 : WithBot α) = 0),
    unbotD 0 ((↑a : WithBot α) * (↑a_1 : WithBot α)) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
⊢ unbotD 0 ((↑a : WithBot α) * b) = unbotD 0 (↑a : WithBot α) * unbotD 0 b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithBot α) = 0
hb : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0
neg : unbotD 0 ⊥ = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
neg₁ : 0 = unbotD 0 (↑a : WithBot α) * 0
neg₂ neg₃ : Eq.{u_1 + 1} (α := α) 0 0
⊢ unbotD 0 ((↑a : WithBot α) * ⊥) = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥

Tactic:
rw [mul_bot ha, unbotD_bot, mul_zero]

Premises used: WithBot.unbotD_bot, MulZeroClass.mul_zero, WithBot.mul_bot
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithBot α) = 0
a_1 : α
hb : ¬(↑a_1 : WithBot α) = 0
neg : unbotD 0 (↑(a * a_1) : WithBot α) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
neg₁ : a * a_1 = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
neg₂ : a * a_1 = a * unbotD 0 (↑a_1 : WithBot α)
neg₃ neg₄ : a * a_1 = a * a_1
⊢ unbotD 0 ((↑a : WithBot α) * (↑a_1 : WithBot α)) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)

Tactic:
rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]

Premises used: WithBot.unbotD_coe, WithBot.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
ha : a ≠ ⊥
hb : b ≠ ⊥
⊢ a * b ≠ ⊥

Tactic:
WithTop.mul_ne_top (α := αᵒᵈ) ha hb

Premises used: WithBot, WithTop.mul_ne_top, OrderDual
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : LT α
a b : WithBot α
ha : ⊥ < a
hb : ⊥ < b
⊢ ⊥ < a * b

Tactic:
WithTop.mul_lt_top (α := αᵒᵈ) ha hb

Premises used: WithTop.mul_lt_top, OrderDual
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
inst_2 : NoZeroDivisors α
⊢ NoZeroDivisors.{u_1} (WithBot α)

Tactic:
inferInstanceAs <| NoZeroDivisors (WithTop α)

Premises used: _private.0.WithBot.instNoZeroDivisors._proof_1
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
a : α
n : ℕ
⊢ (↑(a ^ n) : WithBot α) = (↑a : WithBot α) ^ n

Tactic:
rfl

Premises used: WithBot.some, WithTop.some, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0), 0 * a ≤ 0 * b
inr : ∀ (x0' : x ≠ 0), x * a ≤ x * b
⊢ x * a ≤ x * b

Tactic:
rcases eq_or_ne x 0 with rfl | x0'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
a b : WithBot α
h : a ≤ b
x0 : LE.le.{u_1} (α := WithBot α) 0 0
⊢ 0 * a ≤ 0 * b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
lift : x ≠ ⊥
inr : ∀ (x : α) (x0 : 0 ≤ (↑x : WithBot α)) (x0' : (↑x : WithBot α) ≠ 0), (↑x : WithBot α) * a ≤ (↑x : WithBot α) * b
⊢ x * a ≤ x * b

Tactic:
lift x to α
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
a b : WithBot α
h : a ≤ b
x0 : LE.le.{u_1} (α := WithBot α) 0 ⊥
x0' : Ne.{u_1 + 1} (α := WithBot α) ⊥ 0
⊢ False

Tactic:
(WithBot.bot_lt_coe (0 : α)).not_ge x0

Premises used: WithBot.bot_lt_coe, LT.lt.not_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
a b : WithBot α
h : a ≤ b
x0 : LE.le.{u_1} (α := WithBot α) 0 ⊥
x0' : Ne.{u_1 + 1} (α := WithBot α) ⊥ 0
⊢ False

Tactic:
exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

Premises used: WithBot.bot_lt_coe, LT.lt.not_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
inr : ∀ (h : ⊥ ≤ b), (↑x : WithBot α) * ⊥ ≤ (↑x : WithBot α) * b
inr₁ : ∀ (a : α) (h : (↑a : WithBot α) ≤ b), (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * b
⊢ (↑x : WithBot α) * a ≤ (↑x : WithBot α) * b

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
h : ⊥ ≤ b
inr : ⊥ ≤ (↑x : WithBot α) * b
⊢ (↑x : WithBot α) * ⊥ ≤ (↑x : WithBot α) * b

Tactic:
simp_rw [mul_bot x0', bot_le]

Premises used: WithBot.mul_bot, bot_le
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ b
inr : ∀ (h : (↑a : WithBot α) ≤ ⊥), (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * ⊥
inr₁ :
  ∀ (a_1 : α) (h : (↑a : WithBot α) ≤ (↑a_1 : WithBot α)),
    (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * (↑a_1 : WithBot α)
⊢ (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ ⊥
⊢ (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * ⊥

Tactic:
absurd h (bot_lt_coe _).not_ge

Premises used: absurd, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ ⊥
⊢ (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * ⊥

Tactic:
exact absurd h (bot_lt_coe _).not_ge

Premises used: absurd, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
inr : ∀ (h : a ≤ a_1), x * a ≤ x * a_1
⊢ (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * (↑a_1 : WithBot α)

Tactic:
simp only [← coe_mul, coe_le_coe] at *

Premises used: WithBot.coe_le_coe, WithBot.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a ≤ a_1
⊢ 0 ≤ x

Tactic:
norm_cast at x0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : α
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a ≤ a_1
x0 : 0 ≤ x
⊢ x * a ≤ x * a_1

Tactic:
mul_le_mul_of_nonneg_left h x0

Premises used: mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : α
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a ≤ a_1
x0 : 0 ≤ x
⊢ x * a ≤ x * a_1

Tactic:
exact mul_le_mul_of_nonneg_left h x0

Premises used: mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0), a * 0 ≤ b * 0
inr : ∀ (x0' : x ≠ 0), a * x ≤ b * x
⊢ a * x ≤ b * x

Tactic:
rcases eq_or_ne x 0 with rfl | x0'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
a b : WithBot α
h : a ≤ b
x0 : LE.le.{u_1} (α := WithBot α) 0 0
⊢ a * 0 ≤ b * 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
lift : x ≠ ⊥
inr : ∀ (x : α) (x0 : 0 ≤ (↑x : WithBot α)) (x0' : (↑x : WithBot α) ≠ 0), a * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
⊢ a * x ≤ b * x

Tactic:
lift x to α
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
a b : WithBot α
h : a ≤ b
x0 : LE.le.{u_1} (α := WithBot α) 0 ⊥
x0' : Ne.{u_1 + 1} (α := WithBot α) ⊥ 0
⊢ False

Tactic:
(WithBot.bot_lt_coe (0 : α)).not_ge x0

Premises used: WithBot.bot_lt_coe, LT.lt.not_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
a b : WithBot α
h : a ≤ b
x0 : LE.le.{u_1} (α := WithBot α) 0 ⊥
x0' : Ne.{u_1 + 1} (α := WithBot α) ⊥ 0
⊢ False

Tactic:
exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

Premises used: WithBot.bot_lt_coe, LT.lt.not_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
inr : ∀ (h : ⊥ ≤ b), ⊥ * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
inr₁ : ∀ (a : α) (h : (↑a : WithBot α) ≤ b), (↑a : WithBot α) * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
⊢ a * (↑x : WithBot α) ≤ b * (↑x : WithBot α)

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
h : ⊥ ≤ b
inr : ⊥ ≤ b * (↑x : WithBot α)
⊢ ⊥ * (↑x : WithBot α) ≤ b * (↑x : WithBot α)

Tactic:
simp_rw [bot_mul x0', bot_le]

Premises used: WithBot.bot_mul, bot_le
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ b
inr : ∀ (h : (↑a : WithBot α) ≤ ⊥), (↑a : WithBot α) * (↑x : WithBot α) ≤ ⊥ * (↑x : WithBot α)
inr₁ :
  ∀ (a_1 : α) (h : (↑a : WithBot α) ≤ (↑a_1 : WithBot α)),
    (↑a : WithBot α) * (↑x : WithBot α) ≤ (↑a_1 : WithBot α) * (↑x : WithBot α)
⊢ (↑a : WithBot α) * (↑x : WithBot α) ≤ b * (↑x : WithBot α)

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ ⊥
⊢ (↑a : WithBot α) * (↑x : WithBot α) ≤ ⊥ * (↑x : WithBot α)

Tactic:
absurd h (bot_lt_coe _).not_ge

Premises used: absurd, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ ⊥
⊢ (↑a : WithBot α) * (↑x : WithBot α) ≤ ⊥ * (↑x : WithBot α)

Tactic:
exact absurd h (bot_lt_coe _).not_ge

Premises used: absurd, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
inr : ∀ (h : a ≤ a_1), a * x ≤ a_1 * x
⊢ (↑a : WithBot α) * (↑x : WithBot α) ≤ (↑a_1 : WithBot α) * (↑x : WithBot α)

Tactic:
simp only [← coe_mul, coe_le_coe] at *

Premises used: WithBot.coe_le_coe, WithBot.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a ≤ a_1
⊢ 0 ≤ x

Tactic:
norm_cast at x0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : α
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a ≤ a_1
x0 : 0 ≤ x
⊢ a * x ≤ a_1 * x

Tactic:
mul_le_mul_of_nonneg_right h x0

Premises used: mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : α
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a ≤ a_1
x0 : 0 ≤ x
⊢ a * x ≤ a_1 * x

Tactic:
exact mul_le_mul_of_nonneg_right h x0

Premises used: mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a < b
⊢ x ≠ ⊥

Tactic:
x0.ne_bot

Premises used: LT.lt.ne_bot
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a < b
lift : ∀ (x : α) (x0 : 0 < (↑x : WithBot α)), (↑x : WithBot α) * a < (↑x : WithBot α) * b
⊢ x * a < x * b

Tactic:
lift x to α using x0.ne_bot

Premises used: LT.lt.ne_bot
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a b : WithBot α
h : a < b
x : α
x0 : 0 < (↑x : WithBot α)
bot : ∀ (h : a < ⊥), (↑x : WithBot α) * a < (↑x : WithBot α) * ⊥
coe : ∀ (a_1 : α) (h : a < (↑a_1 : WithBot α)), (↑x : WithBot α) * a < (↑x : WithBot α) * (↑a_1 : WithBot α)
⊢ (↑x : WithBot α) * a < (↑x : WithBot α) * b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
h : a < ⊥
⊢ (↑x : WithBot α) * a < (↑x : WithBot α) * ⊥

Tactic:
absurd h not_lt_bot

Premises used: not_lt_bot, absurd
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
h : a < ⊥
⊢ (↑x : WithBot α) * a < (↑x : WithBot α) * ⊥

Tactic:
exact absurd h not_lt_bot

Premises used: not_lt_bot, absurd
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
a_1 : α
h : a < (↑a_1 : WithBot α)
coe : ∀ (h : ⊥ < (↑a_1 : WithBot α)), (↑x : WithBot α) * ⊥ < (↑x : WithBot α) * (↑a_1 : WithBot α)
coe₁ :
  ∀ (a : α) (h : (↑a : WithBot α) < (↑a_1 : WithBot α)),
    (↑x : WithBot α) * (↑a : WithBot α) < (↑x : WithBot α) * (↑a_1 : WithBot α)
⊢ (↑x : WithBot α) * a < (↑x : WithBot α) * (↑a_1 : WithBot α)

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : ⊥ < (↑a : WithBot α)
coe : ⊥ < (↑x : WithBot α) * (↑a : WithBot α)
coe₁ : ⊥ < (↑(x * a) : WithBot α)
⊢ (↑x : WithBot α) * ⊥ < (↑x : WithBot α) * (↑a : WithBot α)

Tactic:
simp_rw [mul_bot x0.ne.symm, ← coe_mul, bot_lt_coe]

Premises used: Ne.symm, WithBot.bot_lt_coe, WithBot.mul_bot, LT.lt.ne, WithBot.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : (↑a_1 : WithBot α) < (↑a : WithBot α)
coe : ∀ (h : a_1 < a), x * a_1 < x * a
⊢ (↑x : WithBot α) * (↑a_1 : WithBot α) < (↑x : WithBot α) * (↑a : WithBot α)

Tactic:
simp only [← coe_mul, coe_lt_coe] at *

Premises used: WithBot.coe_lt_coe, WithBot.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : a_1 < a
⊢ 0 < x

Tactic:
norm_cast at x0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x a a_1 : α
h : a_1 < a
x0 : 0 < x
⊢ x * a_1 < x * a

Tactic:
mul_lt_mul_of_pos_left h x0

Premises used: mul_lt_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x a a_1 : α
h : a_1 < a
x0 : 0 < x
⊢ x * a_1 < x * a

Tactic:
exact mul_lt_mul_of_pos_left h x0

Premises used: mul_lt_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a < b
⊢ x ≠ ⊥

Tactic:
x0.ne_bot

Premises used: LT.lt.ne_bot
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a < b
lift : ∀ (x : α) (x0 : 0 < (↑x : WithBot α)), a * (↑x : WithBot α) < b * (↑x : WithBot α)
⊢ a * x < b * x

Tactic:
lift x to α using x0.ne_bot

Premises used: LT.lt.ne_bot
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a b : WithBot α
h : a < b
x : α
x0 : 0 < (↑x : WithBot α)
bot : ∀ (h : a < ⊥), a * (↑x : WithBot α) < ⊥ * (↑x : WithBot α)
coe : ∀ (a_1 : α) (h : a < (↑a_1 : WithBot α)), a * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
⊢ a * (↑x : WithBot α) < b * (↑x : WithBot α)

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
h : a < ⊥
⊢ a * (↑x : WithBot α) < ⊥ * (↑x : WithBot α)

Tactic:
absurd h not_lt_bot

Premises used: not_lt_bot, absurd
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
h : a < ⊥
⊢ a * (↑x : WithBot α) < ⊥ * (↑x : WithBot α)

Tactic:
exact absurd h not_lt_bot

Premises used: not_lt_bot, absurd
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
a_1 : α
h : a < (↑a_1 : WithBot α)
coe : ∀ (h : ⊥ < (↑a_1 : WithBot α)), ⊥ * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
coe₁ :
  ∀ (a : α) (h : (↑a : WithBot α) < (↑a_1 : WithBot α)),
    (↑a : WithBot α) * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
⊢ a * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : ⊥ < (↑a : WithBot α)
coe : ⊥ < (↑a : WithBot α) * (↑x : WithBot α)
coe₁ : ⊥ < (↑(a * x) : WithBot α)
⊢ ⊥ * (↑x : WithBot α) < (↑a : WithBot α) * (↑x : WithBot α)

Tactic:
simp_rw [bot_mul x0.ne.symm, ← coe_mul, bot_lt_coe]

Premises used: Ne.symm, WithBot.bot_lt_coe, WithBot.bot_mul, LT.lt.ne, WithBot.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : (↑a_1 : WithBot α) < (↑a : WithBot α)
coe : ∀ (h : a_1 < a), a_1 * x < a * x
⊢ (↑a_1 : WithBot α) * (↑x : WithBot α) < (↑a : WithBot α) * (↑x : WithBot α)

Tactic:
simp only [← coe_mul, coe_lt_coe] at *

Premises used: WithBot.coe_lt_coe, WithBot.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : a_1 < a
⊢ 0 < x

Tactic:
norm_cast at x0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x a a_1 : α
h : a_1 < a
x0 coe : 0 < x
⊢ a_1 * x < a * x

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : x * a < x * b
inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0) (h : 0 * a < 0 * b), a < b
inr : ∀ (x0' : x ≠ 0), a < b
⊢ a < b

Tactic:
rcases eq_or_ne x 0 with rfl | x0'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLT α
a b : WithBot α
x0 : LE.le.{u_1} (α := WithBot α) 0 0
h : 0 * a < 0 * b
⊢ a < b

Tactic:
simp at h
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : x * a < x * b
x0' : x ≠ 0
lift : x ≠ ⊥
inr :
  ∀ (x : α) (x0 : 0 ≤ (↑x : WithBot α)) (h : (↑x : WithBot α) * a < (↑x : WithBot α) * b) (x0' : (↑x : WithBot α) ≠ 0),
    a < b
⊢ a < b

Tactic:
lift x to α
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLT α
a b : WithBot α
x0 : LE.le.{u_1} (α := WithBot α) 0 ⊥
h : ⊥ * a < ⊥ * b
x0' : Ne.{u_1 + 1} (α := WithBot α) ⊥ 0
⊢ False

Tactic:
(WithBot.bot_lt_coe (0 : α)).not_ge x0

Premises used: WithBot.bot_lt_coe, LT.lt.not_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLT α
a b : WithBot α
x0 : LE.le.{u_1} (α := WithBot α) 0 ⊥
h : ⊥ * a < ⊥ * b
x0' : Ne.{u_1 + 1} (α := WithBot α) ⊥ 0
⊢ False

Tactic:
exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

Premises used: WithBot.bot_lt_coe, LT.lt.not_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLT α
a b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
h : (↑x : WithBot α) * a < (↑x : WithBot α) * b
x0' : (↑x : WithBot α) ≠ 0
inr : ∀ (h : (↑x : WithBot α) * a < (↑x : WithBot α) * ⊥), a < ⊥
inr₁ : ∀ (a_1 : α) (h : (↑x : WithBot α) * a < (↑x : WithBot α) * (↑a_1 : WithBot α)), a < (↑a_1 : WithBot α)
⊢ a < b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
h : (↑x : WithBot α) * a < (↑x : WithBot α) * ⊥
⊢ (↑x : WithBot α) * a < ⊥

Tactic:
rw [mul_bot x0'] at h

Premises used: WithBot.mul_bot