Theorem: φ_apply (DividedPowers/DPAlgebra/RobyLemma9.lean)

State before:
R : Type u_4
inst✝¹⁰ : CommRing R
S : Type u_3
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ (φ R S M N) (m ⊗ₜ[R] n) = m ⊗ₜ[S] n
Tactic:
simp only [φ, productMap_apply_tmul, AlgHom.coe_restrictScalars', includeLeft_apply,
  includeRight_apply, tmul_mul_tmul, _root_.mul_one, _root_.one_mul]
State after:
no goals