Theorem: PolynomialMap.componentIsHomogeneous (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✝ p : ℕ
f : M →ₚ[R] N
⊢ IsHomogeneousOfDegree p (component p f)
Tactic:
intro S _ _ s sm
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
⊢ (component p f).toFun' S (s • sm) = s ^ p • (component p f).toFun' S 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
⊢ (component p f).toFun' S (s • sm) = s ^ p • (component p f).toFun' S sm
Tactic:
dsimp [component]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p

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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Tactic:
let ψ := ((aeval (R := S) (monomial 1 s : S[X])).restrictScalars R)
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p

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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Tactic:
suffices  (rTensor M ((monomial 1).restrictScalars R)) (s • sm)
    = (rTensor M ψ.toLinearMap) (rTensor M ((monomial 1).restrictScalars R) sm) by
  rw [this, ← f.isCompat_apply' ψ]
  generalize toFun' f S[X] (rTensor M ((monomial 1).restrictScalars R) sm) = t
  rw [rTensor_apply, rTensor_apply, ← rTensor_comp_apply]
  conv_rhs =>
    rw [← (IsLinearMap.isLinearMap_smul (s ^ p)).mk'_apply, ← coe_restrictScalars R,
      ← LinearMap.comp_apply]
  apply LinearMap.congr_fun
  apply symm
  dsimp only [LinearMap.rTensor, TensorProduct.map]
  apply TensorProduct.lift.unique
  intro f n
  simp only [compl₂_id, coe_comp, coe_restrictScalars, Function.comp_apply, lift.tmul,
    lcoeff_apply, mk_apply, IsLinearMap.mk'_apply, AlgHom.toLinearMap_apply,
    AlgHom.coe_restrictScalars', TensorProduct.smul_tmul']
  apply congr_arg₂ _ _ rfl
  induction f using Polynomial.induction_on' with
  | h_add f g hf hg => rw [coeff_add, smul_add, hf, hg, ← coeff_add, map_add]
  | h_monomial n a =>
      simp only [ψ, aeval_monomial, ← smul_eq_mul, algebraMap_smul, coeff_smul, monomial_pow,
        one_mul, coeff_monomial]
      split_ifs with h
      . rw [smul_eq_mul, mul_comm, h, AlgHom.coe_restrictScalars', aeval_monomial, monomial_pow,
          one_mul, ← C_eq_algebraMap]
        simp only [C_mul_monomial, coeff_monomial, if_pos]
      . simp only [smul_zero, AlgHom.coe_restrictScalars', aeval_monomial, ← C_eq_algebraMap,
          monomial_pow, one_mul, C_mul_monomial, coeff_monomial, if_neg h]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
Tactic:
.  suffices ∀ (sm : S ⊗[R] M), s • sm =
      rTensor M (((IsLinearMap.isLinearMap_smul s).mk').restrictScalars R) sm by
    simp only [this, ← rTensor_comp_apply]
    apply LinearMap.congr_fun
    apply congr_arg
    rw [LinearMap.ext_iff]
    intro r
    simp only [compl₂_id, smul_eq_mul, lift.tmul, coe_comp, coe_restrictScalars,
      Function.comp_apply, IsLinearMap.mk'_apply, mk_apply, AlgHom.toLinearMap_apply,
      AlgHom.coe_restrictScalars', aeval_monomial, pow_one]
    rw [mul_comm]
    simp only [AlgHom.coe_restrictScalars', aeval_monomial, pow_one, ψ, ← smul_eq_mul,
      algebraMap_smul, Polynomial.smul_monomial]
  intro sm
  rw [← (IsLinearMap.isLinearMap_smul s).mk'_apply, ← LinearMap.coe_restrictScalars R]
  apply LinearMap.congr_fun
  dsimp only [LinearMap.rTensor, TensorProduct.map, smul_eq_mul]
  apply lift.unique
  intro r m
  simp only [coe_restrictScalars, IsLinearMap.mk'_apply, compl₂_id, coe_comp, Function.comp_apply,
    mk_apply, smul_tmul', smul_eq_mul]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Tactic:
rw [this, ← f.isCompat_apply' ψ]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ ((Polynomial.rTensor R N S)
        ((LinearMap.rTensor N ψ.toLinearMap) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))))
      p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p

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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ ((Polynomial.rTensor R N S)
        ((LinearMap.rTensor N ψ.toLinearMap) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))))
      p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Tactic:
generalize toFun' f S[X] (rTensor M ((monomial 1).restrictScalars R) sm) = t
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ((Polynomial.rTensor R N S) ((LinearMap.rTensor N ψ.toLinearMap) t)) p = s ^ p • ((Polynomial.rTensor R N S) t) p

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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ((Polynomial.rTensor R N S) ((LinearMap.rTensor N ψ.toLinearMap) t)) p = s ^ p • ((Polynomial.rTensor R N S) t) p
Tactic:
rw [rTensor_apply, rTensor_apply, ← rTensor_comp_apply]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ (LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)) t = s ^ p • (LinearMap.rTensor N (↑R (lcoeff S p))) t

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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ (LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)) t = s ^ p • (LinearMap.rTensor N (↑R (lcoeff S p))) t
Tactic:
conv_rhs =>
  rw [← (IsLinearMap.isLinearMap_smul (s ^ p)).mk'_apply, ← coe_restrictScalars R,
    ← LinearMap.comp_apply]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ (LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)) t =
    (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p))) t

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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ (LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)) t =
    (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p))) t
Tactic:
apply LinearMap.congr_fun
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) =
    ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p))

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) =
    ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p))
Tactic:
apply symm
State after:
case h.a
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p)) =
    LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)

State before:
case h.a
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p)) =
    LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)
Tactic:
dsimp only [LinearMap.rTensor, TensorProduct.map]
State after:
case h.a
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
      lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)) =
    lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)

State before:
case h.a
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
      lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)) =
    lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)
Tactic:
apply TensorProduct.lift.unique
State after:
case h.a.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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ∀ (x : S[X]) (y : N),
    (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
          lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)))
        (x ⊗ₜ[R] y) =
      (((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) x) y

State before:
case h.a.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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ∀ (x : S[X]) (y : N),
    (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
          lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)))
        (x ⊗ₜ[R] y) =
      (((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) x) y
Tactic:
intro f n
State after:
case h.a.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✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
        lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)))
      (f ⊗ₜ[R] n) =
    (((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) f) n

State before:
case h.a.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✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
        lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)))
      (f ⊗ₜ[R] n) =
    (((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) f) n
Tactic:
simp only [compl₂_id, coe_comp, coe_restrictScalars, Function.comp_apply, lift.tmul,
  lcoeff_apply, mk_apply, IsLinearMap.mk'_apply, AlgHom.toLinearMap_apply,
  AlgHom.coe_restrictScalars', TensorProduct.smul_tmul']
State after:
case h.a.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✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ (s ^ p • f.coeff p) ⊗ₜ[R] n = (ψ f).coeff p ⊗ₜ[R] n

State before:
case h.a.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✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ (s ^ p • f.coeff p) ⊗ₜ[R] n = (ψ f).coeff p ⊗ₜ[R] n
Tactic:
apply congr_arg₂ _ _ rfl
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✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ s ^ p • f.coeff p = (ψ f).coeff p

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✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ s ^ p • f.coeff p = (ψ f).coeff p
Tactic:
induction f using Polynomial.induction_on' with
| h_add f g hf hg => rw [coeff_add, smul_add, hf, hg, ← coeff_add, map_add]
| h_monomial n a =>
    simp only [ψ, aeval_monomial, ← smul_eq_mul, algebraMap_smul, coeff_smul, monomial_pow,
      one_mul, coeff_monomial]
    split_ifs with h
    . rw [smul_eq_mul, mul_comm, h, AlgHom.coe_restrictScalars', aeval_monomial, monomial_pow,
        one_mul, ← C_eq_algebraMap]
      simp only [C_mul_monomial, coeff_monomial, if_pos]
    . simp only [smul_zero, AlgHom.coe_restrictScalars', aeval_monomial, ← C_eq_algebraMap,
        monomial_pow, one_mul, C_mul_monomial, coeff_monomial, if_neg h]
State after:
no goals

State before:
case h_add
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✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n : N
f g : S[X]
hf : s ^ p • f.coeff p = (ψ f).coeff p
hg : s ^ p • g.coeff p = (ψ g).coeff p
⊢ s ^ p • (f + g).coeff p = (ψ (f + g)).coeff p
Tactic:
rw [coeff_add, smul_add, hf, hg, ← coeff_add, map_add]
State after:
no goals

State before:
case h_monomial
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
⊢ s ^ p • ((monomial n) a).coeff p = (ψ ((monomial n) a)).coeff p
Tactic:
simp only [ψ, aeval_monomial, ← smul_eq_mul, algebraMap_smul, coeff_smul, monomial_pow,
  one_mul, coeff_monomial]
State after:
case h_monomial
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
⊢ (s ^ p • if n = p then a else 0) = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p

State before:
case h_monomial
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
⊢ (s ^ p • if n = p then a else 0) = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
split_ifs with h
State after:
case pos
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ s ^ p • a = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p

case neg
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p

State before:
case pos
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ s ^ p • a = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p

case neg
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
. rw [smul_eq_mul, mul_comm, h, AlgHom.coe_restrictScalars', aeval_monomial, monomial_pow,
    one_mul, ← C_eq_algebraMap]
  simp only [C_mul_monomial, coeff_monomial, if_pos]
State after:
case neg
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p

State before:
case neg
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
. simp only [smul_zero, AlgHom.coe_restrictScalars', aeval_monomial, ← C_eq_algebraMap,
    monomial_pow, one_mul, C_mul_monomial, coeff_monomial, if_neg h]
State after:
no goals

State before:
case pos
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ s ^ p • a = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
rw [smul_eq_mul, mul_comm, h, AlgHom.coe_restrictScalars', aeval_monomial, monomial_pow,
  one_mul, ← C_eq_algebraMap]
State after:
case pos
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ a * s ^ p = (C a * (monomial p) (s ^ p)).coeff p

State before:
case pos
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ a * s ^ p = (C a * (monomial p) (s ^ p)).coeff p
Tactic:
simp only [C_mul_monomial, coeff_monomial, if_pos]
State after:
no goals

State before:
case neg
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
simp only [smul_zero, AlgHom.coe_restrictScalars', aeval_monomial, ← C_eq_algebraMap,
  monomial_pow, one_mul, C_mul_monomial, coeff_monomial, if_neg h]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
Tactic:
suffices ∀ (sm : S ⊗[R] M), s • sm =
    rTensor M (((IsLinearMap.isLinearMap_smul s).mk').restrictScalars R) sm by
  simp only [this, ← rTensor_comp_apply]
  apply LinearMap.congr_fun
  apply congr_arg
  rw [LinearMap.ext_iff]
  intro r
  simp only [compl₂_id, smul_eq_mul, lift.tmul, coe_comp, coe_restrictScalars,
    Function.comp_apply, IsLinearMap.mk'_apply, mk_apply, AlgHom.toLinearMap_apply,
    AlgHom.coe_restrictScalars', aeval_monomial, pow_one]
  rw [mul_comm]
  simp only [AlgHom.coe_restrictScalars', aeval_monomial, pow_one, ψ, ← smul_eq_mul,
    algebraMap_smul, Polynomial.smul_monomial]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
Tactic:
intro sm
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
Tactic:
rw [← (IsLinearMap.isLinearMap_smul s).mk'_apply, ← LinearMap.coe_restrictScalars R]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
Tactic:
apply LinearMap.congr_fun
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) = LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) = LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))
Tactic:
dsimp only [LinearMap.rTensor, TensorProduct.map, smul_eq_mul]
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) =
    lift ((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯))

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) =
    lift ((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯))
Tactic:
apply lift.unique
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ∀ (x : S) (y : M),
    (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) (x ⊗ₜ[R] y) =
      (((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯)) x) y

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ∀ (x : S) (y : M),
    (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) (x ⊗ₜ[R] y) =
      (((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯)) x) y
Tactic:
intro r m
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
r : S
m : M
⊢ (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) (r ⊗ₜ[R] m) =
    (((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯)) r) m

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
r : S
m : M
⊢ (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) (r ⊗ₜ[R] m) =
    (((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯)) r) m
Tactic:
simp only [coe_restrictScalars, IsLinearMap.mk'_apply, compl₂_id, coe_comp, Function.comp_apply,
  mk_apply, smul_tmul', smul_eq_mul]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
Tactic:
simp only [this, ← rTensor_comp_apply]
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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ (LinearMap.rTensor M (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm =
    (LinearMap.rTensor M (ψ.toLinearMap ∘ₗ ↑R (monomial 1))) 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ (LinearMap.rTensor M (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm =
    (LinearMap.rTensor M (ψ.toLinearMap ∘ₗ ↑R (monomial 1))) sm
Tactic:
apply LinearMap.congr_fun
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ LinearMap.rTensor M (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) =
    LinearMap.rTensor M (ψ.toLinearMap ∘ₗ ↑R (monomial 1))

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ LinearMap.rTensor M (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) =
    LinearMap.rTensor M (ψ.toLinearMap ∘ₗ ↑R (monomial 1))
Tactic:
apply congr_arg
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ ↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) = ψ.toLinearMap ∘ₗ ↑R (monomial 1)

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ ↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) = ψ.toLinearMap ∘ₗ ↑R (monomial 1)
Tactic:
rw [LinearMap.ext_iff]
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ ∀ (x : S), (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) x = (ψ.toLinearMap ∘ₗ ↑R (monomial 1)) x

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ ∀ (x : S), (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) x = (ψ.toLinearMap ∘ₗ ↑R (monomial 1)) x
Tactic:
intro r
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) r = (ψ.toLinearMap ∘ₗ ↑R (monomial 1)) r

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) r = (ψ.toLinearMap ∘ₗ ↑R (monomial 1)) r
Tactic:
simp only [compl₂_id, smul_eq_mul, lift.tmul, coe_comp, coe_restrictScalars,
  Function.comp_apply, IsLinearMap.mk'_apply, mk_apply, AlgHom.toLinearMap_apply,
  AlgHom.coe_restrictScalars', aeval_monomial, pow_one]
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (monomial 1) (s * r) = ψ ((monomial 1) r)

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (monomial 1) (s * r) = ψ ((monomial 1) r)
Tactic:
rw [mul_comm]
State after:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (monomial 1) (r * s) = ψ ((monomial 1) r)

State before:
case 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✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (monomial 1) (r * s) = ψ ((monomial 1) r)
Tactic:
simp only [AlgHom.coe_restrictScalars', aeval_monomial, pow_one, ψ, ← smul_eq_mul,
  algebraMap_smul, Polynomial.smul_monomial]
State after:
no goals