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

Proof state:
case inr.refine_2
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑(m % n) / ↑n < 1

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

Result:
no goals

Proof state:
case inr.refine_3
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)

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

Result:
case inr.refine_3
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑n * ↑(↑m / ↑n)

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
⊢ fract (↑m / ↑n) = ↑(m % n) / ↑n

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

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

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

Proof state:
case inr.refine_3
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑(n * (m / n))

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

Result:
no goals

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:
have hn' : 0 < (n : k) := by
  norm_cast

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

Proof state:
case inr.refine_3
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑n * ↑(↑m / ↑n)

Tactic:
norm_cast

Result:
case inr.refine_3
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑(n * (m / 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 : n > 0
⊢ 0 < ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
case inr.refine_1
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ 0 ≤ ↑(m % n) / ↑n

Tactic:
positivity

Result:
no goals

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

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

Result:
case inr.refine_1
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ 0 ≤ ↑(m % n) / ↑n

case inr.refine_2
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑(m % n) / ↑n < 1

case inr.refine_3
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)