α : Type ?u.280330
R : Type u_2
k : Type ?u.280336
S : Type ?u.280339
M✝ : Type ?u.280342
M₂ : Type ?u.280345
M₃ : Type ?u.280348
ι : Type ?u.280351
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R M✝
M : Type u_1
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n
α : Type ?u.280330
R : Type u_2
k : Type ?u.280336
S : Type ?u.280339
M✝ : Type ?u.280342
M₂ : Type ?u.280345
M₃ : Type ?u.280348
ι : Type ?u.280351
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R M✝
M : Type u_1
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
⊢ CharZero R
refine' ⟨fun m n h => @Nat.cast_injective M _ _ _ _ _⟩
no goals
α : Type ?u.280330
R : Type u_2
k : Type ?u.280336
S : Type ?u.280339
M✝ : Type ?u.280342
M₂ : Type ?u.280345
M₃ : Type ?u.280348
ι : Type ?u.280351
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R M✝
M : Type u_1
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n
rw [← nsmul_one, ← nsmul_one, nsmul_eq_smul_cast R m (1 : M), nsmul_eq_smul_cast R n (1 : M), h]