[GOAL]
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : 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
[PROOFSTEP]
apply induction_on p
[GOAL]
case h_C
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (a : R),
    Polynomial.eval x (eval₂ f g (↑C a)) =
      eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (↑C a)
[PROOFSTEP]
simp
[GOAL]
case h_add
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (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)
[PROOFSTEP]
intro p q hp hq
[GOAL]
case h_add
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ 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)
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case h_X
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (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)
[PROOFSTEP]
intro p n hp
[GOAL]
case h_X
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ 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)
[PROOFSTEP]
simp [hp]
[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 x) (Polynomial.eval q (↑(finSuccEquiv R n) f)) = ↑(eval fun i => Fin.cases (↑(eval x) q) x i) f
[PROOFSTEP]
simp only [finSuccEquiv_apply, coe_eval₂Hom, polynomial_eval_eval₂, eval_eval₂]
[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 => ↑(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
[PROOFSTEP]
conv in RingHom.comp _ _ => {
  refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
  simp}
[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))
[PROOFSTEP]
{ refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
  simp}
[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))
[PROOFSTEP]
{ refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
  simp}
[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))
[PROOFSTEP]
refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
[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
⊢ ↑(RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C))) r = ↑(RingHom.id R) r
[PROOFSTEP]
simp
[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 => ↑(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
[PROOFSTEP]
simp only [eval₂_id]
[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 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
[PROOFSTEP]
congr
[GOAL]
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
[PROOFSTEP]
funext i
[GOAL]
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
[PROOFSTEP]
refine Fin.cases (by simp) (by simp) i
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
simp
