no goals
R : Type u
S : Type v
A : Type w
B : Type ?u.296946
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 = x * y * ↑(algebraMap R A) r
rw [mul_assoc, commutes, ← mul_assoc]