/-
Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)
-/
import SurfaceBlowup.Blowup.CurveSections
import SurfaceBlowup.Surfaces.ConcreteAtlas

/-!
# Exceptional divisor points of two-chart curve data

For the blow-up of a regular local surface at its closed point, this file relates two-chart curve
data (finitely many points of the two charts with local curve generators) to divisors on the
exceptional line `ℙ¹_k`. It computes level-one kernels as products of powers of irreducible
polynomials, shows that a curve datum matching a divisor `Dv` has degree `deg Dv`, constructs curve
data realizing prescribed child ideals, and proves that the glued global function lies in the fixed
tangent cell.

## Main results

* `SurfaceBlowup.level_one_kernel_polynomial`: the level-one kernel on a blow-up chart maps to the
  ideal of `k[X]` generated by a product of powers of distinct monic irreducibles;
  `SurfaceBlowup.two_chart_left_level_one_kernel_polynomial` specialises it to the left chart.
* `SurfaceBlowup.child_ideals_curve_datum`: prescribed child ideals are realized by a curve datum.
* `SurfaceBlowup.fixed_tangent_cell_curve_datum`: every ideal of the fixed tangent cell comes from
  a curve datum matching `Dv`.
* `SurfaceBlowup.matches_divisor_degree`: a curve datum matching `Dv` has degree `deg Dv`.
* `SurfaceBlowup.matches_divisor_level_one_polynomial`: its level-one left kernel is generated by
  the affine polynomial of `Dv`.
* `SurfaceBlowup.global_function_has_tangent_divisor`, `SurfaceBlowup.global_function_mem_cell`:
  the glued global function has tangent divisor `Dv` and lies in the fixed tangent cell.

## Implementation notes

Statements about the concrete surfaces `ConcreteSurface O pi u a b` are written with the local
notations `tChart`, `tExc`, ... for the blow-up charts and their data; see the notation section.

Provenance: `Thm_SurfaceBlowupV2_{boundary_contact_of_twisted_generator,
contracted_level_one_ideal_is_irreducible_power, two_chart_common_multiplicity_eq,
child_ideals_curve_datum, curve_datum_common_and_zero_clauses, curve_datum_matches_divisor,
matches_divisor_degree, fixed_tangent_cell_curve_datum, two_chart_left_level_one_kernel_polynomial,
matches_divisor_level_one_polynomial, global_function_has_tangent_divisor,
global_function_mem_cell}`.
-/

namespace SurfaceBlowup

open scoped BigOperators ENNReal

/-! ### Notation for the concrete surfaces

Local notations for the charts of the blow-up of `R = ConcreteSurface O pi u a b` at its
closed point `(t, x)`, taking the surface data as explicit arguments. -/

/-- The `t`-chart `R[x/t]` of the blow-up of the concrete surface at `(t, x)`. -/
local notation:max "tChart" O:max pi:max u:max a:max b:max =>
  BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)

/-- The structure map `R → R[x/t]`. -/
local notation:max "tBase" O:max pi:max u:max a:max b:max =>
  chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)

/-- The slope `x/t` in the `t`-chart. -/
local notation:max "tSlope" O:max pi:max u:max a:max b:max =>
  chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)

/-- The exceptional ideal `(t)` of the `t`-chart. -/
local notation:max "tExc" O:max pi:max u:max a:max b:max =>
  chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)

/-- The overlap of the two charts. -/
local notation:max "tOverlap" O:max pi:max u:max a:max b:max =>
  BlowupOverlap (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)

/-- The `x`-chart `R[t/x]` of the blow-up of the concrete surface at `(t, x)`. -/
local notation:max "xChart" O:max pi:max u:max a:max b:max =>
  BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)

/-- The structure map `R → R[t/x]`. -/
local notation:max "xBase" O:max pi:max u:max a:max b:max =>
  chartBase (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)

/-- The slope `t/x` in the `x`-chart. -/
local notation:max "xSlope" O:max pi:max u:max a:max b:max =>
  chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)

/-- The exceptional ideal `(x)` of the `x`-chart. -/
local notation:max "xExc" O:max pi:max u:max a:max b:max =>
  chartExceptional (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)

/-- If `f ≡ g` modulo the ideal `I`, then `(f) + I = I + (g)`. -/
private theorem span_sup_eq_sup_span {A : Type} [CommRing A] {I : Ideal A} {f g : A}
    (h : f - g ∈ I) : Ideal.span {f} ⊔ I = I ⊔ Ideal.span {g} := by
  refine le_antisymm (sup_le ?_ le_sup_left) (sup_le le_sup_right ?_) <;>
    rw [Ideal.span_singleton_le_iff_mem]
  · rw [← sub_add_cancel f g]
    exact add_mem (Ideal.mem_sup_left h) (Ideal.mem_sup_right (Ideal.mem_span_singleton_self g))
  · rw [← sub_sub_cancel f g]
    exact sub_mem (Ideal.mem_sup_left (Ideal.mem_span_singleton_self f)) (Ideal.mem_sup_right h)

/-- If `f = ∑ cᵢ t^(d-i) xⁱ`, then in the chart `R[t/x]` the function `f` factors as
`x^d · ∑ cᵢ (t/x)^(d-i)`, and the boundary contact of `f` with `t = 0` is `d` plus the contact
of the strict transform with the slope divisor. -/
theorem boundary_contact_of_twisted_generator (R : Type) [CommRing R] (t x : R)
    [(Ideal.span ({t,x} : Set R)).IsMaximal] (hreg : RegularParameterPair R t x) (d : ℕ) (f : R)
    (c : Fin (d + 1) → R) (hc : f = ∑ i : Fin (d + 1), c i * t ^ (d - i.val) * x ^ i.val) :
    algebraMap R (BlowupChart R x t) f = (chartBase R x t x)^d *
        ∑ i : Fin (d+1), algebraMap R (BlowupChart R x t) (c i) * (chartSlope R x t)^(d - i.val) ∧
      Module.length R (R ⧸ (Ideal.span {f} ⊔ Ideal.span {t})) = (d : ℕ∞) +
        Module.length (BlowupChart R x t) (BlowupChart R x t ⧸
          (Ideal.span {∑ i : Fin (d+1), algebraMap R (BlowupChart R x t) (c i) *
            (chartSlope R x t)^(d - i.val)} ⊔ Ideal.span {chartSlope R x t})) := by
  have hal : ∀ r : R, algebraMap R (BlowupChart R x t) r = chartBase R x t r := fun _ ↦ rfl
  set B := BlowupChart R x t
  set W := chartSlope R x t
  set g : B := ∑ i : Fin (d+1), algebraMap R B (c i) * W^(d - i.val) with hg
  refine ⟨?_, ?_⟩
  · rw [hc, map_sum, Finset.mul_sum]
    refine Finset.sum_congr rfl fun i _ ↦ ?_
    simp only [map_mul, map_pow, hal, ← blowup_chart_relation R x t]
    rw [← pow_mul_pow_sub _ (Nat.le_of_lt_succ i.isLt), hal]
    ring
  set I : Ideal R := Ideal.span {t}
  have hfI : f - c (Fin.last d) * x ^ d ∈ I := by
    rw [hc, Fin.sum_univ_castSucc]
    simp only [Fin.val_last, Nat.sub_self, pow_zero, mul_one, add_sub_cancel_right]
    exact Ideal.sum_mem _ fun i _ ↦ Ideal.mul_mem_right _ _ (Ideal.mul_mem_left _ _
      (Ideal.pow_mem_of_mem _ (Ideal.mem_span_singleton_self t) _ (Nat.sub_pos_of_lt i.isLt)))
  have hx (y) (hy : x * y ∈ I) : y ∈ I := by
    rw [← Ideal.Quotient.eq_zero_iff_mem] at hy ⊢
    apply hreg.2
    simpa using hy
  have hxd (n : ℕ) : ∀ y, x ^ n * y ∈ I → y ∈ I := by
    induction n with
    | zero => simp
    | succ n ih => exact fun y hy ↦ hx _ (ih _ (by rwa [pow_succ, mul_assoc] at hy))
  have hone : Module.length R (R ⧸ (I ⊔ Ideal.span {x})) = 1 := by
    rw [← Ideal.span_insert t {x}]
    have : IsSimpleModule R (R ⧸ Ideal.span ({t, x} : Set R)) :=
      isSimpleModule_iff_quot_maximal.mpr ⟨_, inferInstance, ⟨LinearEquiv.refl _ _⟩⟩
    exact Module.length_eq_one R _
  rw [span_sup_eq_sup_span hfI, length_quotient_sup_mul_eq_add R I (x ^ d) (c (Fin.last d)) (hxd d),
    length_quotient_sup_pow_eq_mul R I x hx d, hone, mul_one, add_comm]
  congr 1
  have hgW : g - algebraMap R B (c (Fin.last d)) ∈ Ideal.span {W} := by
    rw [hg, Fin.sum_univ_castSucc]
    simp only [Fin.val_last, Nat.sub_self, pow_zero, mul_one, add_sub_cancel_right]
    exact Ideal.sum_mem _ fun i _ ↦ Ideal.mul_mem_left _ _
      (Ideal.pow_mem_of_mem _ (Ideal.mem_span_singleton_self W) _ (Nat.sub_pos_of_lt i.isLt))
  rw [span_sup_eq_sup_span hgW]
  obtain ⟨ρ, hρ, -⟩ := boundary_chart_quotient_equiv R t x
  symm
  apply quotient_ring_length_intrinsic
  refine (DoubleQuot.quotQuotEquivQuotSup _ _).symm.trans
    ((Ideal.quotientEquiv _ _ ρ ?_).trans (DoubleQuot.quotQuotEquivQuotSup _ _))
  simp only [Ideal.map_span, Set.image_singleton]
  congr 2
  exact (hρ _).symm

/-- At a point `P` of the exceptional line corresponding to the irreducible `φ`, the image of the
contracted level-one curve ideal in `k[X]` is `(φ^r)`, where `r ≤ L` is the length of the
completed level-one quotient. -/
private theorem contracted_level_one_ideal_is_irreducible_power (R : Type) [CommRing R] (t x : R)
    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]
    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+*
      Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))
    (P : Ideal (BlowupChart R t x)) [P.IsMaximal]
    (φ : Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))
    (hφ : (P.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ})
    (hirr : Irreducible φ) (g : CompletedLocalAt (BlowupChart R t x) P) (L : ℕ)
    (hL : ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map
      (localCompletionMap (Localization.AtPrime P))) ^ L ≤ finiteLocalCurveIdeal (BlowupChart R t x)
      P (chartBase R t x t) g 1) :
    ∃ r : ℕ, r ≤ L ∧
        ((contractedLocalCurveIdeal (BlowupChart R t x) P (chartBase R t x t) g 1).map
        (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ^r} ∧
        Module.length (CompletedLocalAt (BlowupChart R t x) P) (CompletedLocalAt (BlowupChart R t x)
        P ⧸ finiteLocalCurveIdeal (BlowupChart R t x) P (chartBase R t x t) g 1) = (r : ℕ∞) := by
  set A := BlowupChart R t x
  set I := finiteLocalCurveIdeal A P (chartBase R t x t) g 1 with hIdef
  set J := contractedLocalCurveIdeal A P (chartBase R t x t) g 1 with hJdef
  have hPL : P ^ L ≤ J := completed_point_power_contraction A P L I hL
  have hTJ : chartExceptional R t x ≤ J := by
    rw [show chartExceptional R t x = Ideal.span {chartBase R t x t} from rfl, Ideal.span_le]
    rintro _ rfl
    change completedPointMap A P (chartBase R t x t) ∈ I
    rw [hIdef, finiteLocalCurveIdeal, pow_one]
    exact Ideal.subset_span (by simp)
  have hle : Ideal.span {φ ^ L} ≤ (J.map (Ideal.Quotient.mk (chartExceptional R t x))).map e := by
    have h1 := Ideal.map_pow e (Ideal.map (Ideal.Quotient.mk (chartExceptional R t x)) P) L
    have h0 := Ideal.map_pow (Ideal.Quotient.mk (chartExceptional R t x)) P L
    rw [← Ideal.span_singleton_pow, ← hφ, ← h1, ← h0]
    exact Ideal.map_mono (Ideal.map_mono hPL)
  have hK : RingHom.ker ((Ideal.Quotient.mk I).comp (completedPointMap A P)) = J := by
    rw [← RingHom.comap_ker, Ideal.mk_ker]; rfl
  have E1 : (A ⧸ J) ≃+* (CompletedLocalAt A P ⧸ I) :=
    (Ideal.quotEquivOfEq hK.symm).trans (RingHom.quotientKerEquivOfSurjective
      (finite_completed_point_quotient_surjective A P L I hL))
  have hlen := quotient_ring_length_intrinsic _ _ _ _ E1
  obtain ⟨r, hrL, hr⟩ : ∃ r ≤ L,
      (J.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ ^ r} := by
    let _ := Ideal.Quotient.field (Ideal.span ({t,x} : Set R))
    exact polynomial_ideal_of_irreducible_pow_le _ φ hirr _ L hle
  have hφ : Module.length (Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))
      (Polynomial (R ⧸ Ideal.span ({t,x} : Set R)) ⧸ Ideal.span {φ ^ r}) = r := by
    let _ := Ideal.Quotient.field (Ideal.span ({t,x} : Set R))
    exact (polynomial_quotient_irreducible_pow_length _ φ hirr r).1
  refine ⟨r, hrL, hr, ?_⟩
  rw [← hlen, ← hφ]
  exact quotient_ring_length_intrinsic _ _ _ _
    ((DoubleQuot.quotQuotEquivQuotOfLE hTJ).symm.trans (Ideal.quotientEquiv _ _ e hr.symm))

private theorem length_quot_span_pair_toNat_eq {S S' : Type} [CommRing S] [CommRing S']
    (Φ : S ≃+* S') (g e : S) (g' e' : S')
    (hg : Φ g = g') (he : Ideal.span {Φ e} = Ideal.span {e'}) :
    (Module.length S (S ⧸ Ideal.span {g, e ^ 1})).toNat =
      (Module.length S' (S' ⧸ Ideal.span {g', e' ^ 1})).toNat := by
  rw [pow_one, pow_one]
  have h : Ideal.span {g', e'} = (Ideal.span {g, e}).map Φ := by
    rw [Ideal.map_span, Set.image_pair, hg, Ideal.span_insert, Ideal.span_insert, he]
  rw [quotient_ring_length_intrinsic S S' (Ideal.span {g, e}) (Ideal.span {g', e'})
    (Ideal.quotientEquiv _ _ Φ h)]

/-- At a common point of the two charts, the left and right multiplicities agree with the
multiplicity computed on the overlap. -/
theorem two_chart_common_multiplicity_eq (R : Type) [CommRing R] (t x : R)
    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta) (i : D.ι) :
    leftMultiplicity D (Sum.inl i) = commonMultiplicity D i ∧
      rightMultiplicity D (Sum.inl i) = commonMultiplicity D i := by
  constructor
  · unfold leftMultiplicity commonMultiplicity leftLevelIdeal commonLevelIdeal finiteLocalCurveIdeal
    symm
    refine length_quot_span_pair_toNat_eq (D.leftIso i) _ _ _ _ rfl ?_
    have := D.leftIso_compat i (chartBase R t x t)
    unfold overlapException
    rw [this]; rfl
  · unfold rightMultiplicity commonMultiplicity rightLevelIdeal commonLevelIdeal
      finiteLocalCurveIdeal
    symm
    refine length_quot_span_pair_toNat_eq (D.rightIso i) _ _ _ _ rfl ?_
    have hx := D.rightIso_compat i (chartBase R x t x)
    have hrel : beta.right (chartBase R x t x) = overlapException R t x * overlapSlope R t x := by
      have h1 : beta.right (chartBase R x t x) = algebraMap R (BlowupOverlap R t x) x :=
        beta.right.commutes x
      have h2 := congrArg (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))
        (blowup_chart_relation R t x)
      rw [h1]
      unfold overlapException overlapSlope
      rw [← map_mul, h2]
      exact (IsScalarTower.algebraMap_apply R (BlowupChart R t x) (BlowupOverlap R t x) x).symm
    have hu : IsUnit (overlapSlope R t x) := IsLocalization.Away.algebraMap_isUnit _
    have hu' : IsUnit (D.rightIso i
        (completedPointMap (BlowupOverlap R t x) (D.Q i) (overlapSlope R t x))) :=
      (hu.map _).map _
    rw [hrel, map_mul, map_mul] at hx
    refine Eq.trans ?_ (congrArg Ideal.span (congrArg _ hx))
    exact Ideal.span_singleton_mul_right_unit hu' _ |>.symm

private noncomputable def completedLocalCast {A : Type} [CommRing A] {P' P : Ideal A} [P'.IsPrime]
    [P.IsPrime] (h : P' = P) :
    CompletedLocalAt A P' ≃+* CompletedLocalAt A P := by
  subst h; exact RingEquiv.refl _

private theorem completedLocalCast_completedPointMap {A : Type} [CommRing A] {P' P : Ideal A}
    [P'.IsPrime] [P.IsPrime] (h : P' = P) (a : A) :
    completedLocalCast h (completedPointMap A P' a) = completedPointMap A P a := by
  subst h; rfl

private theorem length_finiteLocalCurveIdeal_transport {A S : Type} [CommRing A] [CommRing S]
    {P' P : Ideal A} [P'.IsPrime] [P.IsPrime]
    (Φ : S ≃+* CompletedLocalAt A P') (h : P' = P) (gC : CompletedLocalAt A P) (e0 : A) (n : ℕ∞)
    (hl : Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸
      (Ideal.span {gC} ⊔ Ideal.span {completedPointMap A P e0})) = n) :
    Module.length (CompletedLocalAt A P') (CompletedLocalAt A P' ⧸
      finiteLocalCurveIdeal A P' e0 (Φ ((Φ.trans (completedLocalCast h)).symm gC)) 1) = n := by
  rw [RingEquiv.symm_trans_apply, RingEquiv.apply_symm_apply]
  subst h
  rw [finiteLocalCurveIdeal, pow_one, Ideal.span_insert]
  exact hl

private theorem strictTransformAt_transport (R : Type) [CommRing R] (t x : R)
    {S : Type} [CommRing S]
    {P' P : Ideal (BlowupChart R t x)} [P'.IsPrime] [P.IsPrime]
    (Φ : S ≃+* CompletedLocalAt (BlowupChart R t x) P') (h : P' = P)
    (gC : CompletedLocalAt (BlowupChart R t x) P) (d : ℕ) (J : Ideal R)
    (hs : strictTransformAt R t x P' d J =
        Ideal.span {Φ ((Φ.trans (completedLocalCast h)).symm gC)}) :
    strictTransformAt R t x P d J = Ideal.span {gC} := by
  rw [RingEquiv.symm_trans_apply, RingEquiv.apply_symm_apply] at hs
  subst h
  exact hs

private theorem length_finiteLocalCurveIdeal_toNat {A : Type} [CommRing A] {P : Ideal A} [P.IsPrime]
    (g : CompletedLocalAt A P) (e0 : A) (n : ℕ)
    (hl : Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸
      (Ideal.span {g} ⊔ Ideal.span {completedPointMap A P e0})) = n) :
    n = (Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸
      finiteLocalCurveIdeal A P e0 g 1)).toNat := by
  rw [finiteLocalCurveIdeal, pow_one, Ideal.span_insert, hl, ENat.toNat_natCast]

/-- At the prime `P` of `A`, every element `g` of the completed local ring such that `(g, z)` has
finite colength `n` is transverse to `z` (multiplication by `z` is injective modulo `g`), and the
ideal `(g, z)` contains a power of the maximal ideal. -/
private def TransverseFiniteAt (A : Type) [CommRing A] (P : Ideal A) [P.IsPrime] (z : A) : Prop :=
  ∀ (g : CompletedLocalAt A P) (n : ℕ),
    Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸
      (Ideal.span {g} ⊔ Ideal.span {completedPointMap A P z})) = n →
    Function.Injective (fun w : CompletedLocalAt A P ⧸ Ideal.span {g} =>
      Ideal.Quotient.mk (Ideal.span {g}) (completedPointMap A P z) * w) ∧
    ∃ L : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map
      (localCompletionMap (Localization.AtPrime P)))^L ≤ finiteLocalCurveIdeal A P z g 1

/-- The nonzero affine directions in the support of the divisor `Dv`. -/
private abbrev CommonDirections {k : Type} [Field k] (Dv : ExceptionalDivisor k) : Type :=
  {φ : AffineDirection k // φ ≠ zeroAffine k ∧ 0 < Dv (some φ)}

/-- The overlap point of a nonzero direction (a named function, so that the instance arguments
in the curve datum built below stay syntactically uniform). -/
private noncomputable def commonPoint (R : Type) [CommRing R] [IsLocalRing R] (t x : R)
    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))
    {Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)} (i : CommonDirections Dv) :
    Ideal (BlowupOverlap R t x) :=
  (directionPoint R t x e i.1).map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))

/-- Generic form of `child_ideals_curve_datum`: the points of the exceptional line are assumed to
have the expected properties, and child-ideal generators are assumed transverse and finite. -/
private theorem child_ideals_curve_datum_of_points (R : Type) [CommRing R] [IsLocalRing R] (t x : R)
    [IsNoetherianRing (BlowupChart R t x)] [IsNoetherianRing (BlowupChart R x t)]
    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)) (hinf : (infinityPoint R t x).IsPrime)
    (s : State) (d : ℕ) (beta : BlowupRestriction R t x)
    (I : ∀ Q : divisorSupport Dv, Ideal (divisorLocalRing R t x e Dv hinf Q))
    (hI : ∀ Q : divisorSupport Dv, I Q ∈ childIdealSet R t x e Dv hinf s d Q)
    (hdir : ∀ φ, (directionPoint R t x e φ).IsMaximal ∧
      chartBase R t x t ∈ directionPoint R t x e φ ∧
      (chartSlope R t x ∈ directionPoint R t x e φ ↔ φ = zeroAffine (IsLocalRing.ResidueField R)))
    (hinj : Function.Injective (directionPoint R t x e))
    (hover : ∀ φ, φ ≠ zeroAffine (IsLocalRing.ResidueField R) →
      ((directionPoint R t x e φ).map
        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).IsMaximal ∧
      ((directionPoint R t x e φ).map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).comap
        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) = directionPoint R t x e φ)
    (hinfmax : (infinityPoint R t x).IsMaximal ∧ chartBase R x t x ∈ infinityPoint R t x ∧
      chartSlope R x t ∈ infinityPoint R t x)
    (htrL : ∀ (P : Ideal (BlowupChart R t x)) [P.IsMaximal], chartBase R t x t ∈ P →
      TransverseFiniteAt (BlowupChart R t x) P (chartBase R t x t))
    (htrR : ∀ (P : Ideal (BlowupChart R x t)) [P.IsMaximal], chartBase R x t x ∈ P →
      chartSlope R x t ∈ P → TransverseFiniteAt (BlowupChart R x t) P (chartBase R x t x)) :
    ∃ D : TwoChartCurveData R t x beta, MatchesDivisor e D Dv ∧ ∀ f : R,
      (∀ s : D.ι ⊕ D.ι0, strictTransformAt R t x (leftPoint D s) d (Ideal.span {f}) =
          Ideal.span {leftData D s}) →
      (∀ s : D.ι ⊕ D.ιinf, strictTransformAt R x t (rightPoint D s) d (Ideal.span {f}) =
          Ideal.span {rightData D s}) →
      ∀ Q : divisorSupport Dv, divisorStrictTransform R t x e Dv hinf
          d (Ideal.span {f}) Q = I Q := by
  set k := IsLocalRing.ResidueField R
  set alpha := algebraMap (BlowupChart R t x) (BlowupOverlap R t x)
  choose gen hgen using fun Q ↦ (hI Q).1
  have hlen : ∀ Q : divisorSupport Dv, Module.length (divisorLocalRing R t x e Dv hinf Q)
      (divisorLocalRing R t x e Dv hinf Q ⧸ (Ideal.span {gen Q} ⊔
        Ideal.span {divisorException R t x e Dv hinf Q})) = (Dv Q.val : ℕ∞) :=
    fun Q ↦ hgen Q ▸ (hI Q).2.1
  have hQmax : ∀ i : CommonDirections Dv, (commonPoint R t x e i).IsMaximal :=
    fun i ↦ (hover i.1 i.2.1).1
  have hcomap (i : CommonDirections Dv) : (commonPoint R t x e i).comap alpha =
      directionPoint R t x e i.1 := (hover i.1 i.2.1).2
  have hinfM : (infinityPoint R t x).IsMaximal := hinfmax.1
  have hdirM : ∀ φ, (directionPoint R t x e φ).IsMaximal := fun φ ↦ (hdir φ).1
  have := divisorSupport_finite Dv
  choose Φ hΦ using fun i : CommonDirections Dv ↦
    completed_point_transport_left R t x (commonPoint R t x e i)
  choose Ψ hΨ using fun i : CommonDirections Dv ↦
    completed_point_transport_right R t x beta (commonPoint R t x e i)
  -- `Θ i` identifies the completion at the overlap point `i` with the one at the chart point
  let Θ (i : CommonDirections Dv) := (Φ i).trans (completedLocalCast (hcomap i))
  have hΘ (i : CommonDirections Dv) (a) : Θ i (completedPointMap _ _ (alpha a)) =
      completedPointMap (BlowupChart R t x) (directionPoint R t x e i.1) a := by
    rw [RingEquiv.trans_apply, hΦ i a, completedLocalCast_completedPointMap]
  let gC (i : CommonDirections Dv) : CompletedLocalAt _ (directionPoint R t x e i.1) :=
    gen ⟨some i.1, i.2.2⟩
  have htrC (i : CommonDirections Dv) := @htrL (directionPoint R t x e i.1) (hdirM _)
    (hdir i.1).2.1 (gC i) _ (hlen ⟨some i.1, i.2.2⟩)
  have htr0 (l : {_u : Unit // 0 < Dv (zeroDirection k)}) := @htrL _ (hdirM (zeroAffine k))
    (hdir _).2.1 (gen ⟨zeroDirection k, l.2⟩) _ (hlen ⟨zeroDirection k, l.2⟩)
  have htrI (l : {_u : Unit // 0 < Dv none}) := @htrR (infinityPoint R t x) hinfM hinfmax.2.1
    hinfmax.2.2 (gen ⟨none, l.2⟩) _ (hlen ⟨none, l.2⟩)
  have he (i : CommonDirections Dv) : (Θ i).symm (completedPointMap _ _ (chartBase R t x t)) * 1 =
      completedPointMap _ (commonPoint R t x e i) (overlapException R t x) := by
    rw [mul_one, RingEquiv.symm_apply_eq]; exact (hΘ i _).symm
  have hM (i : CommonDirections Dv) :
      (IsLocalRing.maximalIdeal (Localization.AtPrime (commonPoint R t x e i))).map
        (localCompletionMap _) ≤
      ((IsLocalRing.maximalIdeal (Localization.AtPrime (directionPoint R t x e i.1))).map
        (localCompletionMap _)).map (Θ i).symm := by
    rw [Ideal.map_symm, ← Ideal.map_le_iff_le_comap,
      map_maximalIdeal_localCompletion (commonPoint R t x e i)]
    exact (map_maximalIdeal_localCompletion_transport alpha _ _ (Θ i) (hΘ i)).le
  let D : TwoChartCurveData R t x beta :=
    { ι := CommonDirections Dv
      fin := Finite.of_injective (β := divisorSupport Dv) (fun i ↦ ⟨some i.1, i.2.2⟩)
          fun i j h ↦ Subtype.ext (Option.some_injective _ (congrArg Subtype.val h))
      Q := commonPoint R t x e
      maximal := hQmax
      inj := fun i j h ↦ Subtype.ext <| hinj <|
        (hcomap i).symm.trans <| (congrArg (Ideal.comap alpha) h).trans (hcomap j)
      onE := fun i ↦ Ideal.mem_map_of_mem _ (hdir i.1).2.1
      g := fun i ↦ (Θ i).symm (gC i)
      transverse := fun i ↦ mul_injective_quotient_transport _ isUnit_one (he i) (htrC i).1
      finite := fun i ↦ exists_pow_le_span_pair_transport _ isUnit_one (he i) (hM i) (htrC i).2 1
      leftIso := Φ
      leftIso_compat := hΦ
      rightIso := Ψ
      rightIso_compat := hΨ
      ι0 := {_u : Unit // 0 < Dv (zeroDirection k)}
      P0 := fun _ ↦ directionPoint R t x e (zeroAffine k)
      maximal0 := fun _ ↦ hdirM _
      inj0 := fun a b _ ↦ Subsingleton.elim a b
      slope0 := fun _ ↦ ((hdir _).2.2).2 rfl
      onE0 := fun _ ↦ (hdir _).2.1
      g0 := fun l ↦ gen ⟨zeroDirection k, l.2⟩
      transverse0 := fun l ↦ (htr0 l).1
      finite0 := fun l ↦ (htr0 l).2
      ιinf := {_u : Unit // 0 < Dv none}
      Pinf := fun _ ↦ infinityPoint R t x
      maximalinf := fun _ ↦ hinfM
      injinf := fun a b _ ↦ Subsingleton.elim a b
      slopeinf := fun _ ↦ hinfmax.2.2
      onEinf := fun _ ↦ hinfmax.2.1
      ginf := fun l ↦ gen ⟨none, l.2⟩
      transverseinf := fun l ↦ (htrI l).1
      finiteinf := fun l ↦ (htrI l).2 }
  refine ⟨D, ⟨fun i ↦ ⟨i.1, i.2.1, rfl, ?_⟩, fun φ hφ hpos ↦ ⟨⟨φ, hφ, hpos⟩, rfl⟩,
    fun l ↦ ⟨rfl, length_finiteLocalCurveIdeal_toNat (P := directionPoint R t x e (zeroAffine k))
      _ _ _ (hlen ⟨zeroDirection k, l.2⟩)⟩, fun h ↦ ⟨⟨(), h⟩⟩,
    fun l ↦ ⟨rfl, length_finiteLocalCurveIdeal_toNat (P := infinityPoint R t x) _ _ _
      (hlen ⟨none, l.2⟩)⟩, fun h ↦ ⟨⟨(), h⟩⟩⟩, fun f hL hR ↦ ?_⟩
  · rw [← (two_chart_common_multiplicity_eq R t x beta D i).1]
    exact ((congrArg ENat.toNat (length_finiteLocalCurveIdeal_transport (Φ i) (hcomap i) (gC i)
      (chartBase R t x t) _ (hlen ⟨some i.1, i.2.2⟩))).trans (ENat.toNat_natCast _)).symm
  rintro ⟨_ | φ, hQ⟩
  · exact (hR (Sum.inr ⟨(), hQ⟩)).trans (hgen _).symm
  by_cases hφ : φ = zeroAffine k
  · subst hφ
    exact (hL (Sum.inr ⟨(), hQ⟩)).trans (hgen _).symm
  · exact (strictTransformAt_transport R t x (Φ ⟨φ, hφ, hQ⟩) (hcomap ⟨φ, hφ, hQ⟩) (gC ⟨φ, hφ, hQ⟩)
      d _ (hL (Sum.inl ⟨φ, hφ, hQ⟩))).trans (hgen _).symm

private theorem directionPoint_overlap_facts (O R : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]
    (S : SurfaceData O R) (t x : R) (ht : S.t = t) (hx : S.x = x)
    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))
    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =
      Polynomial.C (IsLocalRing.residue R r))
    (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)
    (φ : AffineDirection (IsLocalRing.ResidueField R))
    (hφ : φ ≠ zeroAffine (IsLocalRing.ResidueField R)) :
    ((directionPoint R t x e φ).map
        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).IsMaximal ∧
      ((directionPoint R t x e φ).map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).comap
        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) = directionPoint R t x e φ := by
  subst ht hx
  obtain ⟨h1, -, h2⟩ := direction_point_overlap_maximal O R S e he heZ φ hφ
  exact ⟨h1, h2⟩

private theorem infinityPoint_facts (O R : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]
    (S : SurfaceData O R) (t x : R) (ht : S.t = t) (hx : S.x = x) :
    (infinityPoint R t x).IsMaximal ∧ chartBase R x t x ∈ infinityPoint R t x ∧
      chartSlope R x t ∈ infinityPoint R t x := by
  subst ht hx
  obtain ⟨h1, h2, h3, -⟩ := infinity_point_maximal O R S
  exact ⟨h1, h2, h3⟩

private theorem length_quot_span_one_sup {A : Type} [CommRing A] (P : Ideal A) [P.IsPrime]
    (y : CompletedLocalAt A P) :
    Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸
      (Ideal.span {(1 : CompletedLocalAt A P)} ⊔ Ideal.span {y})) = ((0 : ℕ) : ℕ∞) := by
  rw [Ideal.span_singleton_one, top_sup_eq, Nat.cast_zero, Module.length_eq_zero_iff]
  exact Ideal.Quotient.subsingleton_iff.mpr rfl

/-- Every family of child ideals over the support of `Dv` is realized by a two-chart curve datum
matching `Dv`: any global function with the prescribed chart strict transforms has strict
transform `I Q` at every point `Q`. -/
theorem child_ideals_curve_datum (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)
    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)
        [IsLocalRing (ConcreteSurface O pi u a b)]
    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+* Polynomial (IsLocalRing.ResidueField
        (ConcreteSurface O pi u a b)))
    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)
        (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))
    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
        (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ)
    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
        (surfaceX O pi u a b))
    (I : ∀ Q : divisorSupport Dv, Ideal (divisorLocalRing (ConcreteSurface O pi u a b)
        (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf Q))
    (hI : ∀ Q : divisorSupport Dv, I Q ∈ childIdealSet (ConcreteSurface O pi u a b)
        (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf s d Q) :
    ∃ D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)
        beta, MatchesDivisor e D Dv ∧ ∀ f : ConcreteSurface O pi u a b,
      (∀ s : D.ι ⊕ D.ι0,
        strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)
            (leftPoint D s) d (Ideal.span {f}) = Ideal.span {leftData D s}) →
      (∀ s : D.ι ⊕ D.ιinf, strictTransformAt (ConcreteSurface O pi u a b) (surfaceX O pi u a b)
          (surfaceT O pi u a b) (rightPoint D s) d (Ideal.span {f}) =
        Ideal.span {rightData D s}) →
      ∀ Q : divisorSupport Dv, divisorStrictTransform (ConcreteSurface O pi u a b)
          (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf d (Ideal.span {f}) Q =
        I Q := by
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)
      (surfaceX O pi u a b)
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)
      (surfaceT O pi u a b)
  obtain ⟨hDom, hReg, S, -, hSt, hSx, -⟩ :=
    concrete_surface_data_exists_unconditional O pi hpi u a b ha
  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set
      (ConcreteSurface O pi u a b))).IsMaximal :=
    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha
  obtain ⟨hdir, hinj, -⟩ := directionPoint_properties _ _ _ e he heZ
  have hinfmax := infinityPoint_facts O _ S _ _ hSt hSx
  refine child_ideals_curve_datum_of_points _ _ _ e Dv hinf s d beta I hI
    (fun φ ↦ ⟨(hdir φ).1, (hdir φ).2.1, (hdir φ).2.2.1⟩) hinj
    (directionPoint_overlap_facts O _ S _ _ hSt hSx e he heZ) hinfmax
    (fun P _ hP g n hg ↦ ?_) (fun P _ hP hW g n hg ↦ ?_)
  · have := @child_ideal_generator_transverse_finite O _ _ _ _ _ pi hpi u a b ha P _ _ hP g n hg
      (infinityPoint _ _ _) hinfmax.1 hinfmax.1.isPrime hinfmax.2.1 hinfmax.2.2 1
      0 (length_quot_span_one_sup _ _)
    exact ⟨this.1.1, this.1.2.2⟩
  · have := @child_ideal_generator_transverse_finite O _ _ _ _ _ pi hpi u a b ha
      (directionPoint _ _ _ e (zeroAffine _)) (hdir _).1 (hdir _).1.isPrime (hdir _).2.1 1 0
      (length_quot_span_one_sup _ _) P _ _ hP hW g n hg
    exact ⟨this.2.1, this.2.2.2⟩

/-- For a curve datum built from `f = ∑ cᵢ tᵈ⁻ⁱ xⁱ` with residue form `H` of divisor `Dv`, the
common points are nonzero affine directions with the right multiplicities, and the zero-slope
points sit at the zero direction with multiplicity `Dv 0`. -/
private theorem curve_datum_common_and_zero_clauses (O : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]
    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)
    (a b : ℕ) (ha : 0 < a) (d : ℕ) (c : Fin (d + 1) → ConcreteSurface O pi u a b)
    [IsLocalRing (ConcreteSurface O pi u a b)]
    (H : Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (hH : HasHomogeneousDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) d H Dv)
    (hcH : ∀ i : Fin (d+1), IsLocalRing.residue (ConcreteSurface O pi u a b) (c i) = H.coeff i.val)
    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+*
      Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)
      (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))
    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)
    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
      (surfaceX O pi u a b))
    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)
      beta)
    (hleft : ∀ s : D.ι ⊕ D.ι0,
      leftData D s = completedPointMap (tChart O pi u a b) (leftPoint D s)
        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *
            tSlope O pi u a b^i.val) ∧
      (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *
          tSlope O pi u a b^i.val) ∈ leftPoint D s) :
    (∀ i : D.ι, ∃ φ : AffineDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)),
      φ ≠ zeroAffine (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) ∧
      D.Q i = (directionPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
          (surfaceX O pi u a b) e φ).map (algebraMap (tChart O pi u a b) (tOverlap O pi u a b)) ∧
      Dv (some φ) = commonMultiplicity D i) ∧
    ∀ k : D.ι0, D.P0 k = directionPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
        (surfaceX O pi u a b) e
          (zeroAffine (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) ∧
      Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) =
        leftMultiplicity D (Sum.inr k) := by
  have hmax : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set
      (ConcreteSurface O pi u a b))).IsMaximal :=
    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha
  have hne : ∃ i : Fin (d+1), c i ∉ Ideal.span {surfaceT O pi u a b, surfaceX O pi u a b} := by
    obtain ⟨j, hj⟩ : ∃ j, H.coeff j ≠ 0 := by
      by_contra! h; exact hH.1 (Polynomial.ext h)
    have hjd : j < d + 1 := Nat.lt_succ_of_le ((Polynomial.le_natDegree_of_ne_zero hj).trans hH.2.1)
    refine ⟨⟨j, hjd⟩, fun hmem ↦ hj ?_⟩
    rw [← hcH ⟨j, hjd⟩]
    exact (IsLocalRing.residue_eq_zero_iff _).2 (IsLocalRing.le_maximalIdeal hmax.ne_top hmem)
  have hHBAR := reduced_form_eq_of_residue_coeff (ConcreteSurface O pi u a b) d c H hH.2.1 hcH
  have hlc : H.leadingCoeff ≠ 0 := Polynomial.leadingCoeff_ne_zero.2 hH.1
  obtain ⟨hlm, -, hlt⟩ := two_chart_left_points_maximal _ _ _ beta D
  have : ∀ s, (leftPoint D s).IsMaximal := hlm
  have mult (s : D.ι ⊕ D.ι0) (φ : AffineDirection (IsLocalRing.ResidueField
      (ConcreteSurface O pi u a b)))
      (hPφ : ((leftPoint D s).map (Ideal.Quotient.mk (tExc O pi u a b))).map e = Ideal.span
          {φ.val}) :
      Dv (some φ) = leftMultiplicity D s := by
    unfold leftMultiplicity leftLevelIdeal finiteLocalCurveIdeal
    rw [(hleft s).1, pow_one, concrete_strict_transform_multiplicity O pi hpi u a b ha d c hne
      (leftPoint D s) (hlt s) e he heZ φ.val φ.property hPφ, hHBAR, ENat.toNat_natCast]
    conv_rhs => rw [hH.2.2.2]
    exact ((count_normalizedFactors_divisorAffinePolynomial _ Dv _ hlc φ).1).symm
  refine ⟨fun i ↦ ?_, fun k ↦ ?_⟩
  · obtain ⟨φ, hφ, himg, hslope⟩ :=
      chart_point_eq_directionPoint _ _ _ e he heZ (leftPoint D (Sum.inl i)) (hlt (Sum.inl i))
    have hZ := (overlap_exceptional_point_comap_maximal _ _ _ (D.Q i) (D.onE i)).2.1
    refine ⟨φ, fun h0 ↦ hZ (hslope.2 h0), ?_, ?_⟩
    · rw [← show leftPoint D (Sum.inl i) = _ from hφ]
      exact (IsLocalization.map_under (Submonoid.powers (tSlope O pi u a b)) _ (D.Q i)).symm
    · rw [mult (Sum.inl i) φ himg]
      exact (two_chart_common_multiplicity_eq _ _ _ beta D i).1
  · obtain ⟨φ, hφ, himg, hslope⟩ :=
      chart_point_eq_directionPoint _ _ _ e he heZ (leftPoint D (Sum.inr k)) (hlt (Sum.inr k))
    obtain rfl : φ = zeroAffine _ := hslope.1 (D.slope0 k)
    exact ⟨hφ, mult (Sum.inr k) _ himg⟩

/-- A curve datum built from `f = ∑ cᵢ tᵈ⁻ⁱ xⁱ`, whose residue form has divisor `Dv`, matches
`Dv`. -/
private theorem curve_datum_matches_divisor (O : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]
    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)
    (a b : ℕ) (ha : 0 < a) (d : ℕ) (f : ConcreteSurface O pi u a b)
    (c : Fin (d + 1) → ConcreteSurface O pi u a b)
    (hc : f = ∑ i : Fin (d + 1), c i * surfaceT O pi u a b ^ (d - i.val) *
      surfaceX O pi u a b ^ i.val)
    [IsLocalRing (ConcreteSurface O pi u a b)]
    (H : Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (hH : HasHomogeneousDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) d H Dv)
    (hcH : ∀ i : Fin (d+1), IsLocalRing.residue (ConcreteSurface O pi u a b) (c i) = H.coeff i.val)
    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+*
      Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)
      (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))
    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)
    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
      (surfaceX O pi u a b))
    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)
      beta)
    (hleft : ∀ s : D.ι ⊕ D.ι0, leftData D s = completedPointMap (tChart O pi u a b) (leftPoint D s)
      (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *
        tSlope O pi u a b^i.val) ∧ (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)
          (tChart O pi u a b) (c i) * tSlope O pi u a b^i.val) ∈ leftPoint D s)
    (hleftsurj : ∀ P : Ideal (tChart O pi u a b), P.IsMaximal →
      tBase O pi u a b (surfaceT O pi u a b) ∈ P → (∑ i : Fin (d+1), algebraMap
        (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) * tSlope O pi u a b^i.val) ∈ P →
      ∃ s : D.ι ⊕ D.ι0, leftPoint D s = P)
    (hright : ∀ s : D.ι ⊕ D.ιinf, Ideal.span {rightData D s} = Ideal.span {completedPointMap
      (xChart O pi u a b) (rightPoint D s) (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)
        (xChart O pi u a b) (c i) * xSlope O pi u a b^(d - i.val))} ∧ (∑ i : Fin (d+1), algebraMap
          (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) * xSlope O pi u a b^(d - i.val)) ∈
        rightPoint D s)
    (hrightsurj : ∀ P : Ideal (xChart O pi u a b), P.IsMaximal →
      xBase O pi u a b (surfaceX O pi u a b) ∈ P → (∑ i : Fin (d+1), algebraMap
        (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) * xSlope O pi u a b^(d - i.val)) ∈
          P → ∃ s : D.ι ⊕ D.ιinf, rightPoint D s = P) :
    MatchesDivisor e D Dv := by
  have h1 := curve_datum_common_and_zero_clauses O pi hpi u a b ha d c H Dv hH hcH e he heZ beta D
    hleft
  have h2 := curve_datum_surj_and_inf_clauses O pi hpi u a b ha d f c hc H Dv hH hcH e he heZ beta D
    hleft hleftsurj hright hrightsurj
  exact ⟨h1.1, h2.1, h1.2, h2.2.1, h2.2.2.1, h2.2.2.2⟩

/-- If a two-chart curve datum matches the divisor `Dv`, the degree of `Dv` is the curve datum
degree. -/
theorem matches_divisor_degree (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R] (S : SurfaceData O R)
    (beta : BlowupRestriction R S.t S.x) (D : TwoChartCurveData R S.t S.x beta)
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))
    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*
      Polynomial (IsLocalRing.ResidueField R))
    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =
      Polynomial.C (IsLocalRing.residue R r))
    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)
    (hm : MatchesDivisor e D Dv) [IsNoetherianRing (BlowupChart R S.t S.x)]
    [IsNoetherianRing (BlowupChart R S.x S.t)] :
    exceptionalDegree (IsLocalRing.ResidueField R) Dv = curveDataDegree D := by
  classical
  set F := IsLocalRing.ResidueField R
  have hP := direction_point_maximal O R S e he heZ
  have hO := direction_point_overlap_maximal O R S e he heZ
  have hinjdir : Function.Injective (directionPoint R S.t S.x e) := (hP (zeroAffine F)).2.2.2.2.2
  choose φ hφ0 hφQ hφm using hm.common
  have hleft (i) : leftPoint D (Sum.inl i) = directionPoint R S.t S.x e (φ i) := by
    change (D.Q i).comap _ = _
    rw [hφQ i]; exact (hO (φ i) (hφ0 i)).2.2
  have hφinj : Function.Injective φ := fun i j h ↦ D.inj (by rw [hφQ i, hφQ j, h])
  have hsurj : ∀ ψ : AffineDirection F, ψ ≠ zeroAffine F → 0 < Dv (some ψ) → ∃ i, φ i = ψ := by
    intro ψ hψ hpos
    obtain ⟨i, hi⟩ := hm.common_surj ψ hψ hpos
    refine ⟨i, hinjdir ?_⟩
    rw [← hleft i]
    change (D.Q i).comap _ = _
    rw [hi]; exact (hO ψ hψ).2.2
  have hdeg (ψ : AffineDirection F) :
      (Module.length R (BlowupChart R S.t S.x ⧸ directionPoint R S.t S.x e ψ)).toNat =
        ψ.val.natDegree := by
    rw [(hP ψ).2.2.2.2.1]; rfl
  have : Fintype D.ι := Fintype.ofFinite _
  have : Fintype D.ι0 := Fintype.ofFinite _
  have : Fintype D.ιinf := Fintype.ofFinite _
  unfold curveDataDegree
  rw [finsum_eq_sum_of_fintype, finsum_eq_sum_of_fintype, Fintype.sum_sum_type]
  have hc : ∀ i, leftResidueDegree D (Sum.inl i) * leftMultiplicity D (Sum.inl i) =
      directionDegree F (some (φ i)) * Dv (some (φ i)) := by
    intro i
    unfold leftResidueDegree
    rw [hleft i, hdeg, (two_chart_common_multiplicity_eq R _ _ beta D i).1, hφm i]
    rfl
  have hz : ∑ k : D.ι0, leftResidueDegree D (Sum.inr k) * leftMultiplicity D (Sum.inr k) =
      directionDegree F (zeroDirection F) * Dv (zeroDirection F) := by
    by_cases hne : Nonempty D.ι0
    · obtain ⟨k⟩ := hne
      have : Subsingleton D.ι0 := ⟨fun a b => D.inj0 ((hm.zero a).1.trans (hm.zero b).1.symm)⟩
      rw [Fintype.sum_subsingleton _ k]
      unfold leftResidueDegree
      change (Module.length R (BlowupChart R S.t S.x ⧸ D.P0 k)).toNat * _ = _
      rw [(hm.zero k).1, hdeg, ← (hm.zero k).2]
      rfl
    · have h0 : Dv (zeroDirection F) = 0 := by
        by_contra h; exact hne (hm.zero_surj (Nat.pos_of_ne_zero h))
      rw [h0, mul_zero]
      have : IsEmpty D.ι0 := not_nonempty_iff.mp hne
      simp
  have hi : ∑ l : D.ιinf, rightMultiplicity D (Sum.inr l) =
      directionDegree F none * Dv none := by
    by_cases hne : Nonempty D.ιinf
    · obtain ⟨l⟩ := hne
      have : Subsingleton D.ιinf := ⟨fun a b => D.injinf ((hm.inf a).1.trans (hm.inf b).1.symm)⟩
      rw [Fintype.sum_subsingleton _ l, ← (hm.inf l).2]
      change _ = 1 * _
      rw [one_mul]
    · have h0 : Dv none = 0 := by
        by_contra h; exact hne (hm.inf_surj (Nat.pos_of_ne_zero h))
      rw [h0, mul_zero]
      have : IsEmpty D.ιinf := not_nonempty_iff.mp hne
      simp
  rw [Finset.sum_congr rfl (fun i _ => hc i), hz, hi]
  have hz1 : ∀ i, (some (φ i) : ClosedDirection F) ≠ zeroDirection F := by
    intro i h
    exact hφ0 i (Option.some_injective _ h)
  unfold exceptionalDegree
  rw [Finsupp.sum_of_support_subset Dv (s := insert none (insert (zeroDirection F)
      (Finset.univ.image (fun i => (some (φ i) : ClosedDirection F))))) ?_ _ (by simp)]
  · rw [Finset.sum_insert (by simp [zeroDirection]), Finset.sum_insert (by simpa using hz1),
      Finset.sum_image (fun a _ b _ h => hφinj (Option.some_injective _ h))]
    ring
  · intro P hPm
    rw [Finsupp.mem_support_iff] at hPm
    rcases P with _ | ψ
    · simp
    · by_cases hψ : ψ = zeroAffine F
      · subst hψ; simp [zeroDirection, zeroAffine]
      · obtain ⟨i, rfl⟩ := hsurj ψ hψ (Nat.pos_of_ne_zero hPm)
        simp

/-- Every ideal `J` of the fixed tangent cell is principal, generated by a degree-`d` form `f`
whose chart strict transforms define a two-chart curve datum matching `Dv` of degree `deg Dv`. -/
theorem fixed_tangent_cell_curve_datum (O : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]
    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)
    (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]
        [IsRegularLocalRing (ConcreteSurface O pi u a b)] (S : SurfaceData O
            (ConcreteSurface O pi u a b))
    (hS : S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b) (e :
        (tChart O pi u a b ⧸ tExc O pi u a b) ≃+* Polynomial (IsLocalRing.ResidueField
            (ConcreteSurface O pi u a b)))
    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)
        (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))
    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) (s : State)
        (d : ℕ) (J : Ideal (ConcreteSurface O pi u a b))
    (hJ : J ∈ fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv)
        (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
            (surfaceX O pi u a b)) :
    ∃ (f : ConcreteSurface O pi u a b) (c : Fin (d+1) → ConcreteSurface O pi u a b)
        (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
            (surfaceX O pi u a b) beta), J = Ideal.span {f} ∧
      f = ∑ i : Fin (d+1), c i * surfaceT O pi u a b^(d - i.val) * surfaceX O pi u a b^i.val ∧
      (∀ s : D.ι ⊕ D.ι0,
        leftData D s = completedPointMap (tChart O pi u a b) (leftPoint D s)
          (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *
              tSlope O pi u a b^i.val) ∧
        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *
            tSlope O pi u a b^i.val) ∈ leftPoint D s) ∧
      (∀ s : D.ι ⊕ D.ιinf,
        Ideal.span {rightData D s} = Ideal.span {completedPointMap (xChart O pi u a b)
            (rightPoint D s)
          (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *
              xSlope O pi u a b^(d - i.val))} ∧
        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *
            xSlope O pi u a b^(d - i.val)) ∈ rightPoint D s) ∧
      (∀ s : D.ι ⊕ D.ι0,
        strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)
            (leftPoint D s) d J = Ideal.span {leftData D s}) ∧
      (∀ s : D.ι ⊕ D.ιinf,
        strictTransformAt (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)
            (rightPoint D s) d J = Ideal.span {rightData D s}) ∧
      MatchesDivisor e D Dv ∧
      curveDataDegree D = exceptionalDegree (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))
          Dv := by
  obtain ⟨ht, hx⟩ := hS
  cases S with | mk a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15
  dsimp only at ht hx
  subst ht hx
  obtain ⟨f, c, H, hJf, hf, hH, hcH, hne⟩ :=
    fixed_tangent_cell_generator_coefficients O _ _ s d Dv J hJ
  obtain ⟨D, hl, hls, hr, hrs, hst1, hst2⟩ :=
    curve_datum_of_parent_function O pi hpi u a b ha d f c hf hne beta
  have hm : MatchesDivisor e D Dv :=
    curve_datum_matches_divisor O pi hpi u a b ha d f c hf H Dv hH hcH e he heZ beta D hl hls hr hrs
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)
      (surfaceX O pi u a b)
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)
      (surfaceT O pi u a b)
  have hd := matches_divisor_degree O (ConcreteSurface O pi u a b)
    ⟨a1, a2, surfaceT O pi u a b, surfaceX O pi u a b, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14,
        a15⟩ beta D Dv e he heZ hm
  subst hJf
  exact ⟨f, c, D, rfl, hf, hl, hr, hst1, hst2, hm, hd.symm⟩

/-- **Level-one kernels on a blow-up chart.** Let `e` identify the exceptional line of the chart
`R[x/t]` with `k[X]` (`k = R ⧸ I`, `I = (t, x)`), and let `P s` be finitely many distinct
closed points of the exceptional line carrying finite-length level-one curve data `g s`. Then the
points correspond to distinct monic irreducibles `φ s` (with `φ s = X` exactly at the points where
the slope vanishes, and `deg φ s` the residue degree), the level-one lengths are finite numbers
`m s`, and the intersection of the contracted level-one ideals maps to `(∏ φ s ^ m s)`. -/
theorem level_one_kernel_polynomial (R : Type) [CommRing R] (t x : R) (I : Ideal R) [I.IsMaximal]
    (hI : Ideal.span ({t,x} : Set R) = I) [IsNoetherianRing (BlowupChart R t x)]
    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (R ⧸ I))
    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =
      Polynomial.C (Ideal.Quotient.mk I r))
    (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)
    {ι : Type} [Finite ι] (P : ι → Ideal (BlowupChart R t x)) [∀ s, (P s).IsMaximal]
    (hinjP : Function.Injective P) (htP : ∀ s, chartBase R t x t ∈ P s)
    (g : ∀ s, CompletedLocalAt (BlowupChart R t x) (P s))
    (hfin : ∀ s, ∃ L : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P s))).map
      (localCompletionMap (Localization.AtPrime (P s))))^L ≤
      finiteLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1) :
    ∃ (φ : ι → Polynomial (R ⧸ I)) (m : ι → ℕ), (∀ s, (φ s).Monic ∧ Irreducible (φ s)) ∧
      Function.Injective φ ∧ (∀ s, chartSlope R t x ∈ P s ↔ φ s = Polynomial.X) ∧
      (∀ s, Module.length R (BlowupChart R t x ⧸ P s) = ((φ s).natDegree : ℕ∞)) ∧
      (∀ s, Module.length (CompletedLocalAt (BlowupChart R t x) (P s))
        (CompletedLocalAt (BlowupChart R t x) (P s) ⧸
          finiteLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1) =
        (m s : ℕ∞)) ∧
      ((⨅ s, contractedLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1).map
        (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {∏ᶠ s, φ s ^ m s} := by
  subst hI
  choose φ hmon hirr hφ hslope hlen using fun s ↦
    blowup_chart_exceptional_point_polynomial R t x e he heZ (P s) (htP s)
  -- the exceptional ideal lies in each point and in each contracted ideal
  have hker_le (J : Ideal (BlowupChart R t x)) (hJ : chartBase R t x t ∈ J) :
      (J.map (Ideal.Quotient.mk (chartExceptional R t x))).comap
        (Ideal.Quotient.mk (chartExceptional R t x)) = J := by
    rw [Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot,
      Ideal.mk_ker]
    refine sup_eq_left.mpr ?_
    unfold chartExceptional
    rw [Ideal.span_le]; simpa using hJ
  have hemap_inj (J J' : Ideal (BlowupChart R t x ⧸ chartExceptional R t x))
      (h : J.map e = J'.map e) : J = J' := by
    rw [← Ideal.comap_map_of_bijective e e.bijective (I := J),
      ← Ideal.comap_map_of_bijective e e.bijective (I := J'), h]
  have hinj : Function.Injective φ := fun s s' h ↦ hinjP <| by
    rw [← hker_le _ (htP s), ← hker_le _ (htP s'), hemap_inj _ _ ((hφ s).trans (h ▸ (hφ s').symm))]
  -- multiplicities
  have hpow : ∀ s, ∃ r : ℕ, ((contractedLocalCurveIdeal (BlowupChart R t x) (P s)
      (chartBase R t x t) (g s) 1).map (Ideal.Quotient.mk (chartExceptional R t x))).map e =
        Ideal.span {φ s ^ r} ∧
      Module.length (CompletedLocalAt (BlowupChart R t x) (P s))
        (CompletedLocalAt (BlowupChart R t x) (P s) ⧸
          finiteLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1) =
        (r : ℕ∞) := fun s => by
    obtain ⟨L, hL⟩ := hfin s
    obtain ⟨r, -, hr, hrlen⟩ := contracted_level_one_ideal_is_irreducible_power R t x e
      (P s) (φ s) (hφ s) (hirr s) (g s) L hL
    exact ⟨r, hr, hrlen⟩
  choose m hmult hm using hpow
  refine ⟨φ, m, fun s => ⟨hmon s, hirr s⟩, hinj, hslope, hlen, hm, ?_⟩
  set J : ι → Ideal (BlowupChart R t x) := fun s =>
    contractedLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1
  have hJt : ∀ s, chartBase R t x t ∈ J s := by
    intro s
    change completedPointMap (BlowupChart R t x) (P s) (chartBase R t x t) ∈
      finiteLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1
    unfold finiteLocalCurveIdeal
    exact Ideal.subset_span (by simp)
  have h1 : (⨅ s, J s).map (Ideal.Quotient.mk (chartExceptional R t x)) =
      ⨅ s, (J s).map (Ideal.Quotient.mk (chartExceptional R t x)) := by
    rw [show (⨅ s, J s) = ⨅ s, ((J s).map (Ideal.Quotient.mk (chartExceptional R t x))).comap
        (Ideal.Quotient.mk (chartExceptional R t x)) from
        iInf_congr (fun s => (hker_le _ (hJt s)).symm)]
    exact Ideal.map_iInf_comap_of_surjective _ Ideal.Quotient.mk_surjective _
  have h2 (K : ι → Ideal (BlowupChart R t x ⧸ chartExceptional R t x)) :
      (⨅ s, K s).map e = ⨅ s, (K s).map e := by
    rw [show (⨅ s, K s) = ⨅ s, ((K s).map e).comap e from
        iInf_congr (fun s => (Ideal.comap_map_of_bijective e e.bijective).symm)]
    exact Ideal.map_iInf_comap_of_surjective _ e.surjective _
  let _ : Fintype ι := Fintype.ofFinite _
  rw [h1, h2, iInf_congr hmult, finprod_eq_prod_of_fintype]
  let _ := Ideal.Quotient.field (Ideal.span ({t,x} : Set R))
  exact pairwise_distinct_irreducible_pow_iInf (R ⧸ Ideal.span ({t,x} : Set R)) ι φ hmon hirr hinj m

/-- The level-one left kernel, transported to `k[X]` along an identification of the exceptional
line, is generated by `∏ φₛ ^ multₛ` for distinct monic irreducibles `φₛ`, with `φ = X`
exactly at the zero-slope points. -/
theorem two_chart_left_level_one_kernel_polynomial (R : Type) [CommRing R] (t x : R)
    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)
    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]
    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+*
      Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))
    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =
      Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r))
    (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X) :
    ∃ φ : D.ι ⊕ D.ι0 → Polynomial (R ⧸ Ideal.span ({t,x} : Set R)),
        (∀ s, (φ s).Monic ∧ Irreducible (φ s)) ∧ Function.Injective φ ∧
        (∀ i, φ (Sum.inl i) ≠ Polynomial.X) ∧ (∀ k, φ (Sum.inr k) = Polynomial.X) ∧
        (∀ s, (φ s).natDegree = leftResidueDegree D s) ∧ (∀ k, leftResidueDegree D (Sum.inr k) = 1)
        ∧ ((leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R t x))).map e =
        Ideal.span {∏ᶠ s, φ s ^ leftMultiplicity D s} := by
  obtain ⟨hmax, hinjP, htP⟩ := two_chart_left_points_maximal R t x beta D
  obtain ⟨φ, m, hφ, hinj, hslope, hlen, hm, hker⟩ := level_one_kernel_polynomial R t x _ rfl e he
    heZ (leftPoint D) hinjP htP (leftData D)
    (two_chart_left_data_transverse_finite R t x beta D 1).2
  have hmult : leftMultiplicity D = m := funext fun s => by
    unfold leftMultiplicity leftLevelIdeal; rw [hm s]; rfl
  have hdeg : ∀ s, (φ s).natDegree = leftResidueDegree D s := by
    intro s; unfold leftResidueDegree; rw [hlen s]; rfl
  have hX : ∀ k, φ (Sum.inr k) = Polynomial.X := fun k => (hslope (Sum.inr k)).1 (D.slope0 k)
  refine ⟨φ, hφ, hinj, fun i hi => ?_, hX, hdeg, fun k => ?_, by rw [hmult]; exact hker⟩
  · have hQ := D.onE i
    have := D.maximal i
    exact (overlap_exceptional_point_comap_maximal R t x (D.Q i) hQ).2.1 ((hslope (Sum.inl i)).2 hi)
  · rw [← hdeg, hX]; exact Polynomial.natDegree_X

private noncomputable def restrictLeftData {R : Type} [CommRing R] {t x : R}
    {beta : BlowupRestriction R t x}
    (D : TwoChartCurveData R t x beta) (p : D.ι → Prop) (q : D.ι0 → Prop) :
    TwoChartCurveData R t x beta where
  ι := {i // p i}
  fin := inferInstance
  Q := fun i => D.Q i.1
  maximal := fun i => D.maximal i.1
  inj := fun _ _ h => Subtype.ext (D.inj h)
  onE := fun i => D.onE i.1
  g := fun i => D.g i.1
  transverse := fun i => D.transverse i.1
  finite := fun i => D.finite i.1
  leftIso := fun i => D.leftIso i.1
  leftIso_compat := fun i => D.leftIso_compat i.1
  rightIso := fun i => D.rightIso i.1
  rightIso_compat := fun i => D.rightIso_compat i.1
  ι0 := {k // q k}
  fin0 := inferInstance
  P0 := fun k => D.P0 k.1
  maximal0 := fun k => D.maximal0 k.1
  inj0 := fun _ _ h => Subtype.ext (D.inj0 h)
  slope0 := fun k => D.slope0 k.1
  onE0 := fun k => D.onE0 k.1
  g0 := fun k => D.g0 k.1
  transverse0 := fun k => D.transverse0 k.1
  finite0 := fun k => D.finite0 k.1
  ιinf := D.ιinf
  fininf := D.fininf
  Pinf := D.Pinf
  maximalinf := D.maximalinf
  injinf := D.injinf
  slopeinf := D.slopeinf
  onEinf := D.onEinf
  ginf := D.ginf
  transverseinf := D.transverseinf
  finiteinf := D.finiteinf

private theorem leftKernel_le_restrictLeftData {R : Type} [CommRing R] {t x : R}
    {beta : BlowupRestriction R t x}
    (D : TwoChartCurveData R t x beta) (p : D.ι → Prop) (q : D.ι0 → Prop) :
    leftKernel D 1 ≤ leftKernel (restrictLeftData D p q) 1 := by
  unfold leftKernel finiteSupportKernel
  refine le_iInf ?_
  rintro (i | k)
  exacts [iInf_le _ (Sum.inl i.1), iInf_le _ (Sum.inr k.1)]

private theorem left_kernel_polynomial_residueField (O R : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]
    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x) (D : TwoChartCurveData R S.t S.x
      beta) (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*
      Polynomial (IsLocalRing.ResidueField R))
    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =
      Polynomial.C (IsLocalRing.residue R r))
    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)
    [IsNoetherianRing (BlowupChart R S.t S.x)] :
    ∃ ψ : D.ι ⊕ D.ι0 → Polynomial (IsLocalRing.ResidueField R),
        (∀ s, (ψ s).Monic ∧ Irreducible (ψ s)) ∧ (∀ s, (ψ s).natDegree = leftResidueDegree D s) ∧
      ((leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R S.t S.x))).map e =
          Ideal.span {∏ᶠ s, ψ s ^ leftMultiplicity D s} := by
  have : (Ideal.span ({S.t, S.x} : Set R)).IsMaximal := by
    rw [S.parameters]; exact IsLocalRing.maximalIdeal.isMaximal R
  let κ : (R ⧸ Ideal.span ({S.t, S.x} : Set R)) ≃+* IsLocalRing.ResidueField R :=
    Ideal.quotEquivOfEq S.parameters
  let e₀ := e.trans (Polynomial.mapEquiv κ).symm
  have he₀ : ∀ r : R, e₀ (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =
      Polynomial.C (Ideal.Quotient.mk (Ideal.span ({S.t,S.x} : Set R)) r) := by
    intro r
    simp only [e₀, RingEquiv.trans_apply, he]
    rw [Polynomial.mapEquiv_symm_apply, Polynomial.map_C]
    congr 1
  have heZ₀ : e₀ (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) =
      Polynomial.X := by
    simp only [e₀, RingEquiv.trans_apply, heZ]
    rw [Polynomial.mapEquiv_symm_apply, Polynomial.map_X]
  obtain ⟨φ, hφ, -, -, -, hdeg, -, hK⟩ :=
    two_chart_left_level_one_kernel_polynomial R S.t S.x beta D e₀ he₀ heZ₀
  refine ⟨fun s => (φ s).map (κ : _ →+* _), fun s => ⟨(hφ s).1.map _, ?_⟩, fun s => ?_, ?_⟩
  · exact (MulEquiv.irreducible_iff (Polynomial.mapEquiv κ).toMulEquiv).2 (hφ s).2
  · rw [Polynomial.natDegree_map_eq_of_injective κ.injective, hdeg]
  · have hmap : ∀ I : Ideal (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x),
        I.map e = (I.map e₀).map (Polynomial.mapEquiv κ) := by
      intro I
      rw [← Ideal.map_coe e, ← Ideal.map_coe e₀, ← Ideal.map_coe (Polynomial.mapEquiv κ),
          Ideal.map_map]
      congr 1
      exact RingHom.ext fun a => by
        simp only [e₀, RingHom.coe_comp, Function.comp_apply, RingEquiv.coe_toRingHom,
          RingEquiv.trans_apply, RingEquiv.apply_symm_apply]
    rw [hmap, hK, Ideal.map_span, Set.image_singleton]
    congr 2
    have : Fintype (D.ι ⊕ D.ι0) := Fintype.ofFinite _
    rw [finprod_eq_prod_of_fintype, finprod_eq_prod_of_fintype, map_prod]
    simp [Polynomial.mapEquiv_apply, Polynomial.map_pow]

private theorem pow_le_comap_completedPointMap (A : Type) [CommRing A] (P : Ideal A) [P.IsPrime]
    (J : Ideal (CompletedLocalAt A P)) (L : ℕ)
    (hL : ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map
        (localCompletionMap (Localization.AtPrime P))) ^ L ≤ J) :
    P^L ≤ J.comap (completedPointMap A P) := by
  rw [← Ideal.map_le_iff_le_comap, Ideal.map_pow]
  refine le_trans (le_of_eq ?_) hL
  congr 1
  unfold completedPointMap
  rw [← Ideal.map_map, Localization.AtPrime.map_eq_maximalIdeal]

/-- The image in `k[X]` of the level-one left kernel lies in `(ψ₀ ^ mult s₀)` whenever the left
point `s₀` is the direction point of `ψ₀`; proved by restricting `D` to the point `s₀`. -/
private theorem left_kernel_map_le_span_direction_pow (O R : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]
    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x)
    (D : TwoChartCurveData R S.t S.x beta)
    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*
      Polynomial (IsLocalRing.ResidueField R))
    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =
      Polynomial.C (IsLocalRing.residue R r))
    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)
    [IsNoetherianRing (BlowupChart R S.t S.x)] (s₀ : D.ι ⊕ D.ι0)
    (ψ₀ : AffineDirection (IsLocalRing.ResidueField R))
    (hP : leftPoint D s₀ = directionPoint R S.t S.x e ψ₀) :
    ((leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R S.t S.x))).map e ≤
      Ideal.span {ψ₀.val ^ leftMultiplicity D s₀} := by
  have hmax : (Ideal.span ({S.t, S.x} : Set R)).IsMaximal := by
    rw [S.parameters]; exact IsLocalRing.maximalIdeal.isMaximal R
  set q := Ideal.Quotient.mk (chartExceptional R S.t S.x)
  let D' := restrictLeftData D (fun i ↦ Sum.inl i = s₀) (fun j ↦ Sum.inr j = s₀)
  have hsub : ∀ s s' : D'.ι ⊕ D'.ι0, s = s' := by
    rintro (⟨i, hi⟩ | ⟨j, hj⟩) (⟨i', hi'⟩ | ⟨j', hj'⟩) <;>
      first
      | (cases hi.trans hi'.symm; rfl) | cases hi.trans hj'.symm
      | cases hj.trans hi'.symm | (cases hj.trans hj'.symm; rfl)
  obtain ⟨s₁, hm₁⟩ : ∃ s₁ : D'.ι ⊕ D'.ι0, leftMultiplicity D' s₁ = leftMultiplicity D s₀ := by
    rcases s₀ with i | j
    exacts [⟨.inl ⟨i, rfl⟩, rfl⟩, ⟨.inr ⟨j, rfl⟩, rfl⟩]
  obtain ⟨ψ, hψ, -, hK'⟩ := left_kernel_polynomial_residueField O R S beta D' e he heZ
  rw [finprod_eq_single _ s₁ (fun s hs ↦ absurd (hsub s s₁) hs), hm₁] at hK'
  have hmono : ((leftKernel D 1).map q).map e ≤ ((leftKernel D' 1).map q).map e :=
    Ideal.map_mono (Ideal.map_mono (leftKernel_le_restrictLeftData D _ _))
  rcases Nat.eq_zero_or_pos (leftMultiplicity D s₀) with h0 | hpos
  · rw [h0, pow_zero, Ideal.span_singleton_one]; exact le_top
  obtain ⟨L, hL⟩ := (two_chart_left_data_transverse_finite R S.t S.x beta D 1).2 s₀
  have hPL : (leftPoint D s₀)^L ≤ leftKernel D' 1 := by
    unfold leftKernel finiteSupportKernel
    have h := pow_le_comap_completedPointMap _ _ _ L hL
    refine le_iInf fun s ↦ ?_
    rcases s with ⟨i, rfl⟩ | ⟨j, rfl⟩ <;> exact h
  have hmemP : ψ₀.val ∈ ((leftPoint D s₀).map q).map e := by
    rw [hP, (direction_point_maximal O R S e he heZ ψ₀).2.2.2.1]; exact Ideal.subset_span rfl
  have hsurj : Function.Surjective (fun a ↦ e (q a)) :=
    e.surjective.comp Ideal.Quotient.mk_surjective
  rw [← Ideal.map_coe e, Ideal.map_map] at hmemP
  obtain ⟨a, ha, hae⟩ := (Ideal.mem_map_iff_of_surjective _ hsurj).1 hmemP
  have h1 : Ideal.span {ψ₀.val ^ L} ≤ Ideal.span {ψ s₁ ^ leftMultiplicity D s₀} := by
    rw [← hK', Ideal.span_singleton_le_iff_mem, ← hae, ← map_pow]
    exact Ideal.mem_map_of_mem _ (Ideal.mem_map_of_mem _ (hPL (Ideal.pow_mem_pow ha L)))
  rw [Ideal.span_singleton_le_span_singleton] at h1
  have h4 : ψ s₁ = ψ₀.val := Polynomial.eq_of_monic_of_associated (hψ s₁).1 ψ₀.2.1
    ((hψ s₁).2.associated_of_dvd ψ₀.2.2
      ((hψ s₁).2.prime.dvd_of_dvd_pow ((dvd_pow_self _ hpos.ne').trans h1)))
  rw [← h4, ← hK']
  exact hmono

/-- If a curve datum matches `Dv`, the level-one left kernel maps to the ideal of `k[X]` generated
by the affine polynomial of `Dv`. -/
theorem matches_divisor_level_one_polynomial (O R : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]
    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x)
    (D : TwoChartCurveData R S.t S.x beta) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))
    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*
      Polynomial (IsLocalRing.ResidueField R))
    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =
      Polynomial.C (IsLocalRing.residue R r))
    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)
    (hm : MatchesDivisor e D Dv) [IsNoetherianRing (BlowupChart R S.t S.x)] :
    ((leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R S.t S.x))).map e =
      Ideal.span {divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv} := by
  classical
  have hmax : (Ideal.span ({S.t, S.x} : Set R)).IsMaximal := by
    rw [S.parameters]; exact IsLocalRing.maximalIdeal.isMaximal R
  set k := IsLocalRing.ResidueField R
  set q := Ideal.Quotient.mk (chartExceptional R S.t S.x)
  have hdp := direction_point_maximal O R S e he heZ
  have hQ {i : D.ι} {ψ : AffineDirection k} (hψ : ψ ≠ zeroAffine k)
      (h : D.Q i = (directionPoint R S.t S.x e ψ).map
        (algebraMap (BlowupChart R S.t S.x) (BlowupOverlap R S.t S.x))) :
      leftPoint D (Sum.inl i) = directionPoint R S.t S.x e ψ := by
    change (D.Q i).comap _ = _
    rw [h]; exact (direction_point_overlap_maximal O R S e he heZ ψ hψ).2.2
  choose φ hφne hφQ hφDv using hm.common
  -- the direction of each left point
  let dir : D.ι ⊕ D.ι0 → AffineDirection k := Sum.elim φ (fun _ ↦ zeroAffine k)
  have hdirP : ∀ s, leftPoint D s = directionPoint R S.t S.x e (dir s) := by
    rintro (i | j)
    exacts [hQ (hφne i) (hφQ i), (hm.zero j).1]
  have hdirM : ∀ s, Dv (some (dir s)) = leftMultiplicity D s := by
    rintro (i | j)
    exacts [(hφDv i).trans (two_chart_common_multiplicity_eq R S.t S.x beta D i).1.symm,
      (hm.zero j).2]
  have hdirDeg (s) : (dir s).val.natDegree = leftResidueDegree D s := by
    rw [leftResidueDegree, hdirP, (hdp (dir s)).2.2.2.2.1, ENat.toNat_natCast]
  have hdirInj : Function.Injective dir := fun s s' h ↦
    (two_chart_left_points_maximal R S.t S.x beta D).2.1 (by rw [hdirP, hdirP, h])
  have hmonic_eq {p p' : AffineDirection k} (h : p.val ∣ p'.val) : p.val = p'.val :=
    Polynomial.eq_of_monic_of_associated p.2.1 p'.2.1 (p.2.2.associated_of_dvd p'.2.2 h)
  have hC (s₀) : ((leftKernel D 1).map q).map e ≤
      Ideal.span {(dir s₀).val ^ leftMultiplicity D s₀} :=
    left_kernel_map_le_span_direction_pow O R S beta D e he heZ s₀ _ (hdirP s₀)
  have : Fintype (D.ι ⊕ D.ι0) := Fintype.ofFinite _
  obtain ⟨ψ, hψ, hψdeg, hK⟩ := left_kernel_polynomial_residueField O R S beta D e he heZ
  rw [finprod_eq_prod_of_fintype] at hK
  -- `∏ dir s ^ mult s ∣ ∏ ψ s ^ mult s`, and both are monic of the same degree
  have hdvd : (∏ s, (dir s).val ^ leftMultiplicity D s) ∣ ∏ s, ψ s ^ leftMultiplicity D s := by
    refine Finset.prod_dvd_of_coprime (fun s _ s' _ hne ↦ IsCoprime.pow ?_) fun s _ ↦
      Ideal.mem_span_singleton.1 (hC s (by rw [hK]; exact Ideal.subset_span rfl))
    rw [Irreducible.coprime_iff_not_dvd (dir s).2.2]
    exact fun hd ↦ hne (hdirInj (Subtype.ext (hmonic_eq hd)))
  have hGP := Polynomial.eq_of_monic_of_dvd_of_natDegree_le
    (Polynomial.monic_prod_of_monic _ _ fun s _ ↦ (dir s).2.1.pow _)
    (Polynomial.monic_prod_of_monic _ _ fun s _ ↦ (hψ s).1.pow _) hdvd <| by
      rw [Polynomial.natDegree_prod_of_monic _ _ fun s _ ↦ (hψ s).1.pow _,
        Polynomial.natDegree_prod_of_monic _ _ fun s _ ↦ (dir s).2.1.pow _]
      refine le_of_eq (Finset.sum_congr rfl fun s _ ↦ ?_)
      rw [Polynomial.natDegree_pow, Polynomial.natDegree_pow, hψdeg, hdirDeg]
  rw [hK, hGP]
  refine congrArg (fun p ↦ Ideal.span {p}) ?_
  unfold divisorAffinePolynomial
  -- finally, the support of `Dv` consists of `∞` and the directions of the left points
  have hsub : Dv.support ⊆ insert none (Finset.univ.image (fun s ↦ some (dir s))) := by
    rintro (_ | ψ0) hP
    · exact Finset.mem_insert_self _ _
    rw [Finsupp.mem_support_iff] at hP
    refine Finset.mem_insert_of_mem (Finset.mem_image.2 ?_)
    by_cases hz : ψ0 = zeroAffine k
    · subst hz
      obtain ⟨j⟩ := hm.zero_surj (Nat.pos_of_ne_zero hP)
      exact ⟨Sum.inr j, Finset.mem_univ _, rfl⟩
    · obtain ⟨i, hi⟩ := hm.common_surj ψ0 hz (Nat.pos_of_ne_zero hP)
      exact ⟨Sum.inl i, Finset.mem_univ _,
        congrArg some ((hdp ψ0).2.2.2.2.2 ((hdirP _).symm.trans (hQ hz hi)))⟩
  symm
  rw [Finsupp.prod_of_support_subset Dv hsub _ (by rintro (_ | ψ0) _ <;> simp),
    Finset.prod_insert (by simp),
    Finset.prod_image (fun a _ b _ h ↦ hdirInj (Option.some_injective _ h))]
  simp only [one_mul]
  exact Finset.prod_congr rfl fun s _ ↦ by rw [hdirM]

/-- The common computation behind `global_function_has_tangent_divisor`: the glued function is
`f = ∑ cᵢ tᵈ⁻ⁱ xⁱ` with residue form `P · a`, where `P` is the (monic) affine polynomial of `Dv`
and `a ≠ 0`. -/
private theorem glued_level_one_data (O R : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]
    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x)
    (D : TwoChartCurveData R S.t S.x beta) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))
    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*
      Polynomial (IsLocalRing.ResidueField R))
    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =
      Polynomial.C (IsLocalRing.residue R r))
    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)
    (hm : MatchesDivisor e D Dv) [IsNoetherianRing (BlowupChart R S.t S.x)]
    [IsNoetherianRing (BlowupChart R S.x S.t)] (hreg : RegularParameterPair R S.t S.x)
    (hregSwap : RegularParameterPair R S.x S.t) (f : R)
    (G : GluedGenerators R S.t S.x beta (curveDataDegree D))
    (hf : ∀ j : ℕ, surfaceToCechInput R S.t S.x j f =
      (cechInputLattice R S.t S.x j).mkQ (gluedFunctionPair R S.t S.x G j))
    (hG : ∀ j : ℕ,
      Ideal.span {Ideal.Quotient.mk ((chartExceptional R S.t S.x)^j) (G.left j)} =
        leftLevelKernel D j ∧
      Ideal.span {Ideal.Quotient.mk ((chartExceptional R S.x S.t)^j) (G.right j)} =
        rightLevelKernel D j) :
    ∃ (c : Fin (curveDataDegree D+1) → R) (a : IsLocalRing.ResidueField R),
      f = ∑ i : Fin (curveDataDegree D+1), c i * S.t^(curveDataDegree D - i.val) * S.x^i.val ∧
      a ≠ 0 ∧ (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv).Monic ∧
      (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv).natDegree + Dv none =
        curveDataDegree D ∧
      ∀ i : Fin (curveDataDegree D+1),
        (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv * Polynomial.C a).coeff i.val =
          IsLocalRing.residue R (c i) := by
  classical
  obtain ⟨c, hfc, hGc, -⟩ := glued_function_initial_form R S.t S.x beta _ G hreg hregSwap f hf
  set k := IsLocalRing.ResidueField R
  set H : Polynomial k := ∑ i : Fin (curveDataDegree D+1),
    Polynomial.C (IsLocalRing.residue R (c i)) * Polynomial.X ^ i.val with hHdef
  set P := divisorAffinePolynomial k Dv with hPdef
  -- `e` maps the class of `G.left 1` to `H`, which therefore generates the same ideal as `P`
  have hal (r : R) : algebraMap R (BlowupChart R S.t S.x) r = chartBase R S.t S.x r := rfl
  have heG : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (G.left 1)) = H := by
    rw [Ideal.Quotient.eq.mpr hGc, map_sum, map_sum]
    exact Finset.sum_congr rfl fun i _ ↦ by rw [map_mul, map_mul, map_pow, map_pow, hal, he, heZ]
  have hspan : Ideal.span {H} = Ideal.span {P} := by
    have hle : (chartExceptional R S.t S.x) ^ 1 ≤ chartExceptional R S.t S.x := by rw [pow_one]
    have h2 := congrArg (fun I ↦ (I.map (Ideal.Quotient.factor hle)).map e) (hG 1).1
    rw [Ideal.map_span, Set.image_singleton, Ideal.map_span, Set.image_singleton] at h2
    have hψ : Ideal.Quotient.factor hle (Ideal.Quotient.mk _ (G.left 1)) =
        Ideal.Quotient.mk (chartExceptional R S.t S.x) (G.left 1) := rfl
    rw [hψ, heG] at h2
    rw [h2, ← matches_divisor_level_one_polynomial O R S beta D Dv e he heZ hm]
    congr 1
    unfold leftLevelKernel finiteSupportLevelKernel
    exact Ideal.map_map _ _
  -- `P = ∏ g Q ^ Dv Q` is monic of degree `deg Dv - Dv ∞`
  set g : ClosedDirection k → ℕ → Polynomial k := fun Q r ↦ Option.elim Q 1 (fun phi ↦ phi.val ^ r)
  have hPprod : P = ∏ Q ∈ Dv.support, g Q (Dv Q) := by
    rw [hPdef, divisorAffinePolynomial, Finsupp.prod]
    exact Finset.prod_congr rfl fun Q _ ↦ by cases Q <;> rfl
  have hterm (Q : ClosedDirection k) (r : ℕ) : (g Q r).Monic ∧
      directionDegree k Q * r = (g Q r).natDegree + (if Q = none then r else 0) := by
    cases Q with
    | none => simp [g, directionDegree]
    | some phi =>
      exact ⟨phi.2.1.pow r, by simp [g, directionDegree, phi.2.1.natDegree_pow, mul_comm]⟩
  have hPmon : P.Monic := hPprod ▸ Polynomial.monic_prod_of_monic _ _ fun Q _ ↦ (hterm Q _).1
  have hPdeg : P.natDegree + Dv none = exceptionalDegree k Dv := by
    rw [hPprod, exceptionalDegree, Finsupp.sum,
      Polynomial.natDegree_prod_of_monic (h := fun Q _ ↦ (hterm Q (Dv Q)).1),
      Finset.sum_congr rfl fun Q _ ↦ (hterm Q (Dv Q)).2, Finset.sum_add_distrib, Finset.sum_ite_eq']
    split_ifs with h
    · rfl
    · rw [Finsupp.notMem_support_iff.mp h]
  -- hence `H = P * C a` with `a ≠ 0`
  obtain ⟨u, hu⟩ := Ideal.span_singleton_eq_span_singleton.mp hspan.symm
  obtain ⟨a, ha, hau⟩ := Polynomial.isUnit_iff.mp u.isUnit
  have hHP : H = P * Polynomial.C a := by rw [← hu, hau]
  refine ⟨c, a, hfc, ha.ne_zero, hPmon,
    hPdeg.trans (matches_divisor_degree O R S beta D Dv e he heZ hm), fun i ↦ ?_⟩
  rw [← hHP, hHdef, Polynomial.finsetSum_coeff, Finset.sum_eq_single i (fun b _ hb ↦ ?_) (by simp)]
  · simp
  · rw [Polynomial.coeff_C_mul_X_pow, if_neg fun h ↦ hb (Fin.ext h.symm)]

/-- A global function glued from the generators of a curve datum matching `Dv` has tangent
divisor `Dv` in degree `deg D`. -/
theorem global_function_has_tangent_divisor (O R : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]
    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x)
    (D : TwoChartCurveData R S.t S.x beta) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))
    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*
      Polynomial (IsLocalRing.ResidueField R))
    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =
      Polynomial.C (IsLocalRing.residue R r))
    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)
    (hm : MatchesDivisor e D Dv) [IsNoetherianRing (BlowupChart R S.t S.x)]
    [IsNoetherianRing (BlowupChart R S.x S.t)] (hreg : RegularParameterPair R S.t S.x)
    (hregSwap : RegularParameterPair R S.x S.t) (f : R)
    (G : GluedGenerators R S.t S.x beta (curveDataDegree D))
    (hf : ∀ j : ℕ, surfaceToCechInput R S.t S.x j f =
      (cechInputLattice R S.t S.x j).mkQ (gluedFunctionPair R S.t S.x G j))
    (hG : ∀ j : ℕ,
      Ideal.span {Ideal.Quotient.mk ((chartExceptional R S.t S.x)^j) (G.left j)} =
        leftLevelKernel D j ∧
      Ideal.span {Ideal.Quotient.mk ((chartExceptional R S.x S.t)^j) (G.right j)} =
        rightLevelKernel D j) :
    HasTangentDivisor O R S (Ideal.span {f}) (curveDataDegree D) Dv := by
  obtain ⟨c, a, hfc, ha0, hPmon, hPdeg, hcoeff⟩ :=
    glued_level_one_data O R S beta D Dv e he heZ hm hreg hregSwap f G hf hG
  set P := divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv
  have hnd : (P * Polynomial.C a).natDegree = P.natDegree := Polynomial.natDegree_mul_C ha0
  refine ⟨f, P * Polynomial.C a, rfl, ⟨?_, ?_, ?_, ?_⟩, ?_⟩
  · exact mul_ne_zero hPmon.ne_zero (Polynomial.C_ne_zero.2 ha0)
  · rw [hnd]; omega
  · rw [hnd]; omega
  · rw [Polynomial.leadingCoeff_mul, hPmon.leadingCoeff, Polynomial.leadingCoeff_C,
      one_mul, mul_comm]
  · rw [hfc]
    unfold tangentLift
    apply initial_form_lift_independent
    intro i
    rw [hcoeff i, ← IsLocalRing.residue_eq_zero_iff, map_sub, sub_eq_zero]
    unfold residueRepresentative
    exact (Function.invFun_eq (IsLocalRing.residue_surjective _)).symm

private theorem span_sup_eq_top_of_isUnit_coeff {R B C : Type} [CommRing R] [CommRing B]
    [CommRing C] [Algebra R B] (φ : B →+* C) (w : B)
    (d : ℕ) (c : Fin (d + 1) → R) (n : Fin (d + 1) → ℕ) (j : Fin (d + 1)) (hj : IsUnit (c j))
        (hnj : n j = 0)
    (hn : ∀ i, i ≠ j → n i ≠ 0) :
    Ideal.span {φ (∑ i : Fin (d+1), algebraMap R B (c i) * w^(n i))} ⊔ Ideal.span {φ w} = ⊤ := by
  set J := Ideal.span {φ (∑ i : Fin (d+1), algebraMap R B (c i) * w^(n i))} ⊔ Ideal.span {φ w}
  have hw : Ideal.Quotient.mk J (φ w) = 0 :=
    Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_sup_right (Ideal.subset_span rfl))
  have hF : Ideal.Quotient.mk J (φ (∑ i : Fin (d+1), algebraMap R B (c i) * w^(n i))) = 0 :=
    Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_sup_left (Ideal.subset_span rfl))
  have hF' : Ideal.Quotient.mk J (φ (∑ i : Fin (d+1), algebraMap R B (c i) * w^(n i))) =
      Ideal.Quotient.mk J (φ (algebraMap R B (c j))) := by
    simp only [map_sum, map_mul, map_pow, hw]
    rw [Finset.sum_eq_single j]
    · rw [hnj, pow_zero, mul_one]
    · intro i _ hi
      rw [zero_pow (hn i hi), mul_zero]
    · intro h; exact absurd (Finset.mem_univ j) h
  rw [hF] at hF'
  have hmem : φ (algebraMap R B (c j)) ∈ J := Ideal.Quotient.eq_zero_iff_mem.mp hF'.symm
  exact Ideal.eq_top_of_isUnit_mem _ hmem ((hj.map (algebraMap R B)).map φ)

/-- If the residues of `c₀, …, c_n` are the coefficients of `P · κ` (`κ ≠ 0`), where `P` is the
monic affine polynomial of `Dv` and `deg P + Dv ∞ = n`, then `c_n` is a unit when `Dv` avoids
`∞`, and `c₀` is a unit when `Dv` avoids the zero direction. -/
private theorem isUnit_coeffs_of_residue_eq {R : Type} [CommRing R] [IsLocalRing R]
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)) {n : ℕ} (c : Fin (n + 1) → R)
    (κ : IsLocalRing.ResidueField R) (hκ : κ ≠ 0)
    (hPmon : (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv).Monic)
    (hPdeg : (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv).natDegree + Dv none = n)
    (hcoeff : ∀ i : Fin (n + 1), (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv *
      Polynomial.C κ).coeff i.val = IsLocalRing.residue R (c i)) :
    (Dv none = 0 → IsUnit (c (Fin.last n))) ∧
      (Dv (zeroDirection (IsLocalRing.ResidueField R)) = 0 → IsUnit (c 0)) := by
  refine ⟨fun h0 ↦ ?_, fun h0 ↦ ?_⟩ <;>
    rw [← IsLocalRing.notMem_maximalIdeal, ← IsLocalRing.residue_eq_zero_iff, ← hcoeff,
      Polynomial.coeff_mul_C]
  · rw [Fin.val_last, ← hPdeg, h0, add_zero, ← Polynomial.leadingCoeff, hPmon.leadingCoeff,
      one_mul]
    exact hκ
  · refine mul_ne_zero (fun hP ↦ ?_) hκ
    rw [Fin.val_zero, ← Polynomial.X_dvd_iff] at hP
    exact (Nat.pos_iff_ne_zero.mp ((count_normalizedFactors_divisorAffinePolynomial _ Dv 1
      one_ne_zero (zeroAffine _)).2.mp hP)) h0

/-- A global function glued from a curve datum matching `Dv`, whose strict transforms are the
prescribed child ideals, generates an ideal of the fixed tangent cell. -/
theorem global_function_mem_cell (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)
    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)
    [IsDomain (ConcreteSurface O pi u a b)] [IsRegularLocalRing (ConcreteSurface O pi u a b)]
    (S : SurfaceData O (ConcreteSurface O pi u a b))
    (hS : S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b ∧ S.a = a ∧ S.b = b)
    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+*
      Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)
      (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))
    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
      (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ) (hd : 0 < d)
    (hs : (∃ c : ℕ, s = State.single a c ∧ b = 0) ∨ (∃ c h : ℕ, s = State.crossing a b c h ∧ 0 < b))
    (hdc : d ≤ stateContactT s) (hdh : ∀ h : ℕ, stateContactX s = some h → d ≤ h)
    (hDinf : 0 < Dv none ↔ d < stateContactT s)
    (hDzero : ∀ h : ℕ, stateContactX s = some h →
      (0 < Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) ↔ d < h))
    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
      (surfaceX O pi u a b))
    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)
      beta)
    (hm : MatchesDivisor e D Dv) (hdD : curveDataDegree D = d) (f : ConcreteSurface O pi u a b)
    (G : GluedGenerators (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)
      beta d)
    (hf : ∀ j : ℕ, surfaceToCechInput (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
      (surfaceX O pi u a b) j f = (cechInputLattice (ConcreteSurface O pi u a b)
        (surfaceT O pi u a b) (surfaceX O pi u a b) j).mkQ (gluedFunctionPair
          (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b) G j))
    (hG : ∀ j : ℕ,
      Ideal.span {Ideal.Quotient.mk (tExc O pi u a b^j) (G.left j)} = leftLevelKernel D j ∧
      Ideal.span {Ideal.Quotient.mk (xExc O pi u a b^j) (G.right j)} = rightLevelKernel D j)
    (I : ∀ Q : divisorSupport Dv, Ideal (divisorLocalRing (ConcreteSurface O pi u a b)
      (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf Q))
    (hI : ∀ Q : divisorSupport Dv, I Q ∈ childIdealSet (ConcreteSurface O pi u a b)
      (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf s d Q)
    (hIf : ∀ Q : divisorSupport Dv, divisorStrictTransform (ConcreteSurface O pi u a b)
      (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf d (Ideal.span {f}) Q = I Q) :
    Ideal.span {f} ∈ (fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv) := by
  classical
  have hreg := concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha
  have hregSwap := concrete_surface_regular_pair_xt O pi hpi.ne_zero u a b ha
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)
      (surfaceX O pi u a b)
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)
      (surfaceT O pi u a b)
  obtain ⟨ht, hx, hA, hB⟩ := hS
  rcases S with ⟨pi', hpi', t0, x0, un, a0, b0, ha0, hpar, hdim, hcomp, hinj, rE, rC, hvert⟩
  dsimp only at ht hx hA hB
  subst t0 x0 a0 b0 hdD
  set S' : SurfaceData O (ConcreteSurface O pi u a b) :=
    ⟨pi', hpi', _, _, un, a, b, ha0, hpar, hdim, hcomp, hinj, rE, rC, hvert⟩
  -- the coefficients of `f` at `x^d` and `t^d` are units when `Dv` avoids `∞`, resp. `0`
  obtain ⟨c, κ, hfc, hκ, hPmon, hPdeg, hcoeff⟩ :=
    glued_level_one_data O _ S' beta D Dv e he heZ hm hreg hregSwap f G hf hG
  obtain ⟨hcT, hcX⟩ := isUnit_coeffs_of_residue_eq Dv c κ hκ hPmon hPdeg hcoeff
  refine ⟨⟨⟨f, rfl⟩, ?_⟩, global_function_has_tangent_divisor O _ S' beta D Dv e he heZ hm hreg
    hregSwap f G hf hG⟩
  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set
      (ConcreteSurface O pi u a b))).IsMaximal := hpar ▸ IsLocalRing.maximalIdeal.isMaximal _
  obtain ⟨hdir, -, hdz⟩ := directionPoint_properties (ConcreteSurface O pi u a b) _ _ e he heZ
  obtain ⟨hP0max, hP0t, -, -⟩ := hdir (zeroAffine _)
  obtain ⟨hinfmax, hxinf, hWinf, -⟩ := infinity_point_maximal O _ S'
  have : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
      (surfaceX O pi u a b)).IsMaximal := hinfmax
  obtain ⟨hstA, hstB⟩ := concrete_strict_transform_generators O pi hpi u a b ha _ f c hfc _ hP0t
    (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) hxinf
      hWinf
  -- the contact orders of `f` with `t = 0` and `x = 0`
  have htc : Module.length (ConcreteSurface O pi u a b) (ConcreteSurface O pi u a b ⧸
      (Ideal.span {f} ⊔ Ideal.span {surfaceT O pi u a b})) = stateContactT s := by
    rw [concrete_infinity_boundary_contact O pi hpi u a b ha _ f c hfc
        (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))
      hxinf hWinf]
    by_cases hpos : 0 < Dv none
    · have h1 := (hI ⟨none, hpos⟩).2.2.1 rfl
      rw [← hIf ⟨none, hpos⟩] at h1
      rw [← hstB]
      exact (congrArg ((curveDataDegree D : ℕ∞) + ·) h1).trans
        (by rw [← Nat.cast_add, Nat.add_sub_cancel' hdc])
    · have hcd : stateContactT s = curveDataDegree D := by have := hDinf.not.mp hpos; omega
      rw [span_sup_eq_top_of_isUnit_coeff _ _ _ c (fun i ↦ curveDataDegree D - i.val) (Fin.last _)
        (hcT (by omega)) (by simp) (fun i hi ↦ by have := Fin.val_lt_last hi; omega),
        Module.length_eq_zero, add_zero, hcd]
  have hxc (h' : ℕ) (hsx : stateContactX s = some h') (hb : 0 < b) :
      Module.length (ConcreteSurface O pi u a b) (ConcreteSurface O pi u a b ⧸
          (Ideal.span {f} ⊔ Ideal.span {surfaceX O pi u a b})) = h' := by
    rw [concrete_zero_boundary_contact O pi hpi u a b ha hb _ f c hfc
      (directionPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b) e
          (zeroAffine _)) hdz]
    by_cases hpos : 0 < Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    · have h1 := (hI ⟨_, hpos⟩).2.2.2 rfl h' hsx
      rw [← hIf ⟨_, hpos⟩] at h1
      rw [← hstA]
      exact (congrArg ((curveDataDegree D : ℕ∞) + ·) h1).trans
        (by rw [← Nat.cast_add, Nat.add_sub_cancel' (hdh h' hsx)])
    · have h0 : Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) = 0 := by
        omega
      have hcd : h' = curveDataDegree D := by
        have := hdh h' hsx; have := (hDzero h' hsx).not.mp hpos; omega
      rw [span_sup_eq_top_of_isUnit_coeff _ _ _ c (fun i ↦ i.val) 0 (hcX h0) (by simp)
        (fun i hi h ↦ hi (Fin.ext h)), Module.length_eq_zero, add_zero, hcd]
  rcases hs with ⟨c', rfl, hb0⟩ | ⟨c', h', rfl, hb⟩
  · have hdc' : curveDataDegree D ≤ c' := hdc
    exact ⟨⟨ha, by omega⟩, rfl, hb0, htc⟩
  · have hdc' : curveDataDegree D ≤ c' := hdc
    have hdh' := hdh h' rfl
    exact ⟨⟨ha, hb, by omega, by omega⟩, rfl, rfl, htc, hxc h' rfl hb⟩

end SurfaceBlowup