no goals
R : Type u
S : Type v
A : Type w
B : Type ?u.321762
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
α : Type u_1
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ a • ↑(algebraMap R A) r = ↑(algebraMap R A) r
rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]