Theorem: MvPolynomial.rTensorAlgHom_coeff_tmul (DividedPowers/ForMathlib/RingTheory/TensorProduct/MvPolynomial.lean)

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

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

State before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
        (algebraMap (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))) (1 ⊗ₜ[R] n)) =
    coeff d p ⊗ₜ[R] n
Tactic:
rw [algebraMap_eq, mul_comm, coeff_C_mul]
State after:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ 1 ⊗ₜ[R] n * coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft) p) = coeff d p ⊗ₜ[R] n

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