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 : α
z : ℤ
hx : (↑z : α) ≤ x
⊢ fract x ≤ |x - (↑z : α)|
have inl : fract x ≤ fract x + HSub.hSub (α := α) (↑⌊x⌋ : α) (↑z : α)
Tactic: conv_rhs => rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]
-- 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 : α)
⊢ 1 - fract x ≤ |x - (↑z : α)|
have inr : 1 - fract x ≤ -(x - (↑z : α))
Tactic: rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).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 : α
z : ℤ
hx : x < (↑z : α)
| -(x - (↑z : α))
have rw : -(fract x + (↑⌊x⌋ : α) - (↑z : α))
Tactic: rw [← fract_add_floor x]
-- 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 : α)
⊢ 1 - fract x ≤ -(x - (↑z : α))
have inr : 1 - fract x ≤ -(fract x + (↑⌊x⌋ : α) - (↑z : α))
Tactic: conv_rhs => rw [← fract_add_floor x]
-- 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 : α)
⊢ 1 - fract x ≤ -(fract x + (↑⌊x⌋ : α) - (↑z : α))
have inr : (↑⌊x⌋ : α) ≤ HSub.hSub (α := α) (↑z : α) 1
Tactic: rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
      le_sub_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 : α
z : ℤ
hx : x < (↑z : α)
⊢ (↑⌊x⌋ : α) ≤ HSub.hSub (α := α) (↑z : α) 1
have inr : ⌊x⌋ ≤ z - 1
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 : α
z : ℤ
hx : x < (↑z : α)
⊢ ⌊x⌋ ≤ z - 1
have inr : ⌊x⌋ < z
Tactic: rwa [le_sub_one_iff, floor_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ round x = ⌊x + 1 / 2⌋
have rw : (⌊2 * x⌋ + 1) / 2 = ⌊(↑2 : α) * (x + 1 / 2)⌋ / 2
Tactic: rw [← cast_mul_floor_div_cancel_of_pos two_pos, round_eq_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ |x - (↑(round x) : α)| ≤ 1 / 2
have rw : x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2 ∧ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
Tactic: rw [round_eq, abs_sub_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (hypothesis)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2 ∧ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
have this : (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2
Tactic: have := floor_le (x + 1 / 2)
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (hypothesis)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
this : (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2 ∧ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
have this₁ : x + 1 / 2 < HAdd.hAdd (α := α) (↑⌊x + 1 / 2⌋ : α) 1
Tactic: have := lt_floor_add_one (x + 1 / 2)
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2 ∧ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
have left : x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2 ∧ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
have right : (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2
have linarith : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
linarith : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → 2 / 2 = 1
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2
have linarith₁ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → HMul.hMul (α := α) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
linarith : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → 2 / 2 = 1
linarith₁ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → HMul.hMul (α := α) 1 2 = 2
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2
have linarith₂ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → GT.gt.{u_2} (α := α) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
linarith : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → 2 / 2 = 1
linarith₁ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → HMul.hMul (α := α) 1 2 = 2
linarith₂ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → GT.gt.{u_2} (α := α) 2 0
linarith₃ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → 2 / 2 = 1
linarith₄ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → HMul.hMul (α := α) 1 2 = 2
linarith₅ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → GT.gt.{u_2} (α := α) 2 0
linarith₆ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → 2 / 2 = 1
linarith₇ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → HMul.hMul (α := α) 1 2 = 2
linarith₈ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → GT.gt.{u_2} (α := α) 2 0
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2
have linarith₉ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) →
  2 * x + HMul.hMul (α := α) 1 1 - (HMul.hMul (α := α) 2 (↑⌊x + 1 / 2⌋ : α) + HMul.hMul (α := α) 2 1) +
      (HMul.hMul (α := α) 1 1 - (2 * x - HMul.hMul (α := α) 2 (↑⌊x + 1 / 2⌋ : α))) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
⊢ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
have linarith : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
linarith : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → 2 / 2 = 1
⊢ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
have linarith₁ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → HMul.hMul (α := α) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
linarith : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → 2 / 2 = 1
linarith₁ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → HMul.hMul (α := α) 1 2 = 2
⊢ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
have linarith₂ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → GT.gt.{u_2} (α := α) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
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
linarith : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → 2 / 2 = 1
linarith₁ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → HMul.hMul (α := α) 1 2 = 2
linarith₂ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → GT.gt.{u_2} (α := α) 2 0
linarith₃ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → 2 / 2 = 1
linarith₄ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → HMul.hMul (α := α) 1 2 = 2
linarith₅ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → GT.gt.{u_2} (α := α) 2 0
linarith₆ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → 2 / 2 = 1
linarith₇ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → HMul.hMul (α := α) 1 2 = 2
linarith₈ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → GT.gt.{u_2} (α := α) 2 0
⊢ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2
have linarith₉ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x →
  HMul.hMul (α := α) 2 (↑⌊x + 1 / 2⌋ : α) - (2 * x + HMul.hMul (α := α) 1 1) +
      (HMul.hMul (α := α) 1 1 - (HMul.hMul (α := α) 2 (↑⌊x + 1 / 2⌋ : α) - 2 * x)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have inl : |HDiv.hDiv (α := α) (↑m : α) (↑0 : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑0 : α))) : α)| =
  HDiv.hDiv (α := α) (↑(min (m % 0) (0 - m % 0)) : α) (↑0 : α)
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
inl :
  |HDiv.hDiv (α := α) (↑m : α) (↑0 : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑0 : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % 0) (0 - m % 0)) : α) (↑0 : α)
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have inr : ∀ (hn : n > 0),
  |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
⊢ LT.lt.{u_2} (α := α) 0 (↑n : α)
have norm_cast : 0 < n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (hypothesis)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have hn' : LT.lt.{u_2} (α := α) 0 (↑n : α)
Tactic: have hn' : 0 < (n : α) := by
    norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_2} (α := α) 0 (↑n : α)
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have inr : min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
  HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
Tactic: rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_2} (α := α) 0 (↑n : α)
inr :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have inr₁ : min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
  HDiv.hDiv (α := α) (min (↑(m % n) : α) (↑(n - m % n) : α)) (↑n : α)
Tactic: rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_2} (α := α) 0 (↑n : α)
inr :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
inr₁ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (min (↑(m % n) : α) (↑(n - m % n) : α)) (↑n : α)
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have inr₂ : min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
Tactic: rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_2} (α := α) 0 (↑n : α)
inr :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
inr₁ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (min (↑(m % n) : α) (↑(n - m % n) : α)) (↑n : α)
inr₂ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have inr₃ : min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
Tactic: rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_2} (α := α) 0 (↑n : α)
inr :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
inr₁ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (min (↑(m % n) : α) (↑(n - m % n) : α)) (↑n : α)
inr₂ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
inr₃ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have inr₄ : min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HSub.hSub (α := α) (↑n : α) (↑(m % n) : α) / (↑n : α))
Tactic: rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_2} (α := α) 0 (↑n : α)
inr :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
inr₁ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (min (↑(m % n) : α) (↑(n - m % n) : α)) (↑n : α)
inr₂ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
inr₃ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
inr₄ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HSub.hSub (α := α) (↑n : α) (↑(m % n) : α) / (↑n : α))
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have inr₅ : min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α))
    (HDiv.hDiv (α := α) (↑n : α) (↑n : α) - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α))
Tactic: rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_2} (α := α) 0 (↑n : α)
inr :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
inr₁ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (min (↑(m % n) : α) (↑(n - m % n) : α)) (↑n : α)
inr₂ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
inr₃ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
inr₄ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HSub.hSub (α := α) (↑n : α) (↑(m % n) : α) / (↑n : α))
inr₅ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α))
      (HDiv.hDiv (α := α) (↑n : α) (↑n : α) - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α))
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
have inr₆ : min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α))
Tactic: rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ x - 1 / 2 = x + 1 / 2 - 1
have linarith : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
linarith : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
⊢ x - 1 / 2 = x + 1 / 2 - 1
have linarith₁ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
linarith : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₁ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₂ : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₃ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
⊢ x - 1 / 2 = x + 1 / 2 - 1
have linarith₄ : x - 1 / 2 < x + 1 / 2 - 1 → GT.gt.{u_2} (α := α) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
linarith : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₁ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₂ : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₃ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₄ : x - 1 / 2 < x + 1 / 2 - 1 → GT.gt.{u_2} (α := α) 2 0
⊢ x - 1 / 2 = x + 1 / 2 - 1
have linarith₅ : x - 1 / 2 < x + 1 / 2 - 1 →
  2 * x - HMul.hMul (α := α) 1 1 - (2 * x + HMul.hMul (α := α) 1 1 - HMul.hMul (α := α) 2 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Order.Round (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
linarith : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₁ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₂ : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₃ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₄ : x - 1 / 2 < x + 1 / 2 - 1 → GT.gt.{u_2} (α := α) 2 0
linarith₅ :
  x - 1 / 2 < x + 1 / 2 - 1 →
    2 * x - HMul.hMul (α := α) 1 1 - (2 * x + HMul.hMul (α := α) 1 1 - HMul.hMul (α := α) 2 1) = 0
⊢ x - 1 / 2 = x + 1 / 2 - 1
have linarith₆ : x + 1 / 2 - 1 < x - 1 / 2 → 2 / 2 = 1
Tactic: linarith