awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
s : Set R
y : R
hys : y ∈ s
h0 : 0 ≤ y - (↑⌊y⌋ : R)
h1 : y - (↑⌊y⌋ : R) < 1
⊢ ∃ x ∈ s, fract x = y - (↑⌊y⌋ : R)

Tactic:
⟨y, hys, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
s : Set R
y : R
hys : y ∈ s
h0 : 0 ≤ y - (↑⌊y⌋ : R)
h1 : y - (↑⌊y⌋ : R) < 1
⊢ ∃ x ∈ s, fract x = y - (↑⌊y⌋ : R)

Tactic:
exact ⟨y, hys, rfl⟩
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
a b : k
ha : 0 < a
⊢ fract (b / a) * a ∈ Ico 0 a

Tactic:
⟨(mul_nonneg_iff_of_pos_right ha).2 (fract_nonneg (b / a)),
    (mul_lt_iff_lt_one_left ha).2 (fract_lt_one (b / a))⟩

Premises used: Iff.mpr, mul_nonneg_iff_of_pos_right, Set.Mem, setOf, HDiv.hDiv, mul_lt_iff_lt_one_left, Set.Ico, And.intro, Int.fract_lt_one, Int.fract_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : FloorRing k
a b : k
ha : a ≠ 0
rw : fract (b / a) * a + (↑⌊b / a⌋ : k) * a = b
rw₁ : (fract (b / a) + (↑⌊b / a⌋ : k)) * a = b
rw₂ : b / a * a = b
rw₃ rw₄ : b = b
⊢ fract (b / a) * a + ⌊b / a⌋ • a = b

Tactic:
rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b ha]

Premises used: add_mul, zsmul_eq_mul, div_mul_cancel₀, Int.fract_add_floor
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
b a : k
hb : 0 < b
⊢ 0 ≤ a - (↑⌊a / b⌋ : k) * b

Tactic:
sub_nonneg_of_le <| (le_div_iff₀ hb).1 <| floor_le _

Premises used: sub_nonneg_of_le, Iff.mp, Int.floor_le, le_div_iff₀
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
b a : k
hb : 0 < b
rw : a / b < HAdd.hAdd (α := k) (↑⌊a / b⌋ : k) 1
⊢ a < b + (↑⌊a / b⌋ : k) * b

Tactic:
rw [← one_add_mul, ← div_lt_iff₀ hb, add_comm]

Premises used: div_lt_iff₀, add_comm, one_add_mul
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < HAdd.hAdd (α := k) (↑⌊a / b⌋ : k) 1

Tactic:
lt_floor_add_one _

Premises used: Int.lt_floor_add_one
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < HAdd.hAdd (α := k) (↑⌊a / b⌋ : k) 1

Tactic:
exact lt_floor_add_one _

Premises used: Int.lt_floor_add_one
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
inl : fract (HDiv.hDiv (α := k) (↑m : k) (↑0 : k)) = HDiv.hDiv (α := k) (↑(m % 0) : k) (↑0 : k)
inr : ∀ (hn : n > 0), fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℕ
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑0 : k)) = HDiv.hDiv (α := k) (↑(m % 0) : k) (↑0 : k)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
hn : n > 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < n
⊢ LT.lt.{u_4} (α := k) 0 (↑n : k)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
hn : n > 0
⊢ LT.lt.{u_4} (α := k) 0 (↑n : k)

Tactic:
have hn' : 0 < (n : k) := by
    norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)

Tactic:
fract_eq_iff.mpr ⟨?_, ?_, m / n, ?_⟩

Premises used: Iff.mpr, HDiv.hDiv, Nat.cast, And.intro, Exists.intro, Int.fract_eq_iff
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
inr : 0 ≤ HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)
inr₁ : HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k) < 1
inr₂ :
  HDiv.hDiv (α := k) (↑m : k) (↑n : k) - HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k) =
    (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)

Tactic:
refine fract_eq_iff.mpr ⟨?_, ?_, m / n, ?_⟩

Premises used: Iff.mpr, HDiv.hDiv, Nat.cast, And.intro, Exists.intro, Int.fract_eq_iff
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
⊢ 0 ≤ HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k)

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
⊢ HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k) < 1

Tactic:
simpa only [div_lt_one hn', Nat.cast_lt] using m.mod_lt hn

Premises used: Nat.mod_lt, div_lt_one, Nat.cast_lt
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
inr : (↑m : k) = (↑(m % n) : k) + HMul.hMul (α := k) (↑n : k) (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k)
⊢ HDiv.hDiv (α := k) (↑m : k) (↑n : k) - HDiv.hDiv (α := k) (↑(m % n) : k) (↑n : k) =
    (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k)

Tactic:
rw [sub_eq_iff_eq_add', ← mul_right_inj' hn'.ne', mul_div_cancel₀ _ hn'.ne', mul_add,
      mul_div_cancel₀ _ hn'.ne']

Premises used: mul_div_cancel₀, LT.lt.ne', mul_add, mul_right_inj', sub_eq_iff_eq_add'
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
inr : (↑m : k) = HAdd.hAdd (α := k) (↑(m % n) : k) (↑(n * (m / n)) : k)
⊢ (↑m : k) = (↑(m % n) : k) + HMul.hMul (α := k) (↑n : k) (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_4} (α := k) 0 (↑n : k)
inr : Eq.{u_4 + 1} (α := k) (↑m : k) (↑(m % n + n * (m / n)) : k)
inr₁ inr₂ : Eq.{u_4 + 1} (α := k) (↑m : k) (↑m : k)
⊢ (↑m : k) = HAdd.hAdd (α := k) (↑(m % n) : k) (↑(n * (m / n)) : k)

Tactic:
rw [← Nat.cast_add, Nat.mod_add_div m n]

Premises used: Nat.cast_add, Nat.mod_add_div
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
inl : fract (HDiv.hDiv (α := k) (↑m : k) (↑0 : k)) = HDiv.hDiv (α := k) (↑(m % (↑0 : ℤ)) : k) (↑0 : k)
inr : ∀ (hn : n > 0), fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % (↑n : ℤ)) : k) (↑n : k)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % (↑n : ℤ)) : k) (↑n : k)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑0 : k)) = HDiv.hDiv (α := k) (↑(m % (↑0 : ℤ)) : k) (↑0 : k)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
hn : n > 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < n
⊢ LT.lt.{u_4} (α := k) 0 (↑n : k)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
hn : n > 0
⊢ LT.lt.{u_4} (α := k) 0 (↑n : k)

Tactic:
replace hn : 0 < (n : k) := by norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
l : ℤ
hl : 0 ≤ l
inl :
  ∀ (l₀ : ℕ) (hl : LE.le (α := ℤ) 0 (↑l₀ : ℤ)),
    fract (HDiv.hDiv (α := k) (↑(↑l₀ : ℤ) : k) (↑n : k)) =
      HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑l₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)
inr :
  ∀ (l₀ : ℕ) (hl : LE.le (α := ℤ) 0 (-(↑l₀ : ℤ))),
    fract (HDiv.hDiv (α := k) (↑(-(↑l₀ : ℤ)) : k) (↑n : k)) =
      HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑l₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)
⊢ fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)

Tactic:
obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
l₀ : ℕ
hl : LE.le (α := ℤ) 0 (↑l₀ : ℤ)
inl :
  fract (HDiv.hDiv (α := k) (↑l₀ : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑l₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)
inl₁ : fract (HDiv.hDiv (α := k) (↑l₀ : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(↑(l₀ % n) : ℤ) : k) (↑n : k)
inl₂ : fract (HDiv.hDiv (α := k) (↑l₀ : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l₀ % n) : k) (↑n : k)
inl₃ inl₄ : HDiv.hDiv (α := k) (↑(l₀ % n) : k) (↑n : k) = HDiv.hDiv (α := k) (↑(l₀ % n) : k) (↑n : k)
⊢ fract (HDiv.hDiv (α := k) (↑(↑l₀ : ℤ) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑l₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)

Tactic:
rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]

Premises used: Int.cast_natCast, Int.fract_div_natCast_eq_div_natCast_mod, Int.natCast_mod
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
l₀ : ℕ
hl : LE.le (α := ℤ) 0 (-(↑l₀ : ℤ))
⊢ l₀ = 0

Tactic:
rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl

Premises used: Right.nonneg_neg_iff, Int.natCast_nonpos_iff
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
l₀ : ℕ
hl : l₀ = 0
⊢ fract (HDiv.hDiv (α := k) (↑(-(↑l₀ : ℤ)) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑l₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)

Tactic:
simp [hl]
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
⊢ ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)

Tactic:
have : ∀ {l : ℤ}, 0 ≤ l → fract ((l : k) / n) = ↑(l % n) / n := by
    intro l hl
    obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg
    · rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]
    · rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl
      simp [hl]
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
inr :
  ∀ (m₀ : ℕ),
    fract (HDiv.hDiv (α := k) (↑(↑m₀ : ℤ) : k) (↑n : k)) =
      HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑m₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)
inr₁ :
  ∀ (m₀ : ℕ),
    fract (HDiv.hDiv (α := k) (↑(-(↑m₀ : ℤ)) : k) (↑n : k)) =
      HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % (↑n : ℤ)) : k) (↑n : k)

Tactic:
obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
⊢ fract (HDiv.hDiv (α := k) (↑(↑m₀ : ℤ) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑m₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)

Tactic:
this (natCast_nonneg m₀)

Premises used: Int.natCast_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
⊢ fract (HDiv.hDiv (α := k) (↑(↑m₀ : ℤ) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑m₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)

Tactic:
exact this (natCast_nonneg m₀)

Premises used: Int.natCast_nonneg
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
⊢ 0 ≤ m₁

Tactic:
simpa [m₁, ← @cast_le k, ← div_le_iff₀ hn] using FloorRing.gc_ceil_coe.le_u_l _

Premises used: div_le_iff₀, Int.cast_le, FloorRing.gc_ceil_coe, GaloisConnection.le_u_l
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
⊢ 0 ≤ m₁

Tactic:
have hm₁ : 0 ≤ m₁ := by
    simpa [m₁, ← @cast_le k, ← div_le_iff₀ hn] using FloorRing.gc_ceil_coe.le_u_l _
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
⊢ fract (HDiv.hDiv (α := k) (↑(-(↑m₀ : ℤ)) : k) (↑n : k)) = fract (HDiv.hDiv (α := k) (-(↑m₀ : k)) (↑n : k))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
⊢ fract (HDiv.hDiv (α := k) (-(↑m₀ : k)) (↑n : k)) = fract (HDiv.hDiv (α := k) (↑m₁ : k) (↑n : k))

Tactic:
?_
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
⊢ fract (HDiv.hDiv (α := k) (↑m₁ : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m₁ % (↑n : ℤ)) : k) (↑n : k)

Tactic:
this hm₁
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
⊢ HDiv.hDiv (α := k) (↑(m₁ % (↑n : ℤ)) : k) (↑n : k) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)

Tactic:
?_
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
inr : fract (HDiv.hDiv (α := k) (-(↑m₀ : k)) (↑n : k)) = fract (HDiv.hDiv (α := k) (↑m₁ : k) (↑n : k))
inr₁ :
  HDiv.hDiv (α := k) (↑(m₁ % (↑n : ℤ)) : k) (↑n : k) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)
⊢ fract (HDiv.hDiv (α := k) (↑(-(↑m₀ : ℤ)) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)

Tactic:
calc
    fract ((Int.cast (-(m₀ : ℤ)) : k) / (n : k))
      = fract (-(m₀ : k) / n) := by simp
    _ = fract ((m₁ : k) / n) := ?_
    _ = Int.cast (m₁ % (n : ℤ)) / Nat.cast n := this hm₁
    _ = Int.cast (-(↑m₀ : ℤ) % ↑n) / Nat.cast n := ?_

Premises used: Int.cast, Int.fract, HDiv.hDiv, Nat.cast, HMod.hMod, Neg.neg
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
inr :
  fract ((HMul.hMul (α := k) (↑q : k) (↑n : k) - (↑m₀ : k)) / (↑n : k)) = fract (HDiv.hDiv (α := k) (↑m₁ : k) (↑n : k))
⊢ fract (HDiv.hDiv (α := k) (-(↑m₀ : k)) (↑n : k)) = fract (HDiv.hDiv (α := k) (↑m₁ : k) (↑n : k))

Tactic:
rw [← fract_intCast_add q, ← mul_div_cancel_right₀ (q : k) hn.ne', ← add_div, ← sub_eq_add_neg]

Premises used: Int.fract_intCast_add, Int.cast, sub_eq_add_neg, LT.lt.ne', mul_div_cancel_right₀, add_div
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
⊢ fract ((HMul.hMul (α := k) (↑q : k) (↑n : k) - (↑m₀ : k)) / (↑n : k)) = fract (HDiv.hDiv (α := k) (↑m₁ : k) (↑n : k))

Tactic:
simp [m₁]
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
inr : m₁ % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
⊢ HDiv.hDiv (α := k) (↑(m₁ % (↑n : ℤ)) : k) (↑n : k) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)

Tactic:
congr 2
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
inr : (q * (↑n : ℤ) - (↑m₀ : ℤ)) % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
⊢ m₁ % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)

Tactic:
simp only [m₁]
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
n : ℕ
hn : LT.lt.{u_4} (α := k) 0 (↑n : k)
this :
  ∀ {l : ℤ}, 0 ≤ l → fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
m₀ : ℕ
q : ℤ := ⌈HDiv.hDiv (α := k) (↑m₀ : k) (↑n : k)⌉
m₁ : ℤ := q * (↑n : ℤ) - (↑m₀ : ℤ)
hm₁ : 0 ≤ m₁
inr : (q * (↑n : ℤ) + -(↑m₀ : ℤ)) % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
inr₁ : (-(↑m₀ : ℤ) + q * (↑n : ℤ)) % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
inr₂ inr₃ : HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
⊢ (q * (↑n : ℤ) - (↑m₀ : ℤ)) % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)

Tactic:
rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self_right]

Premises used: HMul.hMul, sub_eq_add_neg, add_comm, Int.add_mul_emod_self_right
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : (↑(z - 1) : R) < a ↔ HSub.hSub (α := R) (↑z : R) 1 < a
⊢ z ≤ ⌈a⌉ ↔ HSub.hSub (α := R) (↑z : R) 1 < a

Tactic:
rw [← sub_one_lt_iff, lt_ceil]

Premises used: Int.lt_ceil, Int.sub_one_lt_iff
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑(z - 1) : R) < a ↔ (↑(z - 1) : R) < a
⊢ (↑(z - 1) : R) < a ↔ HSub.hSub (α := R) (↑z : R) 1 < a

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : a ≤ (↑(z - 1) : R) ↔ a ≤ HSub.hSub (α := R) (↑z : R) 1
⊢ ⌈a⌉ < z ↔ a ≤ HSub.hSub (α := R) (↑z : R) 1

Tactic:
rw [← le_sub_one_iff, ceil_le]

Premises used: Int.le_sub_one_iff, Int.ceil_le
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a ≤ (↑(z - 1) : R) ↔ a ≤ (↑(z - 1) : R)
⊢ a ≤ (↑(z - 1) : R) ↔ a ≤ HSub.hSub (α := R) (↑z : R) 1

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : z + 1 ≤ ⌈a⌉ ↔ z < ⌈a⌉
rw₁ rw₂ : z < ⌈a⌉ ↔ z < ⌈a⌉
⊢ z + 1 ≤ ⌈a⌉ ↔ (↑z : R) < a

Tactic:
rw [← lt_ceil, add_one_le_iff]

Premises used: Int.lt_ceil, Int.add_one_le_iff
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ 1 ≤ ⌈a⌉ ↔ 0 < a

Tactic:
simpa using le_ceil_iff (z := 1)

Premises used: Int.le_ceil_iff
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
rw : a ≤ HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1
⊢ ⌈a⌉ ≤ ⌊a⌋ + 1

Tactic:
rw [ceil_le, Int.cast_add, Int.cast_one]

Premises used: Int.cast_add, Int.ceil_le, Int.cast_one
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ a ≤ HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1

Tactic:
(lt_floor_add_one a).le

Premises used: Int.lt_floor_add_one, LT.lt.le
-- Module: Mathlib.Algebra.Order.Floor.Ring
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ a ≤ HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1

Tactic:
exact (lt_floor_add_one a).le

Premises used: Int.lt_floor_add_one, LT.lt.le