Theorem: Polynomial.discConv_discConv (LeanCamCombi/DiscreteDeriv.lean)

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
v w : AddMonoidAlgebra S R
P : R[X]
⊢ discConv v (discConv w P) = discConv (v * w) P
Tactic:
simp [discConv]
State after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
v w : AddMonoidAlgebra S R
P : R[X]
⊢ (Finsupp.sum v fun r s => s • (Finsupp.sum w fun r s => s • P.comp (X + C r)).comp (X + C r)) =
    Finsupp.sum (v * w) fun r s => s • P.comp (X + C r)

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
v w : AddMonoidAlgebra S R
P : R[X]
⊢ (Finsupp.sum v fun r s => s • (Finsupp.sum w fun r s => s • P.comp (X + C r)).comp (X + C r)) =
    Finsupp.sum (v * w) fun r s => s • P.comp (X + C r)
Tactic:
sorry
State after:
no goals