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 => ↑(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
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
simp only [finSuccEquiv_apply, coe_eval₂Hom, polynomial_eval_eval₂, eval_eval₂]
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
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 => ↑(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
conv in RingHom.comp _ _ =>
{ refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
  simp }
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
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
simp only [eval₂_id]
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
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
congr
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
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
funext i
no goals
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
refine Fin.cases (by simp) (by simp) i
no goals
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
simp
no goals
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)) (Fin.succ i))) =
      Fin.cases (↑(eval x) q) x (Fin.succ i)
simp