no goals
α : Type ?u.325438
R✝ : Type ?u.325441
k : Type ?u.325444
S : Type ?u.325447
M : Type ?u.325450
M₂ : Type ?u.325453
M₃ : Type ?u.325456
ι : Type ?u.325459
R : Type u_1
inst✝ : Semiring R
m : ℕ
⊢ m • 1 = ↑m
rw [nsmul_eq_mul, mul_one]