awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
k : Type u_4
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsOrderedRing k
inst_3 : FloorRing k
m : ℤ
n : ℕ
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % (↑n : ℤ)) : k) (↑n : k)
have inl : fract (HDiv.hDiv (α := k) (↑m : k) (↑0 : k)) = HDiv.hDiv (α := k) (↑(m % (↑0 : ℤ)) : k) (↑0 : k)
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % (↑n : ℤ)) : k) (↑n : k)
have inr : ∀ (hn : n > 0), 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)
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
have norm_cast : 0 < n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
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
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % (↑n : ℤ)) : k) (↑n : k)
have hn₁ : LT.lt.{u_4} (α := k) 0 (↑n : k)
Tactic: replace hn : 0 < (n : k) := by norm_cast
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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
⊢ fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
have 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)
Tactic: obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ fract (HDiv.hDiv (α := k) (↑l : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l % (↑n : ℤ)) : k) (↑n : k)
have 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)
Tactic: obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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₀ : ℤ)
⊢ fract (HDiv.hDiv (α := k) (↑(↑l₀ : ℤ) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑l₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)
have inl : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ fract (HDiv.hDiv (α := k) (↑(↑l₀ : ℤ) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑l₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)
have inl₁ : fract (HDiv.hDiv (α := k) (↑l₀ : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(↑(l₀ % n) : ℤ) : k) (↑n : k)
Tactic: rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ fract (HDiv.hDiv (α := k) (↑(↑l₀ : ℤ) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑l₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)
have inl₂ : fract (HDiv.hDiv (α := k) (↑l₀ : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(l₀ % n) : k) (↑n : k)
Tactic: rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ fract (HDiv.hDiv (α := k) (↑(↑l₀ : ℤ) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑l₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)
have inl₃ : HDiv.hDiv (α := k) (↑(l₀ % n) : k) (↑n : k) = HDiv.hDiv (α := k) (↑(l₀ % n) : k) (↑n : k)
Tactic: rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
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₀ : ℤ))
⊢ fract (HDiv.hDiv (α := k) (↑(-(↑l₀ : ℤ)) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑l₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)
have hl₁ : l₀ = 0
Tactic: rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
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)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % (↑n : ℤ)) : k) (↑n : k)
have this : ∀ {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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % (↑n : ℤ)) : k) (↑n : k)
have inr : ∀ (m₀ : ℕ),
  fract (HDiv.hDiv (α := k) (↑(↑m₀ : ℤ) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (↑m₀ : ℤ) (↑n : ℤ)) : k) (↑n : k)
Tactic: obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
⊢ fract (HDiv.hDiv (α := k) (↑m : k) (↑n : k)) = HDiv.hDiv (α := k) (↑(m % (↑n : ℤ)) : k) (↑n : k)
have inr₁ : ∀ (m₀ : ℕ),
  fract (HDiv.hDiv (α := k) (↑(-(↑m₀ : ℤ)) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)
Tactic: obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (hypothesis)
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₀ : ℤ)
⊢ fract (HDiv.hDiv (α := k) (↑(-(↑m₀ : ℤ)) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)
have hm₁ : 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 _
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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) (↑(HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)
have inr : fract (HDiv.hDiv (α := k) (-(↑m₀ : k)) (↑n : k)) = fract (HDiv.hDiv (α := k) (↑m₁ : 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 := ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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))
⊢ fract (HDiv.hDiv (α := k) (↑(-(↑m₀ : ℤ)) : k) (↑n : k)) =
    HDiv.hDiv (α := k) (↑(HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)) : k) (↑n : k)
have inr₁ : HDiv.hDiv (α := k) (↑(m₁ % (↑n : ℤ)) : 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 := ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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))
have inr : fract ((HMul.hMul (α := k) (↑q : k) (↑n : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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)
have inr : m₁ % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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₁
⊢ (q * (↑n : ℤ) - (↑m₀ : ℤ)) % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
have inr : (q * (↑n : ℤ) + -(↑m₀ : ℤ)) % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
Tactic: rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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 : ℤ)
⊢ (q * (↑n : ℤ) - (↑m₀ : ℤ)) % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
have inr₁ : (-(↑m₀ : ℤ) + q * (↑n : ℤ)) % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
Tactic: rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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 : ℤ)
⊢ (q * (↑n : ℤ) - (↑m₀ : ℤ)) % (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
have inr₂ : HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ) = HMod.hMod (α := ℤ) (-(↑m₀ : ℤ)) (↑n : ℤ)
Tactic: rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ z ≤ ⌈a⌉ ↔ HSub.hSub (α := R) (↑z : R) 1 < a
have rw : (↑(z - 1) : R) < a ↔ HSub.hSub (α := R) (↑z : R) 1 < a
Tactic: rw [← sub_one_lt_iff, lt_ceil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ (↑(z - 1) : R) < a ↔ HSub.hSub (α := R) (↑z : R) 1 < a
have norm_cast : (↑(z - 1) : R) < a ↔ (↑(z - 1) : R) < a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ ⌈a⌉ < z ↔ a ≤ HSub.hSub (α := R) (↑z : R) 1
have rw : a ≤ (↑(z - 1) : R) ↔ a ≤ HSub.hSub (α := R) (↑z : R) 1
Tactic: rw [← le_sub_one_iff, ceil_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ a ≤ (↑(z - 1) : R) ↔ a ≤ HSub.hSub (α := R) (↑z : R) 1
have norm_cast : a ≤ (↑(z - 1) : R) ↔ a ≤ (↑(z - 1) : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ z + 1 ≤ ⌈a⌉ ↔ (↑z : R) < a
have rw : z + 1 ≤ ⌈a⌉ ↔ z < ⌈a⌉
Tactic: rw [← lt_ceil, add_one_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
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⌉
⊢ z + 1 ≤ ⌈a⌉ ↔ (↑z : R) < a
have rw₁ : z < ⌈a⌉ ↔ z < ⌈a⌉
Tactic: rw [← lt_ceil, add_one_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ ⌈a⌉ ≤ ⌊a⌋ + 1
have rw : a ≤ HAdd.hAdd (α := R) (↑⌊a⌋ : R) 1
Tactic: rw [ceil_le, Int.cast_add, Int.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
ha : -1 < a
⊢ 0 ≤ ⌈a⌉
have rwa : HSub.hSub (α := R) (↑0 : R) 1 < a
Tactic: rwa [Int.le_ceil_iff, Int.cast_zero, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
ha : -1 < a
rwa : HSub.hSub (α := R) (↑0 : R) 1 < a
⊢ 0 ≤ ⌈a⌉
have rwa₁ : HSub.hSub (α := R) 0 1 < a
Tactic: rwa [Int.le_ceil_iff, Int.cast_zero, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ a ≤ (↑z : R)
have rw : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ ⌈a⌉ ≤ z
Tactic: rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ ⌈a⌉ ≤ z
⊢ ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ a ≤ (↑z : R)
have rw₁ : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) (↑1 : R) < a ∧ ⌈a⌉ ≤ z
Tactic: rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ ⌈a⌉ ≤ z
rw₁ : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) (↑1 : R) < a ∧ ⌈a⌉ ≤ z
⊢ ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ a ≤ (↑z : R)
have rw₂ : ⌈a⌉ = z ↔ (↑(z - 1) : R) < a ∧ ⌈a⌉ ≤ z
Tactic: rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ ⌈a⌉ ≤ z
rw₁ : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) (↑1 : R) < a ∧ ⌈a⌉ ≤ z
rw₂ : ⌈a⌉ = z ↔ (↑(z - 1) : R) < a ∧ ⌈a⌉ ≤ z
⊢ ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ a ≤ (↑z : R)
have rw₃ : ⌈a⌉ = z ↔ z - 1 < ⌈a⌉ ∧ ⌈a⌉ ≤ z
Tactic: rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ ⌈a⌉ ≤ z
rw₁ : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) (↑1 : R) < a ∧ ⌈a⌉ ≤ z
rw₂ : ⌈a⌉ = z ↔ (↑(z - 1) : R) < a ∧ ⌈a⌉ ≤ z
rw₃ : ⌈a⌉ = z ↔ z - 1 < ⌈a⌉ ∧ ⌈a⌉ ≤ z
⊢ ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ a ≤ (↑z : R)
have rw₄ : ⌈a⌉ = z ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
Tactic: rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ ⌈a⌉ ≤ z
rw₁ : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) (↑1 : R) < a ∧ ⌈a⌉ ≤ z
rw₂ : ⌈a⌉ = z ↔ (↑(z - 1) : R) < a ∧ ⌈a⌉ ≤ z
rw₃ : ⌈a⌉ = z ↔ z - 1 < ⌈a⌉ ∧ ⌈a⌉ ≤ z
rw₄ : ⌈a⌉ = z ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
⊢ ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ a ≤ (↑z : R)
have rw₅ : ⌈a⌉ ≤ z ∧ z ≤ ⌈a⌉ ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
Tactic: rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ ⌈a⌉ ≤ z
rw₁ : ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) (↑1 : R) < a ∧ ⌈a⌉ ≤ z
rw₂ : ⌈a⌉ = z ↔ (↑(z - 1) : R) < a ∧ ⌈a⌉ ≤ z
rw₃ : ⌈a⌉ = z ↔ z - 1 < ⌈a⌉ ∧ ⌈a⌉ ≤ z
rw₄ : ⌈a⌉ = z ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
rw₅ : ⌈a⌉ ≤ z ∧ z ≤ ⌈a⌉ ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
⊢ ⌈a⌉ = z ↔ HSub.hSub (α := R) (↑z : R) 1 < a ∧ a ≤ (↑z : R)
have rw₆ : z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
Tactic: rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
⊢ z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉
have rw : z ≤ ⌊-a⌋ ↔ ⌈a⌉ ≤ -z
Tactic: rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
rw : z ≤ ⌊-a⌋ ↔ ⌈a⌉ ≤ -z
⊢ z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉
have rw₁ : z ≤ ⌊-a⌋ ↔ a ≤ (↑(-z) : R)
Tactic: rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
rw : z ≤ ⌊-a⌋ ↔ ⌈a⌉ ≤ -z
rw₁ : z ≤ ⌊-a⌋ ↔ a ≤ (↑(-z) : R)
⊢ z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉
have rw₂ : (↑z : R) ≤ -a ↔ a ≤ (↑(-z) : R)
Tactic: rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
rw : z ≤ ⌊-a⌋ ↔ ⌈a⌉ ≤ -z
rw₁ : z ≤ ⌊-a⌋ ↔ a ≤ (↑(-z) : R)
rw₂ : (↑z : R) ≤ -a ↔ a ≤ (↑(-z) : R)
⊢ z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉
have rw₃ : (↑z : R) ≤ -a ↔ a ≤ -(↑z : R)
Tactic: rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
rw : z ≤ ⌊-a⌋ ↔ ⌈a⌉ ≤ -z
rw₁ : z ≤ ⌊-a⌋ ↔ a ≤ (↑(-z) : R)
rw₂ : (↑z : R) ≤ -a ↔ a ≤ (↑(-z) : R)
rw₃ : (↑z : R) ≤ -a ↔ a ≤ -(↑z : R)
⊢ z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉
have rw₄ : a ≤ -(↑z : R) ↔ a ≤ -(↑z : R)
Tactic: rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z
have rw : ⌈-a⌉ ≤ z ↔ -z ≤ ⌊a⌋
Tactic: rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
inst_3 : IsOrderedRing R
z : ℤ
rw : ⌈-a⌉ ≤ z ↔ -z ≤ ⌊a⌋
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z
have rw₁ : -a ≤ (↑z : R) ↔ -z ≤ ⌊a⌋
Tactic: rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]