Divisor_exists_pullbackAlong_single_one_eq_sum.lean

theorem exists_fin_sum_eq_sum_nsmul {α M : Type*} [AddCommMonoid M] (s : Finset α)
    (e : α → ℕ) (f : α → M) :
    ∀ n : ℕ, ∑ a ∈ s, e a = n →
      ∃ W : Fin n → α, (∀ i, W i ∈ s) ∧ ∑ i, f (W i) = ∑ a ∈ s, e a • f a

theorem _root_.AlgebraicCurve.Divisor.exists_pullbackAlong_single_one_eq_sum
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [AlgebraicCurve.HasPrincipalDivisors K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hFI : AlgebraicCurve.FundamentalIdentityAlong K
      φ hφ)
    (P : AlgebraicCurve.Place K F) (hdegP : P.deg = 1)
    (hdeg1 : ∀ w : AlgebraicCurve.Place K F', w.restrictAlong φ hφ = P → w.deg = 1)
    (n : ℕ) (hn : AlgebraicCurve.finrankAlong K φ = n) :
    ∃ W : Fin n → AlgebraicCurve.Place K F',
      AlgebraicCurve.Divisor.pullbackAlong φ hφ (Finsupp.single P 1) = ∑ i, Finsupp.single (W i) 1 ∧
        ∀ i, (W i).restrictAlong φ hφ = P