-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem eval_eq_eval_mv_eval' (s : Fin n → R) (y : R) (f : MvPolynomial (Fin (n + 1)) R) :
    eval (Fin.cons y s : Fin (n + 1) → R) f =
      Polynomial.eval y (Polynomial.map (eval s) (finSuccEquiv R n f))

Proof state:
case e_a.hf
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (aeval (Fin.cons y s)) (X 0) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X 0) ∧
    ∀ (i : Fin n),
      (aeval (Fin.cons y s)) (X i.succ) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X i.succ)

Tactic:
simp only [φ, aeval_X, Fin.cons_zero, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp,
  Polynomial.coe_aeval_eq_eval, Polynomial.map_C, AlgHom.coe_mk, RingHom.toFun_eq_coe,
  Polynomial.coe_mapRingHom, comp_apply, finSuccEquiv_apply, eval₂Hom_X',
  Fin.cases_zero, Polynomial.map_X, Polynomial.eval_X, Fin.cons_succ,
  Fin.cases_succ, eval_X, Polynomial.eval_C,
  RingHom.coe_mk, MonoidHom.coe_coe, AlgHom.coe_coe, implies_true, and_self,
  RingHom.toMonoidHom_eq_coe]

Result:
no goals

Proof state:
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquiv R n) f))

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

Result:
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (aeval (Fin.cons y s)) f = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) f

Proof state:
case e_a
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ aeval (Fin.cons y s) = (Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))

Tactic:
apply MvPolynomial.algHom_ext

Result:
case e_a.hf
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ ∀ (i : Fin (n + 1)), (aeval (Fin.cons y s)) (X i) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X i)

Proof state:
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (aeval (Fin.cons y s)) f = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) f

Tactic:
congr 2

Result:
case e_a
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ aeval (Fin.cons y s) = (Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))

Proof state:
case h.e'_3.h.e'_6
R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
⊢ r = (eval s) ((algebraMap R (MvPolynomial (Fin n) R)) r)

Tactic:
exact (eval_C _).symm

Result:
no goals

Proof state:
case e_a.hf
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ ∀ (i : Fin (n + 1)), (aeval (Fin.cons y s)) (X i) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X i)

Tactic:
rw [Fin.forall_iff_succ]

Result:
case e_a.hf
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (aeval (Fin.cons y s)) (X 0) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X 0) ∧
    ∀ (i : Fin n),
      (aeval (Fin.cons y s)) (X i.succ) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X i.succ)

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
⊢ (eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquiv R n) f))

Tactic:
let φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  { Polynomial.mapRingHom (eval s) with
    commutes' := fun r => by
      convert Polynomial.map_C (eval s)
      exact (eval_C _).symm }

Result:
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 := mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquiv R n) f))

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
⊢ (↑↑__src✝).toFun ((algebraMap R (MvPolynomial (Fin n) R)[X]) r) = (algebraMap R R[X]) r

Tactic:
convert Polynomial.map_C (eval s)

Result:
case h.e'_3.h.e'_6
R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
⊢ r = (eval s) ((algebraMap R (MvPolynomial (Fin n) R)) r)