Eval Int map

theorem evalInt_map (q : k) (hq : valuation k q < 1) (F : ℤ⟦X⟧) :    algebraMap k l (evalInt q F) = evalInt (algebraMap k l q) F := by  have hq' : valuation l (algebraMap k l q) < 1 := valuation_algebraMap_lt_one hq  rw [← sub_eq_zero]  by_contra h  obtain ⟨N, hN⟩ := exists_pow_valuation_lt (algebraMap k l q) hq'    (Units.mk0 _ ((valuation l).ne_zero_iff.mpr h))  -- the image of the `k`-side partial sum is the `l`-side partial sum  have hmapsum : algebraMap k l      (∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n) =      ∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : l) * (algebraMap k l q) ^ n := by    rw [map_sum]    exact Finset.sum_congr rfl fun n _ ↦ by rw [map_mul, map_pow, map_intCast]  -- the `k`-side tail bound, transferred along the map of value groups  have h1 : valuation l (algebraMap k l (evalInt q F) -      ∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : l) * (algebraMap k l q) ^ n) ≤      valuation l (algebraMap k l q) ^ N := by    rw [← hmapsum, ← map_sub]    calc valuation l (algebraMap k l (evalInt q F -            ∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n))        = ValuativeExtension.mapValueGroupWithZero k l (valuation k (evalInt q F -            ∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n)) :=          (ValuativeExtension.mapValueGroupWithZero_valuation _).symm      _ ≤ ValuativeExtension.mapValueGroupWithZero k l (valuation k q ^ N) :=          ValuativeExtension.mapValueGroupWithZero_strictMono.monotone            (valuation_evalInt_sub_sum_le q hq F N)      _ = valuation l (algebraMap k l q) ^ N := by          rw [map_pow, ValuativeExtension.mapValueGroupWithZero_valuation]  -- the `l`-side tail bound  have h2 := valuation_evalInt_sub_sum_le (algebraMap k l q) hq' F N  -- ultrametrically, the difference is then smaller than its own valuation: absurd  refine absurd ?_ (lt_irrefl (valuation l    (algebraMap k l (evalInt q F) - evalInt (algebraMap k l q) F)))  calc valuation l (algebraMap k l (evalInt q F) - evalInt (algebraMap k l q) F)      = valuation l ((algebraMap k l (evalInt q F) -          ∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : l) * (algebraMap k l q) ^ n) -        (evalInt (algebraMap k l q) F -          ∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : l) * (algebraMap k l q) ^ n)) := by        congr 1        ring    _ ≤ max _ _ := Valuation.map_sub _ _ _    _ ≤ valuation l (algebraMap k l q) ^ N := max_le h1 h2    _ < _ := hN