-- Mathlib/Algebra/Order/Floor.lean
theorem fract_div_intCast_eq_div_intCast_mod {m : ℤ} {n : ℕ} :
    fract ((m : k) / n) = ↑(m % n) / n

Proof state:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

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

Result:
case inr.intro.inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑↑m₀ / ↑n) = ↑(↑m₀ % ↑n) / ↑n

case inr.intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Proof state:
case inr.intro.inr.calc_2.e_a.e_a
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ (q * ↑n - ↑m₀) % ↑n = -↑m₀ % ↑n

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

Result:
no goals

Proof state:
case intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : l₀ = 0
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n

Tactic:
simp [hl]

Result:
no goals

Proof state:
case intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ -↑l₀
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n

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

Result:
case intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : l₀ = 0
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n

Proof state:
case inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
⊢ fract (↑m / ↑0) = ↑(m % ↑0) / ↑0

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l : ℤ
hl : 0 ≤ l
⊢ fract (↑l / ↑n) = ↑(l % ↑n) / ↑n

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

Result:
case intro.inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ ↑l₀
⊢ fract (↑↑l₀ / ↑n) = ↑(↑l₀ % ↑n) / ↑n

case intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ -↑l₀
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n

Proof state:
case inr.intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
have hm₁ : 0 ≤ m₁ := by
  simpa [m₁, ← @cast_le k, ← div_le_iff₀ hn] using FloorRing.gc_ceil_coe.le_u_l _

Result:
case inr.intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Proof state:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : n > 0
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Tactic:
replace hn : 0 < (n : k) := by norm_cast

Result:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
⊢ 0 ≤ m₁

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

Result:
no goals

Proof state:
case inr.intro.inr.calc_1
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (-↑m₀ / ↑n) = fract (↑m₁ / ↑n)

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

Result:
case inr.intro.inr.calc_1
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract ((↑q * ↑n - ↑m₀) / ↑n) = fract (↑m₁ / ↑n)

Proof state:
case inr.intro.inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑↑m₀ / ↑n) = ↑(↑m₀ % ↑n) / ↑n

Tactic:
exact this (ofNat_nonneg m₀)

Result:
no goals

Proof state:
case inr.intro.inr.calc_1
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract ((↑q * ↑n - ↑m₀) / ↑n) = fract (↑m₁ / ↑n)

Tactic:
simp [m₁]

Result:
no goals

Proof state:
case inr.intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
let m₁ := q * ↑n - (↑m₀ : ℤ)

Result:
case inr.intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Proof state:
case intro.inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ ↑l₀
⊢ fract (↑↑l₀ / ↑n) = ↑(↑l₀ % ↑n) / ↑n

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

Result:
no goals

Proof state:
case inr.intro.inr.calc_2
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ ↑(m₁ % ↑n) / ↑n = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
congr 2

Result:
case inr.intro.inr.calc_2.e_a.e_a
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ m₁ % ↑n = -↑m₀ % ↑n

Proof state:
case inr.intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
let q := ⌈↑m₀ / (n : k)⌉

Result:
case inr.intro.inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n