Theorem: IMOSL.IMO2010A1.MonoidGood.fract_eq_eps_mul_floor (IMOSLLean4/IMO2010/A1/A1Monoid.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf : MonoidGood f
h : ⌊f 1⌋ = 1
x : M
⊢ Int.fract (f x) = Int.fract (f 1) * ↑⌊f x⌋
Tactic:
rw [Int.fract, Int.fract, h, Int.cast_one, sub_one_mul, ← map_eq_map_one_mul_floor hf]
State after:
no goals