α : Type ?u.158540
R : Type ?u.158543
k : Type ?u.158546
S : Type ?u.158549
M : Type u_1
M₂ : Type ?u.158555
M₃ : Type ?u.158558
ι : Type ?u.158561
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
h : Module ℤ M
n : ℤ
x : M
⊢ SMul.smul n x = n • x
α : Type ?u.158540
R : Type ?u.158543
k : Type ?u.158546
S : Type ?u.158549
M : Type u_1
M₂ : Type ?u.158555
M₃ : Type ?u.158558
ι : Type ?u.158561
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
h : Module ℤ M
n : ℤ
x : M
⊢ SMul.smul n x = n • x
rw [zsmul_eq_smul_cast ℤ n x, Int.cast_id]
no goals
α : Type ?u.158540
R : Type ?u.158543
k : Type ?u.158546
S : Type ?u.158549
M : Type u_1
M₂ : Type ?u.158555
M₃ : Type ?u.158558
ι : Type ?u.158561
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
h : Module ℤ M
n : ℤ
x : M
⊢ SMul.smul n x = n • x
rfl