no goals
R : Type u
S : Type v
A : Type w
B : Type ?u.275396
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
r : R
y : A
⊢ x * (↑(algebraMap R A) r * y) = ↑(algebraMap R A) r * (x * y)
rw [← mul_assoc, ← commutes, mul_assoc]