awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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
⊢ a_1 * x < a * x
have x0₁ : 0 < x
Tactic: norm_cast at x0
Cleared hypotheses: x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a < b
have inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0) (h : 0 * a < 0 * b), a < b
Tactic: rcases eq_or_ne x 0 with rfl | x0'
Cleared hypotheses: x, x0, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a < b
have inr : ∀ (x0' : x ≠ 0), a < b
Tactic: rcases eq_or_ne x 0 with rfl | x0'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a < b
have lift : x ≠ ⊥
Tactic: lift x to α
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 ≠ ⊥
⊢ a < b
have inr : ∀ (x : α) (x0 : 0 ≤ (↑x : WithBot α)) (h : (↑x : WithBot α) * a < (↑x : WithBot α) * b) (x0' : (↑x : WithBot α) ≠ 0),
  a < b
Tactic: lift x to α
Cleared hypotheses: x, x0, h, x0'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a < b
have inr : ∀ (h : (↑x : WithBot α) * a < (↑x : WithBot α) * ⊥), a < ⊥
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 < ⊥
⊢ a < b
have inr₁ : ∀ (a_1 : α) (h : (↑x : WithBot α) * a < (↑x : WithBot α) * (↑a_1 : WithBot α)), a < (↑a_1 : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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 α) * ⊥
⊢ a < ⊥
have h₁ : (↑x : WithBot α) * a < ⊥
Tactic: rw [mul_bot x0'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ a < (↑a_1 : WithBot α)
have inr : ∀ (h : (↑x : WithBot α) * ⊥ < (↑x : WithBot α) * (↑a_1 : WithBot α)), ⊥ < (↑a_1 : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ a < (↑a_1 : WithBot α)
have inr₁ : ∀ (a : α) (h : (↑x : WithBot α) * (↑a : WithBot α) < (↑x : WithBot α) * (↑a_1 : WithBot α)),
  (↑a : WithBot α) < (↑a_1 : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ (↑a_1 : WithBot α) < (↑a : WithBot α)
have inr : ∀ (h : x * a_1 < x * a), a_1 < a
Tactic: simp only [← coe_mul, coe_lt_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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
⊢ a_1 < a
have x0₁ : 0 ≤ x
Tactic: norm_cast at x0
Cleared hypotheses: x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a < b
have inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0) (h : a * 0 < b * 0), a < b
Tactic: rcases eq_or_ne x 0 with rfl | x0'
Cleared hypotheses: x, x0, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a < b
have inr : ∀ (x0' : x ≠ 0), a < b
Tactic: rcases eq_or_ne x 0 with rfl | x0'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a < b
have lift : x ≠ ⊥
Tactic: lift x to α
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 ≠ ⊥
⊢ a < b
have inr : ∀ (x : α) (x0 : 0 ≤ (↑x : WithBot α)) (h : a * (↑x : WithBot α) < b * (↑x : WithBot α)) (x0' : (↑x : WithBot α) ≠ 0),
  a < b
Tactic: lift x to α
Cleared hypotheses: x, x0, h, x0'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a < b
have inr : ∀ (h : a * (↑x : WithBot α) < ⊥ * (↑x : WithBot α)), a < ⊥
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 < ⊥
⊢ a < b
have inr₁ : ∀ (a_1 : α) (h : a * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)), a < (↑a_1 : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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 < ⊥
have h₁ : a * (↑x : WithBot α) < ⊥
Tactic: rw [bot_mul x0'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ a < (↑a_1 : WithBot α)
have inr : ∀ (h : ⊥ * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)), ⊥ < (↑a_1 : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ a < (↑a_1 : WithBot α)
have inr₁ : ∀ (a : α) (h : (↑a : WithBot α) * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)),
  (↑a : WithBot α) < (↑a_1 : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ (↑a_1 : WithBot α) < (↑a : WithBot α)
have inr : ∀ (h : a_1 * x < a * x), a_1 < a
Tactic: simp only [← coe_mul, coe_lt_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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
⊢ a_1 < a
have x0₁ : 0 ≤ x
Tactic: norm_cast at x0
Cleared hypotheses: x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a ≤ b
have lift : ∀ (x : α) (x0 : 0 < (↑x : WithBot α)) (h : (↑x : WithBot α) * a ≤ (↑x : WithBot α) * b), a ≤ b
Tactic: lift x to α using x0.ne_bot
Cleared hypotheses: x, x0, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a ≤ b
have bot : ∀ (h : (↑x : WithBot α) * ⊥ ≤ (↑x : WithBot α) * b), ⊥ ≤ b
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a ≤ b
have coe : ∀ (a : α) (h : (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * b), (↑a : WithBot α) ≤ b
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ (↑a : WithBot α) ≤ b
have coe : ∀ (h : (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * ⊥), (↑a : WithBot α) ≤ ⊥
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α) ≤ ⊥
⊢ (↑a : WithBot α) ≤ b
have coe₁ : ∀ (a_1 : α) (h : (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * (↑a_1 : WithBot α)),
  (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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 α) * ⊥
⊢ (↑a : WithBot α) ≤ ⊥
have h₁ : (↑(x * a) : WithBot α) ≤ ⊥
Tactic: rw [mul_bot x0.ne.symm, ← coe_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
have coe : ∀ (h : x * a ≤ x * a_1), a ≤ a_1
Tactic: simp only [← coe_mul, coe_le_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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
⊢ a ≤ a_1
have x0₁ : 0 < x
Tactic: norm_cast at x0
Cleared hypotheses: x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a ≤ b
have lift : ∀ (x : α) (x0 : 0 < (↑x : WithBot α)) (h : a * (↑x : WithBot α) ≤ b * (↑x : WithBot α)), a ≤ b
Tactic: lift x to α using x0.ne_bot
Cleared hypotheses: x, x0, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ a ≤ b
have bot : ∀ (h : ⊥ * (↑x : WithBot α) ≤ b * (↑x : WithBot α)), ⊥ ≤ b
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a ≤ b
have coe : ∀ (a : α) (h : (↑a : WithBot α) * (↑x : WithBot α) ≤ b * (↑x : WithBot α)), (↑a : WithBot α) ≤ b
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ (↑a : WithBot α) ≤ b
have coe : ∀ (h : (↑a : WithBot α) * (↑x : WithBot α) ≤ ⊥ * (↑x : WithBot α)), (↑a : WithBot α) ≤ ⊥
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α) ≤ ⊥
⊢ (↑a : WithBot α) ≤ b
have coe₁ : ∀ (a_1 : α) (h : (↑a : WithBot α) * (↑x : WithBot α) ≤ (↑a_1 : WithBot α) * (↑x : WithBot α)),
  (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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 : WithBot α) ≤ ⊥
have h₁ : (↑(a * x) : WithBot α) ≤ ⊥
Tactic: rw [bot_mul x0.ne.symm, ← coe_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
have coe : ∀ (h : a * x ≤ a_1 * x), a ≤ a_1
Tactic: simp only [← coe_mul, coe_le_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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
⊢ a ≤ a_1
have x0₁ : 0 < x
Tactic: norm_cast at x0
Cleared hypotheses: x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ round x = (⌊2 * x⌋ + 1) / 2
have rw : (if 2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = ⌊x⌋ + (⌊2 * fract 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ (if 2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
have pos : ∀ (h : 2 * fract x < 1), ⌊x⌋ + ⌊fract x⌋ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
⊢ (if 2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
have neg : ∀ (h : ¬2 * fract x < 1), ⌊x⌋ + ⌈fract x⌉ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
⊢ ⌊x⌋ + ⌊fract x⌋ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
have pos : ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌊x⌋ + ⌈fract x⌉ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
have neg : ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
⊢ ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2
have pos : 0 = HAdd.hAdd (α := ℤ) 0 1 / 2
Tactic: rw [Int.floor_eq_zero_iff.mpr, Int.floor_eq_zero_iff.mpr]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
⊢ ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2
have pos₁ : Membership.mem (γ := Set α) (Ico 0 1) (2 * fract x)
Tactic: rw [Int.floor_eq_zero_iff.mpr, Int.floor_eq_zero_iff.mpr]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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)
⊢ ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2
have pos₂ : Membership.mem (γ := Set α) (Ico 0 1) (fract x)
Tactic: rw [Int.floor_eq_zero_iff.mpr, Int.floor_eq_zero_iff.mpr]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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) (fract x)
have pos : fract x < 1
Tactic: suffices fract x < 1 by simpa
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x < 1
have pos : fract x ≤ 2 * fract x
Tactic: refine lt_of_le_of_lt ?_ h
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ≤ 2 * fract x
have pos : 0 ≤ fract x
Tactic: apply le_mul_of_one_le_left
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
⊢ fract x ≤ 2 * fract x
have pos₁ : LE.le.{u_2} (α := α) 1 2
Tactic: apply le_mul_of_one_le_left
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (hypothesis)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2
have H : ⌊2 * fract x⌋ = 1
Tactic: have H : ⌊2 * fract x⌋ = 1 := by simpa [floor_eq_iff, ← two_mul, fract_lt_one] using h
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2
have neg : 0 < fract x
Tactic: suffices 0 < fract x by simp [this, H, ceil_eq_iff, (fract_lt_one _).le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
⊢ 0 < fract x
have neg : ∀ (h : fract x ≤ 0), 2 * fract x < 1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
H : ⌊2 * fract x⌋ = 1
h : fract x ≤ 0
⊢ 2 * fract x < 1
have neg : HMul.hMul (α := α) 2 0 < 1
Tactic: grw [h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
hx : 2 * fract x ≠ 1
⊢ round x = ⌈2 * x⌉ / 2
have inl : ∀ (m : ℤ) (hm : (↑m : α) = 2 * x), round x = ⌈2 * x⌉ / 2
Tactic: rcases em (2 * x ∈ range Int.cast) with ⟨m, hm⟩ | hx'
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
hx : 2 * fract x ≠ 1
inl : ∀ (m : ℤ) (hm : (↑m : α) = 2 * x), round x = ⌈2 * x⌉ / 2
⊢ round x = ⌈2 * x⌉ / 2
have inr : ∀ (hx' : 2 * x ∉ range Int.cast), round x = ⌈2 * x⌉ / 2
Tactic: rcases em (2 * x ∈ range Int.cast) with ⟨m, hm⟩ | hx'
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : (↑m : α) = 2 * x
⊢ round x = ⌈2 * x⌉ / 2
have inl : round x = m / 2
Tactic: rw [← hm, ceil_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : (↑m : α) = 2 * x
⊢ round x = m / 2
have inl : ∀ (m : ℤ) (hm : (↑(m + m) : α) = 2 * x), round x = (m + m) / 2
Tactic: rcases m.even_or_odd with ⟨m, rfl⟩ | ⟨m, rfl⟩
Cleared hypotheses: m, hm