awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
rw :
  Eq (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
      (MvPolynomial (Fin n) R)[X])
    (((↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        p :
      (MvPolynomial (Fin n) R)[X])
rw₁ rw₂ :
  Eq (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
      (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
      (MvPolynomial (Fin n) R)[X])
⊢ Eq (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
      (MvPolynomial (Fin n) R)[X])
    ((eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
              (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        p :
      (MvPolynomial (Fin n) R)[X])

Tactic:
rw [← finSuccEquiv_eq, RingHom.coe_coe]

Premises used: RingHom.coe_coe, MvPolynomial.finSuccEquiv_eq
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
⊢ RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →+* MvPolynomial (Fin n.succ) R)
      (RingHom.comp Polynomial.C C) =
    C

Tactic:
RingHom.ext fun x => ?_

Premises used: RingHom.ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
refine :
  ∀ (x : R),
    Eq (α := MvPolynomial (Fin n.succ) R)
      ((RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →+* MvPolynomial (Fin n.succ) R)
              (RingHom.comp Polynomial.C C) :
            (a : R) → MvPolynomial (Fin n.succ) R)
          x :
        MvPolynomial (Fin n.succ) R)
      ((C : (a : R) → MvPolynomial (Fin n.succ) R) x : MvPolynomial (Fin n.succ) R)
⊢ RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →+* MvPolynomial (Fin n.succ) R)
      (RingHom.comp Polynomial.C C) =
    C

Tactic:
refine RingHom.ext fun x => ?_

Premises used: RingHom.ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
x : R
⊢ Eq (α := MvPolynomial (Fin n.succ) R)
    (((↑(AlgEquiv.symm (finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →+* MvPolynomial (Fin n.succ) R) :
          (a : (MvPolynomial (Fin n) R)[X]) → MvPolynomial (Fin n.succ) R)
        ((RingHom.comp Polynomial.C C : (a : R) → (MvPolynomial (Fin n) R)[X]) x) :
      MvPolynomial (Fin n.succ) R)
    ((C : (a : R) → MvPolynomial (Fin n.succ) R) x : MvPolynomial (Fin n.succ) R)

Tactic:
(MvPolynomial.finSuccEquiv R n).injective
      (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) ?_)

Premises used: Trans.trans, AlgEquiv.apply_symm_apply, MvPolynomial.finSuccEquiv, AlgEquiv.injective
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
x : R
R₁ :
  Eq (α := (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp Polynomial.C C : (a : R) → (MvPolynomial (Fin n) R)[X]) x : (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        ((C : (a : R) → MvPolynomial (Fin n.succ) R) x) :
      (MvPolynomial (Fin n) R)[X])
⊢ Eq (α := MvPolynomial (Fin n.succ) R)
    (((↑(AlgEquiv.symm (finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →+* MvPolynomial (Fin n.succ) R) :
          (a : (MvPolynomial (Fin n) R)[X]) → MvPolynomial (Fin n.succ) R)
        ((RingHom.comp Polynomial.C C : (a : R) → (MvPolynomial (Fin n) R)[X]) x) :
      MvPolynomial (Fin n.succ) R)
    ((C : (a : R) → MvPolynomial (Fin n.succ) R) x : MvPolynomial (Fin n.succ) R)

Tactic:
refine
    (MvPolynomial.finSuccEquiv R n).injective
      (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) ?_)

Premises used: Trans.trans, AlgEquiv.apply_symm_apply, MvPolynomial.finSuccEquiv, AlgEquiv.injective
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
x : R
⊢ Eq (α := (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp Polynomial.C C : (a : R) → (MvPolynomial (Fin n) R)[X]) x : (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        ((C : (a : R) → MvPolynomial (Fin n.succ) R) x) :
      (MvPolynomial (Fin n) R)[X])

Tactic:
simp only [MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C]

Premises used: MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
⊢ Eq (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (X 0) :
      (MvPolynomial (Fin n) R)[X])
    (Polynomial.X : (MvPolynomial (Fin n) R)[X])

Tactic:
simp [finSuccEquiv_apply]

Premises used: MvPolynomial.finSuccEquiv_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin n
⊢ Eq (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (X j.succ) :
      (MvPolynomial (Fin n) R)[X])
    ((Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X j) : (MvPolynomial (Fin n) R)[X])

Tactic:
simp [finSuccEquiv_apply]

Premises used: MvPolynomial.finSuccEquiv_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp :
  ∀ (m : Fin n →₀ ℕ) (i : ℕ),
    coeff m
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p) i) =
      coeff (cons i m) p
hq :
  ∀ (m : Fin n →₀ ℕ) (i : ℕ),
    coeff m
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) q) i) =
      coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (p + q))
        i) =
    coeff (cons i m) (p + q)

Tactic:
simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]

Premises used: map_add, Polynomial.coeff_add, MvPolynomial.coeff_add
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
monomial :
  r *
      coeff m
        ((HPow.hPow (α := (MvPolynomial (Fin n) R)[X]) (β := ℕ) Polynomial.X ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) *
              (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X])
                (∏ x : Fin n,
                  HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x)
                    ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ))).coeff
          i) =
    if j = cons i m then r else 0
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (Polynomial.coeff
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
          ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
        i))
    (coeff (cons i m) ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Fin (n + 1)) R) r))

Tactic:
simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, Finsupp.prod_pow,
      Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
      Fin.cases_succ, ← _root_.map_prod, ← map_pow, Function.comp_apply]

Premises used: Fin.cases_zero, MvPolynomial.coeff_C_mul, Polynomial.coeff_C_mul, map_pow, MvPolynomial.coe_eval₂Hom, map_prod, Finsupp.prod_pow, Fin.prod_univ_succ, MvPolynomial.finSuccEquiv_apply, RingHom.coe_comp, MvPolynomial.coeff_monomial, Function.comp_apply, MvPolynomial.eval₂_monomial, Fin.cases_succ
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
monomial :
  r *
      coeff m
        (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
          ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
        else 0) =
    r * if j = cons i m then 1 else 0
⊢ r *
      coeff m
        ((HPow.hPow (α := (MvPolynomial (Fin n) R)[X]) (β := ℕ) Polynomial.X ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) *
              (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X])
                (∏ x : Fin n,
                  HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x)
                    ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ))).coeff
          i) =
    if j = cons i m then r else 0

Tactic:
rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]

Premises used: mul_boole, HPow.hPow, mul_comm, Polynomial.coeff_C_mul_X_pow, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
monomial :
  Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if j = cons i m then 1 else 0)
⊢ r *
      coeff m
        (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
          ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
        else 0) =
    r * if j = cons i m then 1 else 0

Tactic:
congr 1
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
monomial :
  Eq.{u + 1} (α := R)
    (coeff m
      (if i = (cons i m : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n,
          HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((cons i m : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if cons i m = cons i m then 1 else 0)
monomial₁ :
  ∀ (hjmi : j ≠ cons i m),
    Eq.{u + 1} (α := R)
      (coeff m
        (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
          ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
        else 0))
      (if j = cons i m then 1 else 0)
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if j = cons i m then 1 else 0)

Tactic:
obtain rfl | hjmi := eq_or_ne j (m.cons i)

Premises used: eq_or_ne, Finsupp.cons, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (cons i m : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n,
          HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((cons i m : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if cons i m = cons i m then 1 else 0)

Tactic:
simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul,
        Finsupp.prod_pow] using coeff_monomial m m (1 : R)

Premises used: Finsupp.cons_succ, MvPolynomial.C_1, if_pos, Finsupp.prod_pow, Finsupp.cons_zero, MvPolynomial.monomial_eq, MvPolynomial.coeff_monomial, OfNat.ofNat, one_mul, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
monomial :
  Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    0
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if j = cons i m then 1 else 0)

Tactic:
simp only [hjmi, if_false]

Premises used: if_false
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
monomial :
  ∀ (hij : i ≠ (j : (a : Fin (n + 1)) → ℕ) 0),
    Eq.{u + 1} (α := R)
      (coeff m
        (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
          ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
        else 0))
      0
monomial₁ :
  ∀ (hjmi : j ≠ cons ((j : (a : Fin (n + 1)) → ℕ) 0) m),
    Eq.{u + 1} (α := R)
      (coeff m
        (if Eq (α := ℕ) ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) then
          ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
        else 0))
      0
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    0

Tactic:
obtain hij | rfl := ne_or_eq i (j 0)

Premises used: ne_or_eq, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
hij : i ≠ (j : (a : Fin (n + 1)) → ℕ) 0
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    0

Tactic:
simp only [hij, if_false, coeff_zero]

Premises used: if_false, MvPolynomial.coeff_zero
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons ((j : (a : Fin (n + 1)) → ℕ) 0) m
monomial :
  Eq.{u + 1} (α := R)
    (coeff m
      (∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)))
    0
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if Eq (α := ℕ) ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    0

Tactic:
simp only [if_true]

Premises used: if_true
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons ((j : (a : Fin (n + 1)) → ℕ) 0) j.tail
⊢ j ≠ j

Tactic:
rw [cons_tail] at hjmi

Premises used: Finsupp.cons_tail
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons ((j : (a : Fin (n + 1)) → ℕ) 0) m
⊢ m ≠ j.tail

Tactic:
have hmj : m ≠ j.tail := by
        rintro rfl
        rw [cons_tail] at hjmi
        contradiction
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
add :
  ∀ (p q : MvPolynomial (Fin (n + 1)) R)
    (hp :
      ∀ (m : Fin n →₀ ℕ) (i : ℕ),
        coeff m
            (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p)
              i) =
          coeff (cons i m) p)
    (hq :
      ∀ (m : Fin n →₀ ℕ) (i : ℕ),
        coeff m
            (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) q)
              i) =
          coeff (cons i m) q)
    (m : Fin n →₀ ℕ) (i : ℕ),
    coeff m
        (Polynomial.coeff
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (p + q)) i) =
      coeff (cons i m) (p + q)
monomial :
  ∀ (j : Fin (n + 1) →₀ ℕ) (r : R) (m : Fin n →₀ ℕ) (i : ℕ),
    Eq.{u + 1} (α := R)
      (coeff m
        (Polynomial.coeff
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
            ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
          i))
      (coeff (cons i m) ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
⊢ coeff m
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) =
    coeff (cons i m) f

Tactic:
induction f using MvPolynomial.induction_on' generalizing i m with
  | add p q hp hq => simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]
  | monomial j r =>
    simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, Finsupp.prod_pow,
      Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
      Fin.cases_succ, ← _root_.map_prod, ← map_pow, Function.comp_apply]
    rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]; congr 1
    obtain rfl | hjmi := eq_or_ne j (m.cons i)
    · simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul,
        Finsupp.prod_pow] using coeff_monomial m m (1 : R)
    · simp only [hjmi, if_false]
      obtain hij | rfl := ne_or_eq i (j 0)
      · simp only [hij, if_false, coeff_zero]
      simp only [if_true]
      have hmj : m ≠ j.tail := by
        rintro rfl
        rw [cons_tail] at hjmi
        contradiction
      simpa only [monomial_eq, C_1, one_mul, Finsupp.prod_pow, tail_apply, if_neg hmj.symm] using
        coeff_monomial m j.tail (1 : R)

Premises used: if_true, Finsupp.cons_succ, if_false, MvPolynomial.monomial, Fin.cases_zero, MvPolynomial.coeff_C_mul, mul_boole, Polynomial.coeff_C_mul, MvPolynomial.C_1, map_add, map_pow, Polynomial.coeff_add, if_pos, MvPolynomial.coe_eval₂Hom, map_prod, Finsupp.prod_pow, Fin.prod_univ_succ, MvPolynomial.coeff_zero, Finsupp.cons_zero, MvPolynomial.finSuccEquiv_apply, MvPolynomial.monomial_eq, RingHom.coe_comp, MvPolynomial.coeff_add, MvPolynomial.coeff_monomial, Function.comp_apply, MvPolynomial.eval₂_monomial, Fin.cases_succ, Finsupp.tail_apply, Polynomial.coeff_C_mul_X_pow, OfNat.ofNat, one_mul, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
⊢ Eq (α := R[X])
    (Polynomial.map (eval s)
      ((Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X])
        ((algebraMap R (MvPolynomial (Fin n) R) : (a : R) → MvPolynomial (Fin n) R) r)))
    ((Polynomial.C : (a : R) → R[X])
      ((eval s : (a : MvPolynomial (Fin n) R) → R)
        ((algebraMap R (MvPolynomial (Fin n) R) : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)))

Tactic:
Polynomial.map_C (eval s)

Premises used: MvPolynomial.eval, Polynomial.map_C
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
h :
  r =
    (eval s : (a : MvPolynomial (Fin n) R) → R)
      ((algebraMap R (MvPolynomial (Fin n) R) : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)
⊢ Eq (α := R[X])
    (OneHom.toFun
      (↑(↑(Polynomial.mapRingHom (eval s)) : (MvPolynomial (Fin n) R)[X] →* R[X]) :
        OneHom (MvPolynomial (Fin n) R)[X] R[X])
      ((algebraMap R (MvPolynomial (Fin n) R)[X] : (a : R) → (MvPolynomial (Fin n) R)[X]) r))
    ((algebraMap R R[X] : (a : R) → R[X]) r)

Tactic:
convert! Polynomial.map_C (eval s)

Premises used: MvPolynomial.eval, Polynomial.map_C
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
⊢ r =
    (eval s : (a : MvPolynomial (Fin n) R) → R)
      ((algebraMap R (MvPolynomial (Fin n) R) : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)

Tactic:
(eval_C _).symm

Premises used: MvPolynomial.eval_C, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
⊢ r =
    (eval s : (a : MvPolynomial (Fin n) R) → R)
      ((algebraMap R (MvPolynomial (Fin n) R) : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)

Tactic:
exact (eval_C _).symm

Premises used: MvPolynomial.eval_C, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial (Fin n) R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
aeval :
  Eq (α := R)
    ((MvPolynomial.aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) f :
      R)
    ((AlgHom.comp (Polynomial.aeval y)
            (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        f :
      R)
⊢ (eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) f =
    Polynomial.eval y
      (Polynomial.map (eval s)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f))

Tactic:
change
    aeval (Fin.cons y s : Fin (n + 1) → R) f =
      (Polynomial.aeval y).comp (φ.comp (finSuccEquiv R n).toAlgHom) f

Premises used: MvPolynomial.aeval, AlgEquiv.toAlgHom, Fin.cons, MvPolynomial.finSuccEquiv, Polynomial.aeval, AlgHom.comp, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial (Fin n) R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
e_a :
  Eq (α := MvPolynomial (Fin (n + 1)) R →ₐ[R] R) (aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s))
    (AlgHom.comp (Polynomial.aeval y)
      (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])))
⊢ Eq (α := R) ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) f : R)
    ((AlgHom.comp (Polynomial.aeval y)
            (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        f :
      R)

Tactic:
congr 2
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial (Fin n) R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
e_a :
  ∀ (i : Fin (n + 1)),
    Eq (α := R)
      ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X i) : R)
      ((AlgHom.comp (Polynomial.aeval y)
              (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
            (a : MvPolynomial (Fin (n + 1)) R) → R)
          (X i) :
        R)
⊢ Eq (α := MvPolynomial (Fin (n + 1)) R →ₐ[R] R) (aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s))
    (AlgHom.comp (Polynomial.aeval y)
      (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])))

Tactic:
apply MvPolynomial.algHom_ext

Premises used: MvPolynomial.algHom_ext