Theorem: DividedPowerAlgebra.dpScalarExtension_apply_dp (DividedPowers/DPAlgebra/BaseChange.lean)

State before:
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
r : R
n : ℕ
m : M
⊢ (dpScalarExtension A R M) ((r ^ n) ⊗ₜ[A] dp A n m) = dp R n (r ⊗ₜ[A] m)
Tactic:
rw [dpScalarExtension, AlgHom.baseChange_tmul, lift'AlgHom_apply_dp, ← dp_smul, smul_tmul',
  smul_eq_mul, mul_one]
State after:
no goals