awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h :
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X a)) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X a)) :
      MvPolynomial τ R)
have mul_X : HAdd.hAdd (α := MvPolynomial τ R)
    (if a = x then (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p else 0 : MvPolynomial τ R)
    (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
        MvPolynomial τ R)) =
  HAdd.hAdd (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (if a = x then p else 0) : MvPolynomial τ R)
    (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
        MvPolynomial τ R))
Tactic: simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
      Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h :
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
⊢ HAdd.hAdd (α := MvPolynomial τ R)
      (if a = x then (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p else 0 : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R)) =
    HAdd.hAdd (α := MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (if a = x then p else 0) : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R))
have pos : a = x →
  HAdd.hAdd (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R)) =
    HAdd.hAdd (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h :
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
pos :
  a = x →
    HAdd.hAdd (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
        (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
              ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
            MvPolynomial τ R)) =
      HAdd.hAdd (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
        (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
              ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
            MvPolynomial τ R))
⊢ HAdd.hAdd (α := MvPolynomial τ R)
      (if a = x then (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p else 0 : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R)) =
    HAdd.hAdd (α := MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (if a = x then p else 0) : MvPolynomial τ R)
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R))
have neg : ¬a = x →
  0 +
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R) =
    (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) 0 +
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) (X (f a))
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
have C : ∀ (a : R),
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)
Tactic: induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q hp hq => simp [hp, hq]
  | mul_X p a h =>
    simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
      Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add]
    split_ifs <;> simp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial τ R)
      ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
have add : ∀ (p q : MvPolynomial σ R)
  (hp :
    Eq (α := MvPolynomial τ R)
      ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
        MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
        MvPolynomial τ R))
  (hq :
    Eq (α := MvPolynomial τ R)
      ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q) :
        MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q) :
        MvPolynomial τ R)),
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q)) :
      MvPolynomial τ R)
Tactic: induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q hp hq => simp [hp, hq]
  | mul_X p a h =>
    simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
      Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add]
    split_ifs <;> simp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
have C : ∀ (a : R),
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)
Tactic: classical
  induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q hp hq => simp [hp, hq]
  | mul_X p a h =>
    simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
      Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add]
    split_ifs <;> simp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial τ R)
      ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
have add : ∀ (p q : MvPolynomial σ R)
  (hp :
    Eq (α := MvPolynomial τ R)
      ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
        MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
        MvPolynomial τ R))
  (hq :
    Eq (α := MvPolynomial τ R)
      ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q) :
        MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q) :
        MvPolynomial τ R)),
  Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q)) :
      MvPolynomial τ R)
Tactic: classical
  induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q hp hq => simp [hp, hq]
  | mul_X p a h =>
    simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
      Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add]
    split_ifs <;> simp
Cleared hypotheses: p
-- 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)
⊢ 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 * X q)) :
      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 * X q)) :
      MvPolynomial σ S)
have mul_X : 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)
Tactic: simp only [Derivation.leibniz, pderiv_X, smul_eq_mul, map_add, map_mul, aeval_X, h]
-- 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
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
j : σ
⊢ 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)
have C : ∀ (a : R),
  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)
          ((C : (a : R) → MvPolynomial (σ ⊕ τ) R) a)) :
      MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          ((C : (a : R) → MvPolynomial (σ ⊕ τ) R) a)) :
      MvPolynomial σ S)
Tactic: induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q hp hq => simp [hp, hq]
  | mul_X p q h =>
    simp only [Derivation.leibniz, pderiv_X, smul_eq_mul, map_add, map_mul, aeval_X, h]
    cases q <;> simp [Pi.single_apply]
Cleared hypotheses: p
-- 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
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
j : σ
⊢ 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)
have C : ∀ (a : R),
  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)
          ((C : (a : R) → MvPolynomial (σ ⊕ τ) R) a)) :
      MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          ((C : (a : R) → MvPolynomial (σ ⊕ τ) R) a)) :
      MvPolynomial σ S)
Tactic: classical
  induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q hp hq => simp [hp, hq]
  | mul_X p q h =>
    simp only [Derivation.leibniz, pderiv_X, smul_eq_mul, map_add, map_mul, aeval_X, h]
    cases q <;> simp [Pi.single_apply]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p : MvPolynomial (σ ⊕ ι) R
n : σ ⊕ ι
h :
  Eq (α := MvPolynomial σ (MvPolynomial ι R))
    ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) p) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) p) :
      MvPolynomial σ (MvPolynomial ι R))
⊢ Eq (α := MvPolynomial σ (MvPolynomial ι R))
    ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) (p * X n)) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) (p * X n)) :
      MvPolynomial σ (MvPolynomial ι R))
have mul_X : ∀ (val : σ),
  Eq (α := MvPolynomial σ (MvPolynomial ι R))
    ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) (p * X (Sum.inl val))) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) (p * X (Sum.inl val))) :
      MvPolynomial σ (MvPolynomial ι R))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p : MvPolynomial (σ ⊕ ι) R
n : σ ⊕ ι
h :
  Eq (α := MvPolynomial σ (MvPolynomial ι R))
    ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) p) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) p) :
      MvPolynomial σ (MvPolynomial ι R))
mul_X :
  ∀ (val : σ),
    Eq (α := MvPolynomial σ (MvPolynomial ι R))
      ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
          ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) (p * X (Sum.inl val))) :
        MvPolynomial σ (MvPolynomial ι R))
      ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
          ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) (p * X (Sum.inl val))) :
        MvPolynomial σ (MvPolynomial ι R))
⊢ Eq (α := MvPolynomial σ (MvPolynomial ι R))
    ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) (p * X n)) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) (p * X n)) :
      MvPolynomial σ (MvPolynomial ι R))
have mul_X₁ : ∀ (val : ι),
  Eq (α := MvPolynomial σ (MvPolynomial ι R))
    ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) (p * X (Sum.inr val))) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) (p * X (Sum.inr val))) :
      MvPolynomial σ (MvPolynomial ι R))
Tactic: cases n
Cleared hypotheses: n