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

State before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
s : S
m : M
⊢ (dpScalarExtensionInv R S M) (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
rw [dpScalarExtensionInv, dividedPowerAlgebra_exponentialModule_equiv_symm_apply]
State after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
s : S
m : M
⊢ (PowerSeries.coeff (S ⊗[R] DividedPowerAlgebra R M) n) ↑((dpScalarExtensionExp R S M) (s ⊗ₜ[R] m)) =
    (s ^ n) ⊗ₜ[R] dp R n m

State before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
s : S
m : M
⊢ (PowerSeries.coeff (S ⊗[R] DividedPowerAlgebra R M) n) ↑((dpScalarExtensionExp R S M) (s ⊗ₜ[R] m)) =
    (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
simp only [dpScalarExtensionExp, LinearMap.baseChangeEquiv, LinearEquiv.coe_symm_mk,
  AlgebraTensorModule.lift_apply, lift.tmul, LinearMap.coe_restrictScalars, LinearMap.flip_apply,
  LinearMap.lsmul_apply, LinearMap.smul_apply, LinearMap.coe_comp, Function.comp_apply]
State after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
s : S
m : M
⊢ (PowerSeries.coeff (S ⊗[R] DividedPowerAlgebra R M) n)
      ↑(s • (ExponentialModule.linearMap Algebra.TensorProduct.includeRight) ((exp_LinearMap R M) m)) =
    (s ^ n) ⊗ₜ[R] dp R n m

State before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
s : S
m : M
⊢ (PowerSeries.coeff (S ⊗[R] DividedPowerAlgebra R M) n)
      ↑(s • (ExponentialModule.linearMap Algebra.TensorProduct.includeRight) ((exp_LinearMap R M) m)) =
    (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
rw [ExponentialModule.coe_smul, PowerSeries.coeff_scale, ExponentialModule.coeff_linearMap,
  Algebra.TensorProduct.includeRight, coe_mk, RingHom.coe_mk, MonoidHom.coe_mk,
  OneHom.coe_mk, coeff_exp_LinearMap, smul_tmul', smul_eq_mul, mul_one]
State after:
no goals