Theorem: Polynomial.rTensorAlgHom_coeff_apply_tmul (DividedPowers/ForMathlib/RingTheory/TensorProduct/Polynomial.lean)

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((rTensorAlgHom R N S) (p ⊗ₜ[R] n)).coeff d = p.coeff d ⊗ₜ[R] n
Tactic:
rw [rTensorAlgHom, Algebra.TensorProduct.lift_tmul]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
          ((IsScalarTower.toAlgHom R (S ⊗[R] N) (S ⊗[R] N)[X]).comp Algebra.TensorProduct.includeRight) n).coeff
      d =
    p.coeff d ⊗ₜ[R] n

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
          ((IsScalarTower.toAlgHom R (S ⊗[R] N) (S ⊗[R] N)[X]).comp Algebra.TensorProduct.includeRight) n).coeff
      d =
    p.coeff d ⊗ₜ[R] n
Tactic:
rw [AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Function.comp_apply,
  Algebra.TensorProduct.includeRight_apply]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((mapAlgHom Algebra.TensorProduct.includeLeft) p * (algebraMap (S ⊗[R] N) (S ⊗[R] N)[X]) (1 ⊗ₜ[R] n)).coeff d =
    p.coeff d ⊗ₜ[R] n

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((mapAlgHom Algebra.TensorProduct.includeLeft) p * (algebraMap (S ⊗[R] N) (S ⊗[R] N)[X]) (1 ⊗ₜ[R] n)).coeff d =
    p.coeff d ⊗ₜ[R] n
Tactic:
rw [← C_eq_algebraMap, mul_comm, coeff_C_mul]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ 1 ⊗ₜ[R] n * ((mapAlgHom Algebra.TensorProduct.includeLeft) p).coeff d = p.coeff d ⊗ₜ[R] n

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ 1 ⊗ₜ[R] n * ((mapAlgHom Algebra.TensorProduct.includeLeft) p).coeff d = p.coeff d ⊗ₜ[R] n
Tactic:
simp [mapAlgHom, coeff_map]
State after:
no goals