Theorem: MvPolynomial.rTensorAlgHom_toLinearMap (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
⊢ rTensorAlgHom.toLinearMap = ↑(finsuppLeft' R S N (σ →₀ ℕ) S)
Tactic:
ext d n e
State after:
case a.h.h.h.a
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
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap ∘ₗ monomial d) 1) n) =
    coeff e (((AlgebraTensorModule.curry ↑(finsuppLeft' R S N (σ →₀ ℕ) S) ∘ₗ monomial d) 1) n)

State before:
case a.h.h.h.a
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
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap ∘ₗ monomial d) 1) n) =
    coeff e (((AlgebraTensorModule.curry ↑(finsuppLeft' R S N (σ →₀ ℕ) S) ∘ₗ monomial d) 1) n)
Tactic:
simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
  LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply]
State after:
case a.h.h.h.a
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
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (rTensorAlgHom ((monomial d) 1 ⊗ₜ[R] n)) = coeff e (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n))

State before:
case a.h.h.h.a
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
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (rTensorAlgHom ((monomial d) 1 ⊗ₜ[R] n)) = coeff e (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n))
Tactic:
rw [rTensorAlgHom_coeff_tmul]
State after:
case a.h.h.h.a
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
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e ((monomial d) 1) ⊗ₜ[R] n = coeff e (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n))

State before:
case a.h.h.h.a
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
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e ((monomial d) 1) ⊗ₜ[R] n = coeff e (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n))
Tactic:
simp only [coeff]
State after:
case a.h.h.h.a
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
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ ((monomial d) 1) e ⊗ₜ[R] n = (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n)) e

State before:
case a.h.h.h.a
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
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ ((monomial d) 1) e ⊗ₜ[R] n = (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n)) e
Tactic:
erw [finsuppLeft_apply_tmul_apply]
State after:
no goals