awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inl : ∀ (m : ℤ) (hm : (↑(m + m) : α) = 2 * x), round x = (m + m) / 2
⊢ round x = m / 2
have inl₁ : ∀ (m : ℤ) (hm : (↑(2 * m + 1) : α) = 2 * x), round x = (2 * m + 1) / 2
Tactic: rcases m.even_or_odd with ⟨m, rfl⟩ | ⟨m, rfl⟩
Cleared hypotheses: m, hm
-- 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 + m) : α) = 2 * x
⊢ round x = (m + m) / 2
have inl : ∀ (hx : HMul.hMul (α := α) 2 (fract (↑m : α)) ≠ 1) (hm : (↑(m + m) : α) = HMul.hMul (α := α) 2 (↑m : α)),
  round.{u_2} (α := α) (↑m : α) = (m + m) / 2
Tactic: obtain rfl : m = x := mul_left_cancel₀ two_ne_zero <| by simp [← hm, ← two_mul]
Cleared hypotheses: x, hx, hm
-- 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 α
m : ℤ
hx : HMul.hMul (α := α) 2 (fract (↑m : α)) ≠ 1
hm : (↑(m + m) : α) = HMul.hMul (α := α) 2 (↑m : α)
⊢ round.{u_2} (α := α) (↑m : α) = (m + m) / 2
have inl : m = (m + m) / 2
Tactic: rw [round_intCast, ← two_mul, Int.mul_ediv_cancel_left _ two_ne_zero]
-- 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 α
m : ℤ
hx : HMul.hMul (α := α) 2 (fract (↑m : α)) ≠ 1
hm : (↑(m + m) : α) = HMul.hMul (α := α) 2 (↑m : α)
inl : m = (m + m) / 2
⊢ round.{u_2} (α := α) (↑m : α) = (m + m) / 2
have inl₁ : m = 2 * m / 2
Tactic: rw [round_intCast, ← two_mul, Int.mul_ediv_cancel_left _ two_ne_zero]
-- 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 α
m : ℤ
hx : HMul.hMul (α := α) 2 (fract (↑m : α)) ≠ 1
hm : (↑(m + m) : α) = HMul.hMul (α := α) 2 (↑m : α)
inl : m = (m + m) / 2
inl₁ : m = 2 * m / 2
⊢ round.{u_2} (α := α) (↑m : α) = (m + m) / 2
have inl₂ : m = m
Tactic: rw [round_intCast, ← two_mul, Int.mul_ediv_cancel_left _ two_ne_zero]
-- 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 : (↑(2 * m + 1) : α) = 2 * x
⊢ round x = (2 * m + 1) / 2
have inl : 2 * fract x = 1
Tactic: refine absurd ?_ 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
hx' : 2 * x ∉ range Int.cast
⊢ round x = ⌈2 * x⌉ / 2
have inr : (⌊2 * x⌋ + 1) / 2 = ⌈2 * x⌉ / 2
Tactic: rw [round_eq_div, (ceil_eq_floor_add_one_iff_notMem _).mpr 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
hx' : 2 * x ∉ range Int.cast
inr : (⌊2 * x⌋ + 1) / 2 = ⌈2 * x⌉ / 2
⊢ round x = ⌈2 * x⌉ / 2
have inr₁ : (⌊2 * x⌋ + 1) / 2 = (⌊2 * x⌋ + 1) / 2
Tactic: rw [round_eq_div, (ceil_eq_floor_add_one_iff_notMem _).mpr 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 : α
y : ℤ
⊢ round (x + (↑y : α)) = round x + y
have rw : (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = round x + y
Tactic: rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
    ← apply_ite₂, ite_self]
-- 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 : α
y : ℤ
rw : (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = round x + y
⊢ round (x + (↑y : α)) = round x + y
have rw₁ : (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
Tactic: rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
    ← apply_ite₂, ite_self]
-- 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 : α
y : ℤ
rw : (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = round x + y
rw₁ :
  (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
⊢ round (x + (↑y : α)) = round x + y
have rw₂ : (if 2 * fract x < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
Tactic: rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
    ← apply_ite₂, ite_self]
-- 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 : α
y : ℤ
rw : (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = round x + y
rw₁ :
  (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₂ : (if 2 * fract x < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
⊢ round (x + (↑y : α)) = round x + y
have rw₃ : (if 2 * fract x < 1 then ⌊x⌋ + y else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
Tactic: rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
    ← apply_ite₂, ite_self]
-- 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 : α
y : ℤ
rw : (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = round x + y
rw₁ :
  (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₂ : (if 2 * fract x < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₃ : (if 2 * fract x < 1 then ⌊x⌋ + y else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
⊢ round (x + (↑y : α)) = round x + y
have rw₄ : (if 2 * fract x < 1 then ⌊x⌋ + y else ⌈x⌉ + y) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
Tactic: rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
    ← apply_ite₂, ite_self]
-- 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 : α
y : ℤ
rw : (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = round x + y
rw₁ :
  (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₂ : (if 2 * fract x < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₃ : (if 2 * fract x < 1 then ⌊x⌋ + y else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₄ : (if 2 * fract x < 1 then ⌊x⌋ + y else ⌈x⌉ + y) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
⊢ round (x + (↑y : α)) = round x + y
have rw₅ : ((if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + if 2 * fract x < 1 then y else y) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
Tactic: rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
    ← apply_ite₂, ite_self]
-- 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 : α
y : ℤ
rw : (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = round x + y
rw₁ :
  (if 2 * fract (x + (↑y : α)) < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₂ : (if 2 * fract x < 1 then ⌊x + (↑y : α)⌋ else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₃ : (if 2 * fract x < 1 then ⌊x⌋ + y else ⌈x + (↑y : α)⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₄ : (if 2 * fract x < 1 then ⌊x⌋ + y else ⌈x⌉ + y) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
rw₅ :
  ((if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + if 2 * fract x < 1 then y else y) =
    (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
⊢ round (x + (↑y : α)) = round x + y
have rw₆ : (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
Tactic: rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
    ← apply_ite₂, ite_self]
-- 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 α
a : α
⊢ round (a + 1) = round a + 1
have rw : round (a + 1) = round (a + (↑1 : α))
Tactic: rw [← round_add_intCast a 1, cast_one]
-- 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 α
a : α
rw : round (a + 1) = round (a + (↑1 : α))
⊢ round (a + 1) = round a + 1
have rw₁ : round (a + 1) = round (a + 1)
Tactic: rw [← round_add_intCast a 1, cast_one]
-- 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 : α
y : ℤ
⊢ round (x - (↑y : α)) = round x - y
have rw : round (x + -(↑y : α)) = round x - y
Tactic: rw [sub_eq_add_neg]
-- 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 : α
y : ℤ
⊢ round (x + -(↑y : α)) = round x - y
have norm_cast : round (x + (↑(-y) : α)) = round x - y
Tactic: norm_cast
-- 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 : α
y : ℤ
⊢ round (x + (↑(-y) : α)) = round x - y
have rw : round x + -y = round x - y
Tactic: rw [round_add_intCast, sub_eq_add_neg]
-- 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 : α
y : ℤ
rw : round x + -y = round x - y
⊢ round (x + (↑(-y) : α)) = round x - y
have rw₁ : round x + -y = round x + -y
Tactic: rw [round_add_intCast, sub_eq_add_neg]
-- 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 α
a : α
⊢ round (a - 1) = round a - 1
have rw : round (a - 1) = round (a - (↑1 : α))
Tactic: rw [← round_sub_intCast a 1, cast_one]
-- 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 α
a : α
rw : round (a - 1) = round (a - (↑1 : α))
⊢ round (a - 1) = round a - 1
have rw₁ : round (a - 1) = round (a - 1)
Tactic: rw [← round_sub_intCast a 1, cast_one]
-- 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 : α
y : ℤ
⊢ round ((↑y : α) + x) = y + round x
have rw : round (x + (↑y : α)) = y + round x
Tactic: rw [add_comm, round_add_intCast, add_comm]
-- 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 : α
y : ℤ
rw : round (x + (↑y : α)) = y + round x
⊢ round ((↑y : α) + x) = y + round x
have rw₁ : round x + y = y + round x
Tactic: rw [add_comm, round_add_intCast, add_comm]
-- 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 : α
y : ℤ
rw : round (x + (↑y : α)) = y + round x
rw₁ : round x + y = y + round x
⊢ round ((↑y : α) + x) = y + round x
have rw₂ : y + round x = y + round x
Tactic: rw [add_comm, round_add_intCast, add_comm]
-- 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 : α
y : ℕ
⊢ round ((↑y : α) + x) = (↑y : ℤ) + round x
have rw : round (x + (↑y : α)) = (↑y : ℤ) + round x
Tactic: rw [add_comm, round_add_natCast, add_comm]
-- 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 : α
y : ℕ
rw : round (x + (↑y : α)) = (↑y : ℤ) + round x
⊢ round ((↑y : α) + x) = (↑y : ℤ) + round x
have rw₁ : round x + (↑y : ℤ) = (↑y : ℤ) + round x
Tactic: rw [add_comm, round_add_natCast, add_comm]
-- 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 : α
y : ℕ
rw : round (x + (↑y : α)) = (↑y : ℤ) + round x
rw₁ : round x + (↑y : ℤ) = (↑y : ℤ) + round x
⊢ round ((↑y : α) + x) = (↑y : ℤ) + round x
have rw₂ : (↑y : ℤ) + round x = (↑y : ℤ) + round x
Tactic: rw [add_comm, round_add_natCast, add_comm]
-- 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 : α
⊢ |x - (↑(round x) : α)| = min (fract x) (1 - fract x)
have simp_rw : |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
Tactic: simp_rw [round, min_def_lt, two_mul, ← lt_tsub_iff_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 : α
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inl : ∀ (hx : fract x < 1 - fract x),
  |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
Tactic: rcases lt_or_ge (fract x) (1 - fract x) with hx | 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 : α
inl :
  ∀ (hx : fract x < 1 - fract x),
    |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inr : ∀ (hx : 1 - fract x ≤ fract x),
  |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
Tactic: rcases lt_or_ge (fract x) (1 - fract x) with hx | 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 : fract x < 1 - fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inl : |x - (↑⌊x⌋ : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
Tactic: rw [if_pos hx, if_pos hx, self_sub_floor, abs_fract]
-- 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 : fract x < 1 - fract x
inl : |x - (↑⌊x⌋ : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inl₁ : |x - (↑⌊x⌋ : α)| = fract x
Tactic: rw [if_pos hx, if_pos hx, self_sub_floor, abs_fract]
-- 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 : fract x < 1 - fract x
inl : |x - (↑⌊x⌋ : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
inl₁ : |x - (↑⌊x⌋ : α)| = fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inl₂ : |fract x| = fract x
Tactic: rw [if_pos hx, if_pos hx, self_sub_floor, abs_fract]
-- 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 : fract x < 1 - fract x
inl : |x - (↑⌊x⌋ : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
inl₁ : |x - (↑⌊x⌋ : α)| = fract x
inl₂ : |fract x| = fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inl₃ : fract x = fract x
Tactic: rw [if_pos hx, if_pos hx, self_sub_floor, abs_fract]
-- 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 : α
hx : 1 - fract x ≤ fract x
⊢ 0 < fract x
have hx₁ : 0 < fract x + fract x
Tactic: replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)
Cleared hypotheses: hx
-- 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 : α
hx : 1 - fract x ≤ fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have this : 0 < fract x
Tactic: have : 0 < fract x := by
      replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)
      simpa only [← two_mul, mul_pos_iff_of_pos_left, zero_lt_two] using 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 : 1 - fract x ≤ fract x
this : 0 < fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inr : |x - (↑⌈x⌉ : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
Tactic: rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm,
      abs_one_sub_fract]
-- 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 : 1 - fract x ≤ fract x
this : 0 < fract x
inr : |x - (↑⌈x⌉ : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inr₁ : |x - (↑⌈x⌉ : α)| = 1 - fract x
Tactic: rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm,
      abs_one_sub_fract]
-- 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 : 1 - fract x ≤ fract x
this : 0 < fract x
inr : |x - (↑⌈x⌉ : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
inr₁ : |x - (↑⌈x⌉ : α)| = 1 - fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inr₂ : |(↑⌈x⌉ : α) - x| = 1 - fract x
Tactic: rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm,
      abs_one_sub_fract]
-- 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 : 1 - fract x ≤ fract x
this : 0 < fract x
inr : |x - (↑⌈x⌉ : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
inr₁ : |x - (↑⌈x⌉ : α)| = 1 - fract x
inr₂ : |(↑⌈x⌉ : α) - x| = 1 - fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inr₃ : |1 - fract x| = 1 - fract x
Tactic: rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm,
      abs_one_sub_fract]
-- 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 : 1 - fract x ≤ fract x
this : 0 < fract x
inr : |x - (↑⌈x⌉ : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
inr₁ : |x - (↑⌈x⌉ : α)| = 1 - fract x
inr₂ : |(↑⌈x⌉ : α) - x| = 1 - fract x
inr₃ : |1 - fract x| = 1 - fract x
⊢ |x - (↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉) : α)| = if fract x < 1 - fract x then fract x else 1 - fract x
have inr₄ : 1 - fract x = 1 - fract x
Tactic: rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm,
      abs_one_sub_fract]
-- 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 : α
z : ℤ
⊢ |x - (↑(round x) : α)| ≤ |x - (↑z : α)|
have rw : fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
Tactic: rw [abs_sub_round_eq_min, min_le_iff]
-- 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 : α
z : ℤ
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
have inl : ∀ (hx : (↑z : α) ≤ x), fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
Tactic: rcases le_or_gt (z : α) x with (hx | 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 : α
z : ℤ
inl : ∀ (hx : (↑z : α) ≤ x), fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
have inr : ∀ (hx : x < (↑z : α)), fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
Tactic: rcases le_or_gt (z : α) x with (hx | 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 : α
z : ℤ
hx : (↑z : α) ≤ x
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
have inl : fract x ≤ |x - (↑z : α)|
Tactic: 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 : α
z : ℤ
hx : x < (↑z : α)
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
have inr : 1 - fract x ≤ |x - (↑z : α)|
Tactic: right
-- 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 : α
z : ℤ
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
have inl : ∀ (hx : (↑z : α) ≤ x), fract x ≤ |x - (↑z : α)|
Tactic: rcases le_or_gt (z : α) x with (hx | hx) <;> [left; right]
-- 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 : α
z : ℤ
inl : ∀ (hx : (↑z : α) ≤ x), fract x ≤ |x - (↑z : α)|
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
have inr : ∀ (hx : x < (↑z : α)), 1 - fract x ≤ |x - (↑z : α)|
Tactic: rcases le_or_gt (z : α) x with (hx | hx) <;> [left; right]
-- 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 : α
z : ℤ
hx : (↑z : α) ≤ x
| |x - (↑z : α)|
have rw : fract x + HSub.hSub (α := α) (↑⌊x⌋ : α) (↑z : α)
Tactic: rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]