awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 < ⊥
⊢ a < ⊥

Tactic:
absurd h bot_le.not_gt

Premises used: absurd, LE.le.not_gt, bot_le
-- 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 < ⊥
⊢ a < ⊥

Tactic:
exact absurd h bot_le.not_gt

Premises used: absurd, LE.le.not_gt, bot_le
-- 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
a_1 : α
h : (↑x : WithBot α) * a < (↑x : WithBot α) * (↑a_1 : WithBot α)
inr : ∀ (h : (↑x : WithBot α) * ⊥ < (↑x : WithBot α) * (↑a_1 : WithBot α)), ⊥ < (↑a_1 : WithBot α)
inr₁ :
  ∀ (a : α) (h : (↑x : WithBot α) * (↑a : WithBot α) < (↑x : WithBot α) * (↑a_1 : WithBot α)),
    (↑a : WithBot α) < (↑a_1 : WithBot α)
⊢ a < (↑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 : PosMulReflectLT α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑x : WithBot α) * ⊥ < (↑x : WithBot α) * (↑a : WithBot α)
⊢ ⊥ < (↑a : WithBot α)

Tactic:
WithBot.bot_lt_coe _

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

Tactic:
exact WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLT α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : (↑x : WithBot α) * (↑a_1 : WithBot α) < (↑x : WithBot α) * (↑a : WithBot α)
inr : ∀ (h : x * a_1 < x * a), a_1 < a
⊢ (↑a_1 : 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 : PosMulReflectLT α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : x * a_1 < x * 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 : PosMulReflectLT α
x : α
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : x * a_1 < x * a
x0 : 0 ≤ x
⊢ a_1 < a

Tactic:
lt_of_mul_lt_mul_left h x0

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

Tactic:
exact lt_of_mul_lt_mul_left h x0

Premises used: lt_of_mul_lt_mul_left
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a * x < b * x
inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0) (h : a * 0 < b * 0), 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 : MulPosReflectLT α
a b : WithBot α
x0 : LE.le.{u_1} (α := WithBot α) 0 0
h : a * 0 < b * 0
⊢ 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 : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a * x < b * x
x0' : x ≠ 0
lift : x ≠ ⊥
inr :
  ∀ (x : α) (x0 : 0 ≤ (↑x : WithBot α)) (h : a * (↑x : WithBot α) < b * (↑x : WithBot α)) (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 : MulPosReflectLT α
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 : MulPosReflectLT α
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 : MulPosReflectLT α
a b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
h : a * (↑x : WithBot α) < b * (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
inr : ∀ (h : a * (↑x : WithBot α) < ⊥ * (↑x : WithBot α)), a < ⊥
inr₁ : ∀ (a_1 : α) (h : a * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : 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 : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
h : a * (↑x : WithBot α) < ⊥ * (↑x : WithBot α)
⊢ a * (↑x : WithBot α) < ⊥

Tactic:
rw [bot_mul x0'] at h

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

Tactic:
absurd h bot_le.not_gt

Premises used: absurd, LE.le.not_gt, bot_le
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
h : a * (↑x : WithBot α) < ⊥
⊢ a < ⊥

Tactic:
exact absurd h bot_le.not_gt

Premises used: absurd, LE.le.not_gt, bot_le
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a_1 : α
h : a * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
inr : ∀ (h : ⊥ * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)), ⊥ < (↑a_1 : WithBot α)
inr₁ :
  ∀ (a : α) (h : (↑a : WithBot α) * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)),
    (↑a : WithBot α) < (↑a_1 : WithBot α)
⊢ a < (↑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 : MulPosReflectLT α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : ⊥ * (↑x : WithBot α) < (↑a : WithBot α) * (↑x : WithBot α)
⊢ ⊥ < (↑a : WithBot α)

Tactic:
WithBot.bot_lt_coe _

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

Tactic:
exact WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosReflectLT α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : (↑a_1 : WithBot α) * (↑x : WithBot α) < (↑a : WithBot α) * (↑x : WithBot α)
inr : ∀ (h : a_1 * x < a * x), a_1 < a
⊢ (↑a_1 : 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 : MulPosReflectLT α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a_1 * x < a * x
⊢ 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 : MulPosReflectLT α
x : α
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a_1 * x < a * x
x0 : 0 ≤ x
⊢ a_1 < a

Tactic:
lt_of_mul_lt_mul_right h x0

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

Tactic:
exact lt_of_mul_lt_mul_right h x0

Premises used: lt_of_mul_lt_mul_right
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : x * a ≤ x * 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 : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : x * a ≤ x * b
lift : ∀ (x : α) (x0 : 0 < (↑x : WithBot α)) (h : (↑x : WithBot α) * a ≤ (↑x : WithBot α) * b), a ≤ b
⊢ a ≤ 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 : PosMulReflectLE α
a b : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
h : (↑x : WithBot α) * a ≤ (↑x : WithBot α) * b
bot : ∀ (h : (↑x : WithBot α) * ⊥ ≤ (↑x : WithBot α) * b), ⊥ ≤ b
coe : ∀ (a : α) (h : (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * b), (↑a : WithBot α) ≤ b
⊢ a ≤ b

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

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLE α
b : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
h : (↑x : WithBot α) * ⊥ ≤ (↑x : WithBot α) * b
⊢ ⊥ ≤ b

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulReflectLE α
b : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * b
coe : ∀ (h : (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * ⊥), (↑a : WithBot α) ≤ ⊥
coe₁ :
  ∀ (a_1 : α) (h : (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * (↑a_1 : WithBot α)),
    (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ (↑a : 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 : PosMulReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * ⊥
⊢ (↑(x * a) : WithBot α) ≤ ⊥

Tactic:
rw [mul_bot x0.ne.symm, ← coe_mul] at h

Premises used: Ne.symm, 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 : PosMulReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : (↑(x * a) : WithBot α) ≤ ⊥
⊢ (↑a : 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 : PosMulReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : (↑(x * a) : WithBot α) ≤ ⊥
⊢ (↑a : 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 : PosMulReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * (↑a_1 : WithBot α)
coe : ∀ (h : x * a ≤ x * a_1), a ≤ a_1
⊢ (↑a : 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 : PosMulReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : x * a ≤ x * 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 : PosMulReflectLE α
x a a_1 : α
h : x * a ≤ x * a_1
x0 : 0 < x
⊢ a ≤ a_1

Tactic:
le_of_mul_le_mul_left h x0

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

Tactic:
exact le_of_mul_le_mul_left h x0

Premises used: le_of_mul_le_mul_left
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a * x ≤ b * x
⊢ 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 : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a * x ≤ b * x
lift : ∀ (x : α) (x0 : 0 < (↑x : WithBot α)) (h : a * (↑x : WithBot α) ≤ b * (↑x : WithBot α)), a ≤ b
⊢ a ≤ 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 : MulPosReflectLE α
a b : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
h : a * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
bot : ∀ (h : ⊥ * (↑x : WithBot α) ≤ b * (↑x : WithBot α)), ⊥ ≤ b
coe : ∀ (a : α) (h : (↑a : WithBot α) * (↑x : WithBot α) ≤ b * (↑x : WithBot α)), (↑a : WithBot α) ≤ b
⊢ a ≤ b

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

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosReflectLE α
b : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
h : ⊥ * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
⊢ ⊥ ≤ b

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosReflectLE α
b : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : (↑a : WithBot α) * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
coe : ∀ (h : (↑a : WithBot α) * (↑x : WithBot α) ≤ ⊥ * (↑x : WithBot α)), (↑a : WithBot α) ≤ ⊥
coe₁ :
  ∀ (a_1 : α) (h : (↑a : WithBot α) * (↑x : WithBot α) ≤ (↑a_1 : WithBot α) * (↑x : WithBot α)),
    (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ (↑a : 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 : MulPosReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : (↑a : WithBot α) * (↑x : WithBot α) ≤ ⊥ * (↑x : WithBot α)
⊢ (↑(a * x) : WithBot α) ≤ ⊥

Tactic:
rw [bot_mul x0.ne.symm, ← coe_mul] at h

Premises used: Ne.symm, 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 : MulPosReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : (↑(a * x) : WithBot α) ≤ ⊥
⊢ (↑a : 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 : MulPosReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : (↑(a * x) : WithBot α) ≤ ⊥
⊢ (↑a : 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 : MulPosReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : (↑a : WithBot α) * (↑x : WithBot α) ≤ (↑a_1 : WithBot α) * (↑x : WithBot α)
coe : ∀ (h : a * x ≤ a_1 * x), a ≤ a_1
⊢ (↑a : 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 : MulPosReflectLE α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : a * x ≤ a_1 * x
⊢ 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 : MulPosReflectLE α
x a a_1 : α
h : a * x ≤ a_1 * x
x0 : 0 < x
⊢ a ≤ a_1

Tactic:
le_of_mul_le_mul_right h x0

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

Tactic:
exact le_of_mul_le_mul_right h x0

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
rw : (if 2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
⊢ round x = (⌊2 * x⌋ + 1) / 2

Tactic:
rw [← floor_add_fract x, round, fract_intCast_add, fract_fract, floor_intCast_add, mul_add,
    ← Int.cast_ofNat, ← Int.cast_mul, floor_intCast_add, ceil_intCast_add, add_assoc,
    Int.mul_add_ediv_left _ _ two_ne_zero, Int.cast_ofNat]

Premises used: Int.fract_intCast_add, Int.mul_add_ediv_left, Int.floor_intCast_add, add_assoc, Int.floor_add_fract, Int.cast_ofNat, two_ne_zero, Int.cast_mul, Int.fract_fract, round, mul_add, Int.ceil_intCast_add
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
pos : ∀ (h : 2 * fract x < 1), ⌊x⌋ + ⌊fract x⌋ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
neg : ∀ (h : ¬2 * fract x < 1), ⌊x⌋ + ⌈fract x⌉ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
⊢ (if 2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
pos : ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2
⊢ ⌊x⌋ + ⌊fract x⌋ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2

Tactic:
congr 1
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : ¬2 * fract x < 1
neg : ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2
⊢ ⌊x⌋ + ⌈fract x⌉ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2

Tactic:
congr 1
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
pos : 0 = HAdd.hAdd (α := ℤ) 0 1 / 2
pos₁ : Membership.mem (γ := Set α) (Ico 0 1) (2 * fract x)
pos₂ : Membership.mem (γ := Set α) (Ico 0 1) (fract x)
⊢ ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
rw [Int.floor_eq_zero_iff.mpr, Int.floor_eq_zero_iff.mpr]

Premises used: Iff.mpr, Int.floor_eq_zero_iff
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 = HAdd.hAdd (α := ℤ) 0 1 / 2

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
⊢ Membership.mem (γ := Set α) (Ico 0 1) (2 * fract x)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
this : fract x < 1
⊢ Membership.mem (γ := Set α) (Ico 0 1) (fract x)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
pos : fract x < 1
⊢ Membership.mem (γ := Set α) (Ico 0 1) (fract x)

Tactic:
suffices fract x < 1 by simpa
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x < 1

Tactic:
lt_of_le_of_lt ?_ h

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
pos : fract x ≤ 2 * fract x
⊢ fract x < 1

Tactic:
refine lt_of_le_of_lt ?_ h

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
pos : 0 ≤ fract x
pos₁ : LE.le.{u_2} (α := α) 1 2
⊢ fract x ≤ 2 * fract x

Tactic:
apply le_mul_of_one_le_left

Premises used: le_mul_of_one_le_left
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 ≤ fract x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
⊢ LE.le.{u_2} (α := α) 1 2

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌊2 * fract x⌋ = 1

Tactic:
simpa [floor_eq_iff, ← two_mul, fract_lt_one] using h

Premises used: two_mul, Int.floor_eq_iff, Int.fract_lt_one
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌊2 * fract x⌋ = 1

Tactic:
have H : ⌊2 * fract x⌋ = 1 := by simpa [floor_eq_iff, ← two_mul, fract_lt_one] using h
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : ¬2 * fract x < 1
H : ⌊2 * fract x⌋ = 1
this : 0 < fract x
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
simp [this, H, ceil_eq_iff, (fract_lt_one _).le]

Premises used: Int.ceil_eq_iff, LT.lt.le, Int.fract_lt_one