-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
τ : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
q : σ ⊕ τ
h :
  Eq (α := MvPolynomial σ S)
    ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
        ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) p) :
      MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          p) :
      MvPolynomial σ S)
mul_X :
  ∀ (val : σ),
    HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
          ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p :
            MvPolynomial σ S)
          ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              (Pi.single (M := fun (x : σ ⊕ τ) ↦ MvPolynomial (σ ⊕ τ) R) (Sum.inl j)
                (1 : (fun (x : σ ⊕ τ) ↦ MvPolynomial (σ ⊕ τ) R) (Sum.inl j)) (Sum.inl val)) :
            MvPolynomial σ S) +
        HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
          (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f) (Sum.inl val))
          ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
              ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                  (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
                p) :
            MvPolynomial σ S) =
      HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
          ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p :
            MvPolynomial σ S)
          ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
              (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f) (Sum.inl val)) :
            MvPolynomial σ S) +
        HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
          (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f) (Sum.inl val))
          ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
              ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                  (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
                p) :
            MvPolynomial σ S)
⊢ HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            p :
          MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (Pi.single (M := fun (x : σ ⊕ τ) ↦ MvPolynomial (σ ⊕ τ) R) (Sum.inl j)
              (1 : (fun (x : σ ⊕ τ) ↦ MvPolynomial (σ ⊕ τ) R) (Sum.inl j)) q) :
          MvPolynomial σ S) +
      HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f) q)
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p) :
          MvPolynomial σ S) =
    HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            p :
          MvPolynomial σ S)
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f) q) :
          MvPolynomial σ S) +
      HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f) q)
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p) :
          MvPolynomial σ S)
have mul_X₁ : ∀ (val : τ),
  HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            p :
          MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (Pi.single (M := fun (x : σ ⊕ τ) ↦ MvPolynomial (σ ⊕ τ) R) (Sum.inl j)
              (1 : (fun (x : σ ⊕ τ) ↦ MvPolynomial (σ ⊕ τ) R) (Sum.inl j)) (Sum.inr val)) :
          MvPolynomial σ S) +
      HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f) (Sum.inr val))
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p) :
          MvPolynomial σ S) =
    HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            p :
          MvPolynomial σ S)
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f) (Sum.inr val)) :
          MvPolynomial σ S) +
      HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f) (Sum.inr val))
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p) :
          MvPolynomial σ S)
Tactic: cases q
Cleared hypotheses: q