no goals
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ mulLeft R a ^ n = mulLeft R (a ^ n)
simpa only [mulLeft, ← Algebra.coe_lmul_eq_mul] using ((Algebra.lmul R A).map_pow a n).symm