awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
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 :
  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)
⊢ 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)

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

Premises used: MvPolynomial.aeval_X, MvPolynomial.pderiv_X, map_add, Derivation.leibniz, map_mul, smul_eq_mul
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
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
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)
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)

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
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
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)
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:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
a : R
⊢ Eq (α := MvPolynomial σ (MvPolynomial ι R))
    ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
          ((C : (a : R) → MvPolynomial (σ ⊕ ι) R) a)) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R)
          ((C : (a : R) → MvPolynomial (σ ⊕ ι) R) a)) :
      MvPolynomial σ (MvPolynomial ι R))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p q : MvPolynomial (σ ⊕ ι) R
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))
h_1 :
  Eq (α := MvPolynomial σ (MvPolynomial ι R))
    ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) q) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) q) :
      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 + q)) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) (p + q)) :
      MvPolynomial σ (MvPolynomial ι R))

Tactic:
simp_all
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
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))
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))
⊢ 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))

Tactic:
cases n
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p : MvPolynomial (σ ⊕ ι) R
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))
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:
simp_all [pderiv_X, Pi.single_apply, apply_ite]

Premises used: Pi.single_apply, MvPolynomial.pderiv_X, apply_ite
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p : MvPolynomial (σ ⊕ ι) R
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))
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:
simp_all [pderiv_X, Pi.single_apply, apply_ite]

Premises used: Pi.single_apply, MvPolynomial.pderiv_X, apply_ite
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
S : Type u_2
σ : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
x : S
f : RingHom.{u_1, u_2} R (Polynomial S)
g : σ → Polynomial S
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Polynomial.eval x (eval₂ f g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) =
      eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s))
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add :
  ∀ (p q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) =
          eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) (p + q)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) (p * X n)
⊢ Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) p

Tactic:
apply induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
S : Type u_2
σ : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
x : S
f : RingHom.{u_1, u_2} R (Polynomial S)
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (a : R),
    Polynomial.eval x (eval₂ f g ((C : (a : R) → MvPolynomial σ R) a)) =
      eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s))
        ((C : (a : R) → MvPolynomial σ R) a)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
S : Type u_2
σ : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
x : S
f : RingHom.{u_1, u_2} R (Polynomial S)
g : σ → Polynomial S
p_1 p q : MvPolynomial σ R
hp :
  Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) p
hq :
  Polynomial.eval x (eval₂ f g q) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) q
⊢ Polynomial.eval x (eval₂ f g (p + q)) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) (p + q)

Tactic:
simp [hp, hq]
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
S : Type u_2
σ : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
x : S
f : RingHom.{u_1, u_2} R (Polynomial S)
g : σ → Polynomial S
p_1 p : MvPolynomial σ R
n : σ
hp :
  Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) p
⊢ Polynomial.eval x (eval₂ f g (p * X n)) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) (p * X n)

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
simp :
  eval₂ (RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C)))
      (fun (s : Fin (n + 1)) ↦
        (eval x : (a : MvPolynomial (Fin n) R) → R)
          (Polynomial.eval q
            (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
              (fun (k : Fin n) ↦
                (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
              s)))
      f =
    (eval fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i :
        (a : MvPolynomial (Fin (n + 1)) R) → R)
      f
⊢ Eq (α := R)
    ((eval x : (a : MvPolynomial (Fin n) R) → R)
        (Polynomial.eval q
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) f)) :
      R)
    ((eval fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        f :
      R)

Tactic:
simp only [finSuccEquiv_apply, coe_eval₂Hom, polynomial_eval_eval₂, eval_eval₂]

Premises used: MvPolynomial.eval_eval₂, MvPolynomial.coe_eval₂Hom, MvPolynomial.finSuccEquiv_apply, MvPolynomial.polynomial_eval_eval₂
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C)) = RingHom.id R

Tactic:
@RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_

Premises used: RingHom.ext
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
refine :
  ∀ (r : R),
    Eq (α := R)
      ((RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C)) : (a : R) → R) r :
        R)
      ((RingHom.id R : (a : R) → R) r : R)
| RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C))

Tactic:
refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_

Premises used: RingHom.ext
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
r : R
simp : r
⊢ Eq (α := R)
    ((RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C)) : (a : R) → R) r :
      R)
    ((RingHom.id R : (a : R) → R) r : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
refine : ∀ (r : R), r
| RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C))

Tactic:
refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
    simp

Premises used: RingHom.ext
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
conv :
  eval₂ (RingHom.id R)
      (fun (s : Fin (n + 1)) ↦
        (eval x : (a : MvPolynomial (Fin n) R) → R)
          (Polynomial.eval q
            (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
              (fun (k : Fin n) ↦
                (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
              s)))
      f =
    (eval fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i :
        (a : MvPolynomial (Fin (n + 1)) R) → R)
      f
⊢ eval₂ (RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C)))
      (fun (s : Fin (n + 1)) ↦
        (eval x : (a : MvPolynomial (Fin n) R) → R)
          (Polynomial.eval q
            (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
              (fun (k : Fin n) ↦
                (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
              s)))
      f =
    (eval fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i :
        (a : MvPolynomial (Fin (n + 1)) R) → R)
      f

Tactic:
conv in RingHom.comp _ _ =>
    refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
    simp

Premises used: RingHom.ext, RingHom.comp