R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) (↑(finSuccEquiv R n) f))
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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))
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 }
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(aeval (Fin.cons y s)) f = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) f
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) (↑(finSuccEquiv R n) f))
show
  aeval (Fin.cons y s : Fin (n + 1) → R) f =
    (Polynomial.aeval y).comp (φ.comp (finSuccEquiv R n).toAlgHom) f
case e_a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ aeval (Fin.cons y s) = AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(aeval (Fin.cons y s)) f = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) f
congr 2
case e_a.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ∀ (i : Fin (n + 1)),
    ↑(aeval (Fin.cons y s)) (X i) = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X i)
case e_a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ aeval (Fin.cons y s) = AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))
apply MvPolynomial.algHom_ext
case e_a.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(aeval (Fin.cons y s)) (X 0) = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X 0) ∧
    ∀ (i : Fin n),
      ↑(aeval (Fin.cons y s)) (X (Fin.succ i)) =
        ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X (Fin.succ i))
case e_a.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ∀ (i : Fin (n + 1)),
    ↑(aeval (Fin.cons y s)) (X i) = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X i)
rw [Fin.forall_fin_succ]
no goals
case e_a.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
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 :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(aeval (Fin.cons y s)) (X 0) = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X 0) ∧
    ∀ (i : Fin n),
      ↑(aeval (Fin.cons y s)) (X (Fin.succ i)) =
        ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X (Fin.succ i))
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]
case h.e'_3.h.e'_6
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
src✝ : (MvPolynomial (Fin n) R)[X] →+* R[X] := mapRingHom (eval s)
r : R
⊢ r = ↑(eval s) (↑(algebraMap R (MvPolynomial (Fin n) R)) r)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
src✝ : (MvPolynomial (Fin n) R)[X] →+* R[X] := mapRingHom (eval s)
r : R
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                  OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
    ↑(algebraMap R R[X]) r
convert Polynomial.map_C (eval s)
no goals
case h.e'_3.h.e'_6
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1054353
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
src✝ : (MvPolynomial (Fin n) R)[X] →+* R[X] := mapRingHom (eval s)
r : R
⊢ r = ↑(eval s) (↑(algebraMap R (MvPolynomial (Fin n) R)) r)
exact (eval_C _).symm