no goals
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra S B
inst✝ : Algebra R A
h : ∀ (x : R), ↑(algebraMap R A) x = ↑(algebraMap S A) (↑(algebraMap R S) x)
x : R
y : S
z : A
⊢ (x • y) • z = x • y • z
simp_rw [Algebra.smul_def, RingHom.map_mul, mul_assoc, h]