[GOAL]
R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
src✝ : ZMod n →+* R := castHom h R
a : ZMod n
r : (fun x => R) a
⊢ ↑a * r = r * ↑a
[PROOFSTEP]
rcases ZMod.int_cast_surjective a with ⟨k, rfl⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
src✝ : ZMod n →+* R := castHom h R
k : ℤ
r : R
⊢ ↑↑k * r = r * ↑↑k
[PROOFSTEP]
show ZMod.castHom h R k * r = r * ZMod.castHom h R k
[GOAL]
case intro
R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
src✝ : ZMod n →+* R := castHom h R
k : ℤ
r : R
⊢ ↑(castHom h R) ↑k * r = r * ↑(castHom h R) ↑k
[PROOFSTEP]
rw [map_intCast]
[GOAL]
case intro
R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
src✝ : ZMod n →+* R := castHom h R
k : ℤ
r : R
⊢ ↑k * r = r * ↑k
[PROOFSTEP]
exact Commute.cast_int_left r k
