Place_mk_taylorCoeff_evalEval.lean

theorem taylorRem_zero_fun (v : Place K F) (t : F) (r : ℕ) : taylorRem v t 0 r = 0

theorem taylorCoeff_zero_fun (v : Place K F) (t : F) (r : ℕ) : taylorCoeff v t r 0 = 0

theorem taylorRem_algebraMap_one (v : Place K F) (t : F) (c : K) :
    taylorRem v t (algebraMap K F c) 1 = 0

theorem evalAt_eq_zero_of_ord_pos (v : Place K F) {g : F} (hg0 : g ≠ 0) (hpos : 0 < v.ord g) :
    v.evalAt g = 0

theorem _root_.AlgebraicCurve.Place.mk_taylorCoeff_evalEval
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1) {z y : F}
    (hz : z ∈ v.toValuationSubring) (hy : y ∈ v.toValuationSubring)
    (G : Polynomial (Polynomial K)) :
    (PowerSeries.mk fun n =>
        taylorCoeff v t n ((G.map (Polynomial.mapRingHom (algebraMap K F))).evalEval z y))
      = (G.map (Polynomial.mapRingHom (algebraMap K (PowerSeries K)))).evalEval
          (PowerSeries.mk fun n => taylorCoeff v t n z) (PowerSeries.mk fun n => taylorCoeff v t n
            y) := by
  let O := v.toValuationSubring
  let φ : O →+* PowerSeries K :=
    { toFun := fun f => PowerSeries.mk fun n => taylorCoeff v t n (f : F)
      map_one' := by
        ext n
        rw [PowerSeries.coeff_mk, PowerSeries.coeff_one, OneMemClass.coe_one, ← map_one (algebraMap
          K F),
          taylorCoeff_algebraMap]
      map_mul' := fun f g => by
        ext n
        rw [PowerSeries.coeff_mk, MulMemClass.coe_mul, PowerSeries.coeff_mul,
          taylorCoeff_mul v hv ht f.2 g.2 n]
        simp only [PowerSeries.coeff_mk]
      map_zero' := by
        ext n
        rw [PowerSeries.coeff_mk, ZeroMemClass.coe_zero, taylorCoeff_zero_fun, map_zero]
      map_add' := fun f g => by
        ext n
        rw [PowerSeries.coeff_mk, AddMemClass.coe_add, taylorCoeff_add v hv ht f.2 g.2 n, map_add,
          PowerSeries.coeff_mk, PowerSeries.coeff_mk] }
  have hφ : ∀ f : O, φ f = PowerSeries.mk fun n => taylorCoeff v t n (f : F) := fun _ => rfl
  have hφC : φ.comp (algebraMap K O) = algebraMap K (PowerSeries K) := by
    refine RingHom.ext fun c => ?_
    ext n
    rw [RingHom.comp_apply, hφ, PowerSeries.coeff_mk, Place.coe_algebraMap,
      taylorCoeff_algebraMap, ← PowerSeries.C_eq_algebraMap, PowerSeries.coeff_C]
  have hOF : (algebraMap O F).comp (algebraMap K O) = algebraMap K F :=
    (IsScalarTower.algebraMap_eq K O F).symm
  have hsub : ∀ f : O, algebraMap O F f = (f : F) := fun _ => rfl
  have hA : (G.map (Polynomial.mapRingHom (algebraMap K F))).evalEval z y
      = (((G.map (Polynomial.mapRingHom (algebraMap K O))).evalEval ⟨z, hz⟩ ⟨y, hy⟩ : O) : F) := by
    rw [← hsub, ← Polynomial.map_mapRingHom_evalEval (algebraMap O F), Polynomial.map_map,
      Polynomial.mapRingHom_comp, hOF]
    rfl
  rw [hA, ← hφ, ← Polynomial.map_mapRingHom_evalEval φ, Polynomial.map_map,
    Polynomial.mapRingHom_comp, hφC]
  rfl