Theorem: DividedPowerAlgebra.AlgHom.baseChange_tmul (DividedPowers/DPAlgebra/BaseChange.lean)

State before:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
φ : B →ₐ[R] C
a : A
b : B
⊢ (baseChange φ) (a ⊗ₜ[R] b) = a • φ b
Tactic:
simp only [baseChange, toRingHom_eq_coe, coe_mk, RingHom.coe_coe, productMap_apply_tmul,
  IsScalarTower.coe_toAlgHom', ← smul_eq_mul, algebraMap_smul]
State after:
no goals