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

State before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
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 ⊗ₜ[S] n) = (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Tactic:
simp only [ψ, ψLeft, ψRight, AlgHom.toRingHom_eq_coe, productMap_apply_tmul, AlgHom.coe_mk,
  RingHom.coe_coe, AlgHom.coe_comp, AlgHom.coe_restrictScalars', Ideal.Quotient.mkₐ_eq_mk,
  Function.comp_apply, includeLeft_apply, includeRight_apply]
State after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
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
⊢ (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] 1) * (Ideal.Quotient.mk (kerφ R S M N)) (1 ⊗ₜ[R] n) =
    (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)

State before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
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
⊢ (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] 1) * (Ideal.Quotient.mk (kerφ R S M N)) (1 ⊗ₜ[R] n) =
    (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Tactic:
rw [← RingHom.map_mul]
State after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
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
⊢ (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] 1 * 1 ⊗ₜ[R] n) = (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)

State before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
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
⊢ (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] 1 * 1 ⊗ₜ[R] n) = (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Tactic:
simp only [tmul_mul_tmul, _root_.mul_one, _root_.one_mul]
State after:
no goals