awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg : 0 < fract x
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
suffices 0 < fract x by simp [this, H, ceil_eq_iff, (fract_lt_one _).le]
-- 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
neg : ∀ (h : fract x ≤ 0), 2 * fract x < 1
⊢ 0 < fract x

Tactic:
contrapose! 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 : fract x ≤ 0
neg : HMul.hMul (α := α) 2 0 < 1
⊢ 2 * fract x < 1

Tactic:
grw [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 : fract x ≤ 0
⊢ HMul.hMul (α := α) 2 0 < 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
⊢ round.{u_2} (α := α) 0 = 0

Tactic:
simp [round]

Premises used: round
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
⊢ round.{u_2} (α := α) 1 = 1

Tactic:
simp [round]

Premises used: round
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n : ℕ
⊢ round.{u_2} (α := α) (↑n : α) = (↑n : ℤ)

Tactic:
simp [round]

Premises used: round
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n : ℕ
inst_4 : n.AtLeastTwo
⊢ round.{u_2} (α := α) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
round_natCast n

Premises used: round_natCast
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n : ℤ
⊢ round.{u_2} (α := α) (↑n : α) = n

Tactic:
simp [round]

Premises used: round
-- Module: Mathlib.Algebra.Order.Round
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
inr : ∀ (hx' : 2 * x ∉ range Int.cast), round x = ⌈2 * x⌉ / 2
⊢ round x = ⌈2 * x⌉ / 2

Tactic:
rcases em (2 * x ∈ range Int.cast) with ⟨m, hm⟩ | hx'

Premises used: Int.cast, HMul.hMul, Membership.mem, em, Set.range, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Round
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 : round x = m / 2
⊢ round x = ⌈2 * x⌉ / 2

Tactic:
rw [← hm, ceil_intCast]

Premises used: Int.ceil_intCast
-- Module: Mathlib.Algebra.Order.Round
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
inl₁ : ∀ (m : ℤ) (hm : (↑(2 * m + 1) : α) = 2 * x), round x = (2 * m + 1) / 2
⊢ round x = m / 2

Tactic:
rcases m.even_or_odd with ⟨m, rfl⟩ | ⟨m, rfl⟩

Premises used: Int.even_or_odd, rfl
-- Module: Mathlib.Algebra.Order.Round
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
⊢ HMul.hMul (α := α) 2 (↑m : α) = 2 * x

Tactic:
simp [← hm, ← two_mul]

Premises used: two_mul
-- Module: Mathlib.Algebra.Order.Round
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
inl :
  ∀ (hx : HMul.hMul (α := α) 2 (fract (↑m : α)) ≠ 1) (hm : (↑(m + m) : α) = HMul.hMul (α := α) 2 (↑m : α)),
    round.{u_2} (α := α) (↑m : α) = (m + m) / 2
⊢ round x = (m + m) / 2

Tactic:
obtain rfl : m = x := mul_left_cancel₀ two_ne_zero <| by simp [← hm, ← two_mul]

Premises used: mul_left_cancel₀, two_ne_zero, rfl
-- Module: Mathlib.Algebra.Order.Round
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
inl₂ inl₃ : m = m
⊢ round.{u_2} (α := α) (↑m : α) = (m + m) / 2

Tactic:
rw [round_intCast, ← two_mul, Int.mul_ediv_cancel_left _ two_ne_zero]

Premises used: two_mul, round_intCast, two_ne_zero, Int.mul_ediv_cancel_left
-- Module: Mathlib.Algebra.Order.Round
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

Tactic:
absurd ?_ hx

Premises used: absurd
-- Module: Mathlib.Algebra.Order.Round
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
inl : 2 * fract x = 1
⊢ round x = (2 * m + 1) / 2

Tactic:
refine absurd ?_ hx

Premises used: absurd
-- Module: Mathlib.Algebra.Order.Round
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
⊢ 2 * fract x = 1

Tactic:
(mul_fract_eq_one_iff_exists_int one_lt_two).mpr ⟨m, mod_cast hm.symm⟩

Premises used: Iff.mpr, Int.cast, HMul.hMul, congrArg, cast, Int.cast_ofNat, Nat.cast, Int.cast_mul._simp_1, HAdd.hAdd, Exists.intro, one_lt_two, Int.cast_add._simp_1, congrFun', Int.mul_fract_eq_one_iff_exists_int, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Int.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Round
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
⊢ 2 * fract x = 1

Tactic:
exact (mul_fract_eq_one_iff_exists_int one_lt_two).mpr ⟨m, mod_cast hm.symm⟩

Premises used: Iff.mpr, Exists.intro, one_lt_two, Int.mul_fract_eq_one_iff_exists_int
-- Module: Mathlib.Algebra.Order.Round
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
inr₁ inr₂ : (⌊2 * x⌋ + 1) / 2 = (⌊2 * x⌋ + 1) / 2
⊢ round x = ⌈2 * x⌉ / 2

Tactic:
rw [round_eq_div, (ceil_eq_floor_add_one_iff_notMem _).mpr hx']

Premises used: Iff.mpr, round_eq_div, Int.ceil_eq_floor_add_one_iff_notMem
-- Module: Mathlib.Algebra.Order.Round
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
rw₆ rw₇ : (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
⊢ round (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]

Premises used: apply_ite₂, ite_self, Int.fract_add_intCast, Int.floor_add_intCast, round, Int.ceil_add_intCast
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
a : α
rw : round (a + 1) = round (a + (↑1 : α))
rw₁ rw₂ : round (a + 1) = round (a + 1)
⊢ round (a + 1) = round a + 1

Tactic:
rw [← round_add_intCast a 1, cast_one]

Premises used: round_add_intCast, OfNat.ofNat, Int.cast_one
-- Module: Mathlib.Algebra.Order.Round
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

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
y : ℤ
norm_cast : round (x + (↑(-y) : α)) = round x - y
⊢ round (x + -(↑y : α)) = round x - y

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
y : ℤ
rw : round x + -y = round x - y
rw₁ rw₂ : round x + -y = round x + -y
⊢ round (x + (↑(-y) : α)) = round x - y

Tactic:
rw [round_add_intCast, sub_eq_add_neg]

Premises used: sub_eq_add_neg, round_add_intCast
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
a : α
rw : round (a - 1) = round (a - (↑1 : α))
rw₁ rw₂ : round (a - 1) = round (a - 1)
⊢ round (a - 1) = round a - 1

Tactic:
rw [← round_sub_intCast a 1, cast_one]

Premises used: round_sub_intCast, OfNat.ofNat, Int.cast_one
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
y : ℕ
⊢ round (x + (↑y : α)) = round x + (↑y : ℤ)

Tactic:
mod_cast round_add_intCast x y

Premises used: Int.cast_natCast, congrArg, round_add_intCast, cast, Nat.cast, HAdd.hAdd, round, congrFun', Eq
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
n : ℕ
inst_4 : n.AtLeastTwo
⊢ round (x + OfNat.ofNat n) = round x + OfNat.ofNat n

Tactic:
round_add_natCast x n

Premises used: round_add_natCast
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
y : ℕ
⊢ round (x - (↑y : α)) = round x - (↑y : ℤ)

Tactic:
mod_cast round_sub_intCast x y

Premises used: Int.cast_natCast, round_sub_intCast, congrArg, HSub.hSub, cast, Nat.cast, round, congrFun', Eq
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
n : ℕ
inst_4 : n.AtLeastTwo
⊢ round (x - OfNat.ofNat n) = round x - OfNat.ofNat n

Tactic:
round_sub_natCast x n

Premises used: round_sub_natCast
-- Module: Mathlib.Algebra.Order.Round
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
rw₂ rw₃ : y + round x = y + round x
⊢ round ((↑y : α) + x) = y + round x

Tactic:
rw [add_comm, round_add_intCast, add_comm]

Premises used: round_add_intCast, add_comm
-- Module: Mathlib.Algebra.Order.Round
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
rw₂ rw₃ : (↑y : ℤ) + round x = (↑y : ℤ) + round x
⊢ round ((↑y : α) + x) = (↑y : ℤ) + round x

Tactic:
rw [add_comm, round_add_natCast, add_comm]

Premises used: round_add_natCast, add_comm
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
n : ℕ
inst_4 : n.AtLeastTwo
x : α
⊢ round (OfNat.ofNat n + x) = OfNat.ofNat n + round x

Tactic:
round_natCast_add x n

Premises used: round_natCast_add
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
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
⊢ |x - (↑(round x) : α)| = min (fract x) (1 - fract x)

Tactic:
simp_rw [round, min_def_lt, two_mul, ← lt_tsub_iff_left]

Premises used: two_mul, round, min_def_lt, lt_tsub_iff_left
-- Module: Mathlib.Algebra.Order.Round
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
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
⊢ |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

Premises used: Int.fract, HSub.hSub, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Round
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
inl₃ 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

Tactic:
rw [if_pos hx, if_pos hx, self_sub_floor, abs_fract]

Premises used: Int.abs_fract, if_pos, Int.self_sub_floor
-- Module: Mathlib.Algebra.Order.Round
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 + fract x

Tactic:
replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
hx : 0 < fract x + fract x
⊢ 0 < fract x

Tactic:
simpa only [← two_mul, mul_pos_iff_of_pos_left, zero_lt_two] using hx

Premises used: two_mul, mul_pos_iff_of_pos_left, zero_lt_two
-- Module: Mathlib.Algebra.Order.Round
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

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
-- Module: Mathlib.Algebra.Order.Round
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
inr₄ 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

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]

Premises used: Iff.mpr, Ne.symm, not_lt, Int.ceil_sub_self_eq, Int.abs_one_sub_fract, abs_sub_comm, if_neg, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
rw : fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
⊢ |x - (↑(round x) : α)| ≤ |x - (↑z : α)|

Tactic:
rw [abs_sub_round_eq_min, min_le_iff]

Premises used: min_le_iff, abs_sub_round_eq_min
-- Module: Mathlib.Algebra.Order.Round
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 : α)|
inr : ∀ (hx : x < (↑z : α)), fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|

Tactic:
rcases le_or_gt (z : α) x with (hx | hx)

Premises used: Int.cast, le_or_gt
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : (↑z : α) ≤ x
inl : fract x ≤ |x - (↑z : α)|
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|

Tactic:
left
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : x < (↑z : α)
inr : 1 - fract x ≤ |x - (↑z : α)|
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|

Tactic:
right
-- Module: Mathlib.Algebra.Order.Round
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 : α)|
inr : ∀ (hx : x < (↑z : α)), 1 - fract x ≤ |x - (↑z : α)|
⊢ fract x ≤ |x - (↑z : α)| ∨ 1 - fract x ≤ |x - (↑z : α)|

Tactic:
rcases le_or_gt (z : α) x with (hx | hx) <;> [left; right]

Premises used: Int.cast, le_or_gt
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : (↑z : α) ≤ x
rw : fract x + HSub.hSub (α := α) (↑⌊x⌋ : α) (↑z : α)
| |x - (↑z : α)|

Tactic:
rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]

Premises used: Iff.mpr, add_sub_assoc, Int.fract_add_floor, sub_nonneg, abs_eq_self
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : (↑z : α) ≤ x
inl : fract x ≤ fract x + HSub.hSub (α := α) (↑⌊x⌋ : α) (↑z : α)
⊢ fract x ≤ |x - (↑z : α)|

Tactic:
conv_rhs => rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]

Premises used: Iff.mpr, add_sub_assoc, Int.fract_add_floor, sub_nonneg, abs_eq_self
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : (↑z : α) ≤ x
⊢ fract x ≤ fract x + HSub.hSub (α := α) (↑⌊x⌋ : α) (↑z : α)

Tactic:
simpa only [le_add_iff_nonneg_right, sub_nonneg, cast_le] using le_floor.mpr hx

Premises used: Iff.mpr, le_add_iff_nonneg_right, Int.cast_le, Int.le_floor, sub_nonneg
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : x < (↑z : α)
inr : 1 - fract x ≤ -(x - (↑z : α))
⊢ 1 - fract x ≤ |x - (↑z : α)|

Tactic:
rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]

Premises used: sub_neg, Iff.mpr, LT.lt.le, abs_eq_neg_self
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : x < (↑z : α)
rw : -(fract x + (↑⌊x⌋ : α) - (↑z : α))
| -(x - (↑z : α))

Tactic:
rw [← fract_add_floor x]

Premises used: Int.fract_add_floor
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : x < (↑z : α)
inr : 1 - fract x ≤ -(fract x + (↑⌊x⌋ : α) - (↑z : α))
⊢ 1 - fract x ≤ -(x - (↑z : α))

Tactic:
conv_rhs => rw [← fract_add_floor x]

Premises used: Int.fract_add_floor
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : x < (↑z : α)
inr : (↑⌊x⌋ : α) ≤ HSub.hSub (α := α) (↑z : α) 1
⊢ 1 - fract x ≤ -(fract x + (↑⌊x⌋ : α) - (↑z : α))

Tactic:
rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
      le_sub_comm]

Premises used: add_sub_assoc, neg_sub, neg_add, le_add_neg_iff_add_le, add_comm, sub_add_cancel, le_sub_comm
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : x < (↑z : α)
inr : ⌊x⌋ ≤ z - 1
⊢ (↑⌊x⌋ : α) ≤ HSub.hSub (α := α) (↑z : α) 1

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
z : ℤ
hx : x < (↑z : α)
inr : ⌊x⌋ < z
inr₁ inr₂ inr₃ inr₄ : x < (↑z : α)
⊢ ⌊x⌋ ≤ z - 1

Tactic:
rwa [le_sub_one_iff, floor_lt]

Premises used: Int.le_sub_one_iff, Int.floor_lt
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
rw : (⌊2 * x⌋ + 1) / 2 = ⌊(↑2 : α) * (x + 1 / 2)⌋ / 2
⊢ round x = ⌊x + 1 / 2⌋

Tactic:
rw [← cast_mul_floor_div_cancel_of_pos two_pos, round_eq_div]

Premises used: round_eq_div, two_pos, Int.cast_mul_floor_div_cancel_of_pos
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ (⌊2 * x⌋ + 1) / 2 = ⌊(↑2 : α) * (x + 1 / 2)⌋ / 2

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
n : ℤ
⊢ round x = n ↔ x ∈ Ico ((↑n : α) - 1 / 2) ((↑n : α) + 1 / 2)

Tactic:
norm_num [round_eq, floor_eq_iff, ← lt_sub_iff_add_lt, add_sub_assoc]

Premises used: add_sub_assoc, round_eq, Int.floor_eq_iff, lt_sub_iff_add_lt
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
⊢ round.{u_2} (α := α) 2⁻¹ = 1

Tactic:
norm_num [round_eq_iff]

Premises used: round_eq_iff
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
⊢ round.{u_2} (α := α) (-2⁻¹) = 0

Tactic:
norm_num [round_eq_iff]

Premises used: round_eq_iff
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ round x = 0 ↔ x ∈ Ico (-(1 / 2)) (1 / 2)

Tactic:
simp [round_eq_iff]

Premises used: round_eq_iff
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
rw : x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2 ∧ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
⊢ |x - (↑(round x) : α)| ≤ 1 / 2

Tactic:
rw [round_eq, abs_sub_le_iff]

Premises used: abs_sub_le_iff, round_eq
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2

Tactic:
have := floor_le (x + 1 / 2)
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
this : (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2
⊢ x + 1 / 2 < HAdd.hAdd (α := α) (↑⌊x + 1 / 2⌋ : α) 1

Tactic:
have := lt_floor_add_one (x + 1 / 2)
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
this_1 : (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2
this : x + 1 / 2 < HAdd.hAdd (α := α) (↑⌊x + 1 / 2⌋ : α) 1
left : x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2
right : (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2 ∧ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2

Tactic:
constructor