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

State before:
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℤ
m n : M
⊢ (fun x => ↑(φ x)) (m * n) = (fun x => ↑(φ x)) m * ↑⌊(fun x => ↑(φ x)) n⌋
Tactic:
rw [Int.floor_intCast, ← Int.cast_mul, ← φ.map_mul]
State after:
no goals