Theorem: IMOSL.IMO2006A1.f_alt_formula (IMOSLLean4/IMO2006/A1/A1.lean)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ (↑⌊r⌋ - 1) * f r - ↑⌊r⌋ ^ 2 = ↑⌊r⌋ * ((↑⌊r⌋ - 1) * r - ↑⌊r⌋ ^ 2)
Tactic:
rw [sq, f, Int.fract, mul_sub, mul_sub, sub_sub, ← add_one_mul (α := R), sub_add_cancel,
  mul_sub, sub_left_inj, ← mul_assoc, sub_one_mul, ← mul_sub_one, mul_assoc]
State after:
no goals