u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : ℕ
b : R
⊢ a • b = ↑a * b
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : ℕ
a' b c : R
x✝¹ : ↑a = a'
x✝ : a' * b = c
⊢ a • b = c
subst_vars
no goals
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : ℕ
b : R
⊢ a • b = ↑a * b
simp