Theorem: PolynomialMap.recompose_component (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
⊢ (lfsum fun p => component p f) = f
Tactic:
ext S _ _ sm
State after:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (lfsum fun p => component p f).toFun' S sm = f.toFun' S sm

State before:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (lfsum fun p => component p f).toFun' S sm = f.toFun' S sm
Tactic:
rw [lfsum_eq (LocFinsupp_component f), LocFinsupp_component_eq]
State after:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    f.toFun' S sm

State before:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    f.toFun' S sm
Tactic:
have hsm : sm = ((aeval 1).restrictScalars R).toLinearMap.rTensor M
  (((monomial 1).restrictScalars R).rTensor M sm) := by
  rw [← LinearMap.rTensor_comp_apply, LinearMap.rTensor, eq_comm]
  convert DFunLike.congr_fun TensorProduct.map_id sm
  ext s
  simp only [coe_comp, coe_restrictScalars, Function.comp_apply, AlgHom.toLinearMap_apply,
    AlgHom.coe_restrictScalars', aeval_monomial, Algebra.id.map_eq_id, RingHom.id_apply, pow_one,
    mul_one, id_coe, id_eq]
State after:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    f.toFun' S sm

State before:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    f.toFun' S sm
Tactic:
conv_rhs => rw [hsm, ← f.isCompat_apply']
State after:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    (LinearMap.rTensor N (AlgHom.restrictScalars R (aeval 1)).toLinearMap)
      (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))

State before:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    (LinearMap.rTensor N (AlgHom.restrictScalars R (aeval 1)).toLinearMap)
      (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))
Tactic:
generalize f.toFun' S[X] (((monomial 1).restrictScalars R).rTensor M sm) = sn
State after:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
⊢ (((Polynomial.rTensor R N S) sn).sum fun x m => m) =
    (LinearMap.rTensor N (AlgHom.restrictScalars R (aeval 1)).toLinearMap) sn

State before:
case toFun'.h.h.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
⊢ (((Polynomial.rTensor R N S) sn).sum fun x m => m) =
    (LinearMap.rTensor N (AlgHom.restrictScalars R (aeval 1)).toLinearMap) sn
Tactic:
convert rTensor'_sum (R := R) (fun _ ↦ 1) sn
State after:
case h.e'_2.h.e'_7.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝² : CommRing S
x✝¹ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
x✝ : S ⊗[R] N
⊢ x✝ = 1 • x✝

case h.e'_3.h.e'_5.h.e'_12.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap = Polynomial.lsum fun n => ↑R ((lsmul S S) 1)

State before:
case h.e'_2.h.e'_7.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝² : CommRing S
x✝¹ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
x✝ : S ⊗[R] N
⊢ x✝ = 1 • x✝

case h.e'_3.h.e'_5.h.e'_12.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap = Polynomial.lsum fun n => ↑R ((lsmul S S) 1)
Tactic:
simp only [_root_.one_smul]
State after:
case h.e'_3.h.e'_5.h.e'_12.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap = Polynomial.lsum fun n => ↑R ((lsmul S S) 1)

State before:
case h.e'_3.h.e'_5.h.e'_12.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap = Polynomial.lsum fun n => ↑R ((lsmul S S) 1)
Tactic:
ext p
State after:
case h.e'_3.h.e'_5.h.e'_12.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap p = (Polynomial.lsum fun n => ↑R ((lsmul S S) 1)) p

State before:
case h.e'_3.h.e'_5.h.e'_12.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap p = (Polynomial.lsum fun n => ↑R ((lsmul S S) 1)) p
Tactic:
simp only [AlgHom.toLinearMap_apply, AlgHom.coe_restrictScalars', coe_aeval_eq_eval,
  Polynomial.lsum_apply, coe_restrictScalars, lsmul_apply, smul_eq_mul, one_mul, eval_eq_sum]
State after:
case h.e'_3.h.e'_5.h.e'_12.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (p.sum fun e a => a * 1 ^ e) = p.sum fun x x => x

State before:
case h.e'_3.h.e'_5.h.e'_12.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (p.sum fun e a => a * 1 ^ e) = p.sum fun x x => x
Tactic:
apply congr_arg₂ _ rfl
State after:
case h.e'_3.h.e'_5.h.e'_12.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (fun e a => a * 1 ^ e) = fun x x => x

State before:
case h.e'_3.h.e'_5.h.e'_12.h.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (fun e a => a * 1 ^ e) = fun x x => x
Tactic:
simp only [one_pow, mul_one]
State after:
no goals

State before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
Tactic:
rw [← LinearMap.rTensor_comp_apply, LinearMap.rTensor, eq_comm]
State after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (TensorProduct.map ((AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1)) LinearMap.id) sm = sm

State before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (TensorProduct.map ((AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1)) LinearMap.id) sm = sm
Tactic:
convert DFunLike.congr_fun TensorProduct.map_id sm
State after:
case h.e'_2.h.e'_5.h.e'_15
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1) = LinearMap.id

State before:
case h.e'_2.h.e'_5.h.e'_15
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1) = LinearMap.id
Tactic:
ext s
State after:
case h.e'_2.h.e'_5.h.e'_15.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
s : S
⊢ ((AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1)) s = LinearMap.id s

State before:
case h.e'_2.h.e'_5.h.e'_15.h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
s : S
⊢ ((AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1)) s = LinearMap.id s
Tactic:
simp only [coe_comp, coe_restrictScalars, Function.comp_apply, AlgHom.toLinearMap_apply,
  AlgHom.coe_restrictScalars', aeval_monomial, Algebra.id.map_eq_id, RingHom.id_apply, pow_one,
  mul_one, id_coe, id_eq]
State after:
no goals