-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
lemma aeval_sumElim_pderiv_inl {S τ : Type*} [CommRing S] [Algebra R S]
    (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (j : σ) :
    aeval (Sum.elim X (C ∘ f)) ((pderiv (Sum.inl j)) p) =
      (pderiv j) ((aeval (Sum.elim X (C ∘ f))) p)

Proof state:
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
j : σ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
induction' p using MvPolynomial.induction_on with a p q hp hq p q h

Result:
case h_C
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
a : R
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) (C a)) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) (C a))

case h_add
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p q : MvPolynomial (σ ⊕ τ) R
hp : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
hq : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) q) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) q)
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) (p + q)) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) (p + q))

case h_X
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
q : σ ⊕ τ
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) (p * X q)) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X q))

Proof state:
case h_add
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p q : MvPolynomial (σ ⊕ τ) R
hp : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
hq : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) q) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) q)
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) (p + q)) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) (p + q))

Tactic:
simp [hp, hq]

Result:
no goals

Proof state:
case h_C
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
a : R
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) (C a)) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) (C a))

Tactic:
simp

Result:
no goals

Proof state:
case h_X
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
q : σ ⊕ τ
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) (p * X q)) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X q))

Tactic:
simp only [Derivation.leibniz, pderiv_X, smul_eq_mul, map_add, map_mul, aeval_X, h]

Result:
case h_X
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
q : σ ⊕ τ
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 q) +
      Sum.elim X (⇑C ∘ f) q * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) q) +
      Sum.elim X (⇑C ∘ f) q * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Proof state:
case h_X
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
q : σ ⊕ τ
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 q) +
      Sum.elim X (⇑C ∘ f) q * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) q) +
      Sum.elim X (⇑C ∘ f) q * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
cases q <;> simp [Pi.single_apply]

Result:
no goals