-- Mathlib/Algebra/MvPolynomial/Polynomial.lean
theorem eval_polynomial_eval_finSuccEquiv {n : ℕ} {x : Fin n → R}
    [CommSemiring R] (f : MvPolynomial (Fin (n + 1)) R) (q : MvPolynomial (Fin n) R) :
    (eval x) (Polynomial.eval q (finSuccEquiv R n f)) = eval (Fin.cases (eval x q) x) f

Proof state:
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 => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s)))
      f =
    (eval fun i => Fin.cases ((eval x) q) x i) f

Tactic:
simp only [eval₂_id]

Result:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ (eval fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) f =
    (eval fun i => Fin.cases ((eval x) q) x i) f

Proof state:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ ∀ (i : Fin n),
    (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i.succ)) =
      Fin.cases ((eval x) q) x i.succ

Tactic:
simp

Result:
no goals

Proof state:
case e_a.e_f
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ (fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) = fun i =>
    Fin.cases ((eval x) q) x i

Tactic:
funext i

Result:
case e_a.e_f.h
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i)) = Fin.cases ((eval x) q) x i

Proof state:
case e_a.e_f.h
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i)) = Fin.cases ((eval x) q) x i

Tactic:
refine Fin.cases (by simp) (by simp) i

Result:
no goals

Proof state:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) 0)) = Fin.cases ((eval x) q) x 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ eval₂ ((eval x).comp ((Polynomial.evalRingHom q).comp (Polynomial.C.comp C)))
      (fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) f =
    (eval fun i => Fin.cases ((eval x) q) x i) f

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

Result:
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 => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s)))
      f =
    (eval fun i => Fin.cases ((eval x) q) x i) f

Proof state:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ (eval x) (Polynomial.eval q ((finSuccEquiv R n) f)) = (eval fun i => Fin.cases ((eval x) q) x i) f

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

Result:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ eval₂ ((eval x).comp ((Polynomial.evalRingHom q).comp (Polynomial.C.comp C)))
      (fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) f =
    (eval fun i => Fin.cases ((eval x) q) x i) f

Proof state:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ (eval fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) f =
    (eval fun i => Fin.cases ((eval x) q) x i) f

Tactic:
congr

Result:
case e_a.e_f
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ (fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) = fun i =>
    Fin.cases ((eval x) q) x i