no goals
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ ↑f (a * ↑(algebraMap R A) r) = ↑f a * ↑(algebraMap R B) r
rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]