awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
p : MvPolynomial (σ ⊕ ι) R
i : σ
⊢ 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))
have C : ∀ (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: induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q _ _ => simp_all
  | mul_X p n _ => cases n <;> simp_all [pderiv_X, Pi.single_apply, apply_ite]
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
p : MvPolynomial (σ ⊕ ι) R
i : σ
C :
  ∀ (a : R),
    Eq (α := MvPolynomial σ (MvPolynomial ι R))
      ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
          ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
            ((MvPolynomial.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)
            ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ ι) R) a)) :
        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) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) p) :
      MvPolynomial σ (MvPolynomial ι R))
have add : ∀ (p q : MvPolynomial (σ ⊕ ι) R),
  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)) 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: induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q _ _ => simp_all
  | mul_X p n _ => cases n <;> simp_all [pderiv_X, Pi.single_apply, apply_ite]
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
p : MvPolynomial (σ ⊕ ι) R
i : σ
⊢ 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))
have C : ∀ (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: classical
  induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q _ _ => simp_all
  | mul_X p n _ => cases n <;> simp_all [pderiv_X, Pi.single_apply, apply_ite]
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
p : MvPolynomial (σ ⊕ ι) R
i : σ
C :
  ∀ (a : R),
    Eq (α := MvPolynomial σ (MvPolynomial ι R))
      ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
          ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
            ((MvPolynomial.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)
            ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ ι) R) a)) :
        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) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) p) :
      MvPolynomial σ (MvPolynomial ι R))
have add : ∀ (p q : MvPolynomial (σ ⊕ ι) R),
  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)) 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: classical
  induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q _ _ => simp_all
  | mul_X p n _ => cases n <;> simp_all [pderiv_X, Pi.single_apply, apply_ite]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
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
⊢ Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) p
have C : ∀ (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: apply induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
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)
⊢ Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) p
have 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)
Tactic: apply induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
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)
⊢ Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun (s : σ) ↦ Polynomial.eval x (g s)) p
have 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)
Tactic: apply induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ 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)
have 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
Tactic: simp only [finSuccEquiv_apply, coe_eval₂Hom, polynomial_eval_eval₂, eval_eval₂]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
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))
have 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)
Tactic: refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
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
⊢ 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)
have simp : r
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
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))
have refine : ∀ (r : R), r
Tactic: refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
    simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ 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
have 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
Tactic: conv in RingHom.comp _ _ =>
    refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
    simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ 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
have simp : Eq (α := R)
  ((eval 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)) :
        (a : MvPolynomial (Fin (n + 1)) R) → 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 [eval₂_id]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ Eq (α := R)
    ((eval 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)) :
          (a : MvPolynomial (Fin (n + 1)) R) → 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)
have e_a : Eq.{u_1 + 1} (α := Fin (n + 1) → 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)))
  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
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Polynomial (goal)
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ Eq.{u_1 + 1} (α := Fin (n + 1) → 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)))
    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
have e_a : ∀ (i : Fin (n + 1)),
  Eq (α := R)
    ((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))
            i)) :
      R)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i : R)
Tactic: funext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial α R)
    ((rename g : (a : MvPolynomial τ R) → MvPolynomial α R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial α R)
    ((rename (g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p : MvPolynomial α R)
have simp_rw : Eq (α := MvPolynomial α R)
  ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g) : (a : MvPolynomial τ R) → MvPolynomial α R)
      (eval₂ C (X ∘ f) p) :
    MvPolynomial α R)
  ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p :
    MvPolynomial α R)
Tactic: simp_rw [aeval_def, algebraMap_eq, rename, aeval_eq_eval₂Hom]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g) : (a : MvPolynomial τ R) → MvPolynomial α R)
        (eval₂ C (X ∘ f) p) :
      MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p :
      MvPolynomial α R)
have rw : Eq (α := MvPolynomial α R)
  (eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C)
    (comp (β := MvPolynomial τ R)
      (⇑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) : (a : MvPolynomial τ R) → MvPolynomial α R) (X ∘ f))
    p)
  ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p)
Tactic: rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial α R)
    (eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C)
      (comp (β := MvPolynomial τ R)
        (⇑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) : (a : MvPolynomial τ R) → MvPolynomial α R) (X ∘ f))
      p)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p)
have simp : Eq (α := MvPolynomial α R)
  (eval₂ (RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C)
      (fun (x : σ) ↦ X (g (f x))) p :
    MvPolynomial α R)
  ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : σ) ↦ X (g (f x)) : (a : MvPolynomial σ R) → MvPolynomial α R)
      p :
    MvPolynomial α R)
Tactic: simp only [comp_def, eval₂Hom_X']