Definitions/Def_ModularCurve_SpecializationMap.lean

import Definitions.Def_ModularCurve_JqCoeff
import Definitions.Def_ModularCurve_LaurentCoeff
import Definitions.Def_ModularCurve_PhiGen
import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure ↗
import Mathlib.RingTheory.IntegralClosure.GoingDown ↗
import Mathlib.RingTheory.Polynomial.IsIntegral ↗
import Mathlib.RingTheory.Valuation.LocalSubring ↗
import Mathlib.RingTheory.Algebraic.Basic ↗
import Definitions.Def_AlgebraicCurve_PlacesOverDVR
import Mathlib.FieldTheory.IsAlgClosed.Basic ↗
import Mathlib.Algebra.Polynomial.Lifts ↗
import Mathlib.RingTheory.Ideal.Quotient.Operations ↗
import Mathlib.RingTheory.Localization.AtPrime.Basic ↗
import Mathlib.RingTheory.Valuation.ValuationSubring ↗
import Mathlib.RingTheory.PrincipalIdealDomain ↗
import Mathlib.Algebra.CharP.Basic ↗
import Mathlib.Data.Int.CharZero ↗
import Mathlib.Data.Nat.Prime.Int ↗
import Mathlib.RingTheory.DedekindDomain.IntegralClosure ↗
import Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra ↗
import Mathlib.RingTheory.Ideal.Maps ↗
import Mathlib.RingTheory.Ideal.Maximal ↗
import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic ↗
import Definitions.Def_ModularCurve_FibreModel
import Definitions.Def_ModularCurve_ArithmeticGalois
import Definitions.Def_ModularCurve_PlaceSpecialization

set_option autoImplicit false

noncomputable section

namespace ModularCurve
namespace CharPModel

open AlgebraicCurve

variable (N : ℕ) [NeZero N]

variable (A : ValuationSubring (AlgebraicClosure ℚ))

end CharPModel
end ModularCurve

set_option autoImplicit false

noncomputable section

namespace ModularCurve
namespace CharPModel

section LaurentMap

variable {R S : Type*} [CommRing R] [CommRing S]

private def laurentMapRingHom (f : R →+* S) : LaurentSeries R →+* LaurentSeries S where
  toFun x := x.map f
  map_one' := by
    ext g
    rw [HahnSeries.map_coeff, HahnSeries.coeff_one, HahnSeries.coeff_one, apply_ite f,
      map_one, map_zero]
  map_mul' x y := HahnSeries.map_mul f.toNonUnitalRingHom
  map_zero' := by
    ext g
    rw [HahnSeries.map_coeff, HahnSeries.coeff_zero, HahnSeries.coeff_zero, map_zero]
  map_add' x y := HahnSeries.map_add f.toAddMonoidHom

@[simp]
private theorem laurentMapRingHom_apply (f : R →+* S) (x : LaurentSeries R) :
    laurentMapRingHom f x = x.map f := rfl

private theorem laurentMap_injective {f : R →+* S} (hf : Function.Injective f) {x y : LaurentSeries
    R}
    (h : x.map f = y.map f) : x = y := by
  ext g
  have hg := congrArg (fun z : LaurentSeries S => z.coeff g) h
  simpa only [HahnSeries.map_coeff] using hf hg

private theorem map_eval₂Bivar (Φ : Polynomial (Polynomial ℤ)) (f : R →+* S) (u v : LaurentSeries R)
    :
    (Φ.eval₂ (Polynomial.aeval (R := ℤ) u).toRingHom v).map f
      = Φ.eval₂ (Polynomial.aeval (R := ℤ) (u.map f)).toRingHom (v.map f) := by
  have hcomp : (laurentMapRingHom f).comp (Polynomial.aeval (R := ℤ) u).toRingHom
      = (Polynomial.aeval (R := ℤ) (u.map f)).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
        AlgHom.coe_toRingHom, Polynomial.aeval_X, laurentMapRingHom_apply]
  have h := Polynomial.hom_eval₂ Φ (Polynomial.aeval (R := ℤ) u).toRingHom
    (laurentMapRingHom f) v
  rw [← laurentMapRingHom_apply, h, hcomp, laurentMapRingHom_apply]

end LaurentMap

section FibreEval

variable {R S : Type*} [CommRing R] [CommRing S]

private theorem qExpand_map (N : ℕ) [NeZero N] (f : R →+* S) (x : LaurentSeries R) :
    (qExpand R N x).map f = qExpand S N (x.map f) := by
  ext k
  rw [HahnSeries.map_coeff]
  by_cases hk : (N : ℤ) ∣ k
  · obtain ⟨m, rfl⟩ := hk
    rw [qExpand_coeff_mul, qExpand_coeff_mul, HahnSeries.map_coeff]
  · have h1 := qExpand_coeff_of_not_dvd (R := R) (N := N) x hk
    have h2 := qExpand_coeff_of_not_dvd (R := S) (N := N) (x.map f) hk
    rw [h1, h2, map_zero]

private theorem map_jqNModC (N : ℕ) [NeZero N] {K K' : Type*} [CommRing K] [CommRing K']
    (f : K →+* K') : (jqNModC K N).map f = jqNModC K' N := by
  show (qExpand K N (jqModC K)).map f = qExpand K' N (jqModC K')
  rw [qExpand_map, map_jqModC]

variable (N : ℕ) [NeZero N] (data : ModularPolynomialData N)

private theorem intEval_eq_zero :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jqModC ℤ)).toRingHom (jqNModC ℤ N) = 0 := by
  refine laurentMap_injective (f := Int.castRingHom ℚ) (Int.castRingHom ℚ).injective_int ?_
  rw [map_eval₂Bivar, map_jqModC, map_jqNModC,
    show (0 : LaurentSeries ℤ).map (Int.castRingHom ℚ) = 0 from
      map_zero (laurentMapRingHom (Int.castRingHom ℚ))]
  exact data.eval_eq_zero

private theorem fibreEval_eq_zero (k : Type*) [CommRing k] :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jqModC k)).toRingHom (jqNModC k N) = 0 := by
  have h := congrArg (fun x : LaurentSeries ℤ => x.map (Int.castRingHom k))
    (intEval_eq_zero N data)
  simpa only [map_eval₂Bivar, map_jqModC, map_jqNModC,
    show (0 : LaurentSeries ℤ).map (Int.castRingHom k) = 0 from
      map_zero (laurentMapRingHom (Int.castRingHom k))] using h

private theorem intEvalSwap_eq_zero (hsym : EvalSymm data.Φ) :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jqNModC ℤ N)).toRingHom (jqModC ℤ) = 0 := by
  refine laurentMap_injective (f := Int.castRingHom ℚ) (Int.castRingHom ℚ).injective_int ?_
  rw [map_eval₂Bivar, map_jqModC, map_jqNModC,
    show (0 : LaurentSeries ℤ).map (Int.castRingHom ℚ) = 0 from
      map_zero (laurentMapRingHom (Int.castRingHom ℚ))]
  rw [show jqModC ℚ = jq from rfl, show jqNModC ℚ N = jqN N from rfl]
  rw [hsym (jqN N) jq]
  exact data.eval_eq_zero

private theorem fibreEvalSwap_eq_zero (hsym : EvalSymm data.Φ) (k : Type*) [CommRing k] :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jqNModC k N)).toRingHom (jqModC k) = 0 := by
  have h := congrArg (fun x : LaurentSeries ℤ => x.map (Int.castRingHom k))
    (intEvalSwap_eq_zero N data hsym)
  simpa only [map_eval₂Bivar, map_jqModC, map_jqNModC,
    show (0 : LaurentSeries ℤ).map (Int.castRingHom k) = 0 from
      map_zero (laurentMapRingHom (Int.castRingHom k))] using h

end FibreEval

end CharPModel
end ModularCurve

noncomputable section

namespace ModularCurve
namespace CharPModel

section LineTier

private theorem transcendental_subtype {K L : Type*} [Field K] [Field L] [Algebra K L]
    (S : IntermediateField K L) {x : L} (hx : x ∈ S) (h : Transcendental K x) :
    Transcendental K (⟨x, hx⟩ : S) := by
  intro halg
  apply h
  obtain ⟨p, hp0, hp⟩ := halg
  refine ⟨p, hp0, ?_⟩
  have h2 := congrArg S.val hp
  rw [map_zero, ← Polynomial.aeval_algHom_apply] at h2
  simpa using h2

private theorem tjq_pow (K : Type*) [CommRing K] (n : ℕ) :
    (jqModC K) ^ n = HahnSeries.single (-(n : ℤ)) 1 *
      HahnSeries.ofPowerSeries ℤ K ((jNum.map (Int.castRingHom K)) ^ n) := by
  have h : n • (-1 : ℤ) = -(n : ℤ) := by simp
  rw [jqModC, mul_pow, HahnSeries.single_pow, one_pow, h, ← map_pow]

private theorem tjq_constantCoeff_map (K : Type*) [CommRing K] :
    PowerSeries.constantCoeff (jNum.map (Int.castRingHom K)) = 1 := by
  rw [← PowerSeries.coeff_zero_eq_constantCoeff, PowerSeries.coeff_map,
    PowerSeries.coeff_zero_eq_constantCoeff, constantCoeff_jNum, map_one]

private theorem tjq_coeff_pow_self (K : Type*) [CommRing K] (n : ℕ) :
    ((jqModC K) ^ n).coeff (-(n : ℤ)) = 1 := by
  rw [tjq_pow, HahnSeries.coeff_single_mul, one_mul, sub_neg_eq_add, neg_add_cancel,
    show (0 : ℤ) = ((0 : ℕ) : ℤ) from rfl, HahnSeries.ofPowerSeries_apply_coeff,
    PowerSeries.coeff_zero_eq_constantCoeff, map_pow, tjq_constantCoeff_map, one_pow]

private theorem tjq_coeff_pow_of_lt (K : Type*) [CommRing K] {n : ℕ} {m : ℤ}
    (hm : m < -(n : ℤ)) : ((jqModC K) ^ n).coeff m = 0 := by
  rw [tjq_pow, HahnSeries.coeff_single_mul, one_mul]
  exact ofPowerSeries_coeff_of_neg _ (by omega)

private theorem tjq_algebraMap_eq_single (K : Type*) [CommRing K] (c : K) :
    algebraMap K (LaurentSeries K) c = HahnSeries.single 0 c := by
  have h1 : algebraMap K (PowerSeries K) c = PowerSeries.C c := by simp
  rw [HahnSeries.algebraMap_apply', h1, HahnSeries.ofPowerSeries_C]
  rfl

private theorem tjq_aeval_eq_zero (K : Type*) [CommRing K] {p : Polynomial K}
    (hp : Polynomial.aeval (jqModC K) p = 0) : p = 0 := by
  by_contra hp0
  set n := p.natDegree with hn
  have hcoeff : (Polynomial.aeval (jqModC K) p).coeff (-(n : ℤ)) = p.coeff n := by
    rw [Polynomial.aeval_def, Polynomial.eval₂_eq_sum_range, HahnSeries.coeff_sum,
      Finset.sum_eq_single n]
    · rw [tjq_algebraMap_eq_single, HahnSeries.coeff_single_zero_mul,
        tjq_coeff_pow_self, mul_one]
    · intro i hi hin
      have hilt : i < n := lt_of_le_of_ne (Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)) hin
      rw [tjq_algebraMap_eq_single, HahnSeries.coeff_single_zero_mul,
        tjq_coeff_pow_of_lt, mul_zero]
      omega
    · intro hn'
      exact absurd (Finset.self_mem_range_succ n) hn'
  rw [hp] at hcoeff
  simp only [HahnSeries.coeff_zero] at hcoeff
  exact hp0 (Polynomial.leadingCoeff_eq_zero.mp hcoeff.symm)

private theorem tjq_transcendental (K : Type*) [CommRing K] :
    Transcendental K (jqModC K) :=
  transcendental_iff.mpr fun _ hp => tjq_aeval_eq_zero K hp

private theorem coeffEmb_jq_eq_jqModC :
    coeffEmb (AlgebraicClosure ℚ) jq = jqModC (AlgebraicClosure ℚ) := by
  have hmap : jNumQ.map (algebraMap ℚ (AlgebraicClosure ℚ))
      = jNum.map (Int.castRingHom (AlgebraicClosure ℚ)) := by
    ext n
    simp [jNumQ, PowerSeries.coeff_map]
  rw [jq, jqModC, map_mul]
  congr 1
  · ext k
    rw [coeffEmb_coeff]
    by_cases hk : k = (-1 : ℤ) <;> simp [hk]
  · ext k
    rw [coeffEmb_coeff]
    by_cases hk : 0 ≤ k
    · lift k to ℕ using hk
      rw [HahnSeries.ofPowerSeries_apply_coeff, HahnSeries.ofPowerSeries_apply_coeff,
        ← hmap, PowerSeries.coeff_map]
    · rw [ofPowerSeries_coeff_of_neg _ (by omega), ofPowerSeries_coeff_of_neg _ (by omega),
        map_zero]

section ResidueFieldInline

variable {K₀ F₀ F₀' : Type*} [Field K₀] [Field F₀] [Field F₀'] [Algebra K₀ F₀] [Algebra K₀ F₀']
  [Algebra F₀ F₀'] [IsScalarTower K₀ F₀ F₀'] [FiniteDimensional F₀ F₀']

open IsLocalRing in
private theorem rf_linearIndependent_lift (w : AlgebraicCurve.Place K₀ F₀') {ι : Type*}
    [Fintype ι] (x : ι → w.toValuationSubring)
    (hx : LinearIndependent (w.restrict F₀).ResidueField
      fun i => (residue w.toValuationSubring (x i) : w.ResidueField)) :
    LinearIndependent F₀ fun i => ((x i : w.toValuationSubring) : F₀') := by
  classical
  rw [Fintype.linearIndependent_iff]
  intro g hg
  by_contra hne
  obtain ⟨i₀, hi₀⟩ : ∃ i, g i ≠ 0 := not_forall.mp hne
  set O : ValuationSubring F₀ := (w.restrict F₀).toValuationSubring
  have hne' : (Finset.univ.filter fun i => g i ≠ 0).Nonempty := ⟨i₀, by simpa using hi₀⟩
  obtain ⟨m, hm, hmmax⟩ := Finset.exists_max_image _ (fun i => O.valuation (g i)) hne'
  have hgm : g m ≠ 0 := by simpa using hm
  have hb : ∀ i, g i / g m ∈ O := by
    intro i
    by_cases hi : g i = 0
    · simp [hi]
    · apply O.mem_of_valuation_le_one
      rw [map_div₀]
      have hm0 : (0 : O.ValueGroup) < O.valuation (g m) := by
        rw [zero_lt_iff]; exact (map_ne_zero _).mpr hgm
      exact (div_le_one₀ hm0).mpr (hmmax i (by simpa using hi))
  let b : ι → O := fun i => ⟨g i / g m, hb i⟩
  have hrel : ∑ i, AlgebraicCurve.Place.restrictInclusion F₀ w (b i) * x i = 0 := by
    apply Subtype.ext
    have hcoe : ((∑ i, AlgebraicCurve.Place.restrictInclusion F₀ w (b i) * x i :
        w.toValuationSubring) : F₀') =
        ∑ i, algebraMap F₀ F₀' (g i / g m) * (x i : F₀') := by
      rw [AddSubmonoidClass.coe_finsetSum]
      refine Finset.sum_congr rfl fun i _ => ?_
      rw [MulMemClass.coe_mul, AlgebraicCurve.Place.coe_restrictInclusion]
    rw [hcoe]
    have : ∑ i, algebraMap F₀ F₀' (g i / g m) * (x i : F₀') =
        algebraMap F₀ F₀' (g m)⁻¹ * ∑ i, g i • ((x i : w.toValuationSubring) : F₀') := by
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl fun i _ => ?_
      rw [Algebra.smul_def, div_eq_inv_mul, map_mul, mul_assoc]
    rw [this, hg, mul_zero]
    rfl
  have hres : ∑ i, (residue O (b i) : (w.restrict F₀).ResidueField) •
      (residue w.toValuationSubring (x i) : w.ResidueField) = 0 := by
    have h := congrArg (residue w.toValuationSubring) hrel
    rw [map_sum, map_zero] at h
    rw [← h]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Algebra.smul_def, AlgebraicCurve.Place.algebraMap_residueField_eq,
      AlgebraicCurve.Place.restrictResidueMap_residue, map_mul]
  have hm1 := (Fintype.linearIndependent_iff.mp hx) _ hres m
  have hbm : b m = 1 := Subtype.ext (div_self hgm)
  rw [hbm, map_one] at hm1
  exact one_ne_zero hm1

open IsLocalRing in
private theorem rf_finite_residueField (w : AlgebraicCurve.Place K₀ F₀') :
    Module.Finite (w.restrict F₀).ResidueField w.ResidueField := by
  classical
  rw [← Module.rank_lt_aleph0_iff]
  refine lt_of_le_of_lt (rank_le (n := Module.finrank F₀ F₀') fun s hs => ?_)
    Cardinal.natCast_lt_aleph0
  choose x hx using fun y : s => residue_surjective (R := w.toValuationSubring)
    (y : w.ResidueField)
  have hs' : LinearIndependent (w.restrict F₀).ResidueField
      fun i : s => (residue w.toValuationSubring (x i) : w.ResidueField) := by
    simpa only [hx] using hs
  have := rf_linearIndependent_lift (F₀ := F₀) w x hs'
  simpa [Fintype.card_coe] using this.fintype_card_le_finrank

end ResidueFieldInline

private theorem transcendental_jBar (N : ℕ) [NeZero N] :
    Transcendental (AlgebraicClosure ℚ) (jBar N) := by
  have h := tjq_transcendental (AlgebraicClosure ℚ)
  rw [← coeffEmb_jq_eq_jqModC] at h
  exact transcendental_subtype _
    (coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionField_le_full N (jq_mem N))) h

private theorem transcendental_jC (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    Transcendental k (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) :=
  transcendental_subtype _ (jqModC_mem k N) (tjq_transcendental k)

private theorem fibreEval_subtype (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ)
        (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom
      (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) = 0 := by
  have hcomp : ((modularFunctionFieldC k N).val.toRingHom).comp
      (Polynomial.aeval (R := ℤ)
        (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom
      = (Polynomial.aeval (R := ℤ) (jqModC k)).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
        AlgHom.coe_toRingHom, Polynomial.aeval_X]
      rfl
  have h := Polynomial.hom_eval₂ data.Φ
    (Polynomial.aeval (R := ℤ)
      (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom
    ((modularFunctionFieldC k N).val.toRingHom)
    (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)
  apply Subtype.val_injective
  have h0 : (modularFunctionFieldC k N).val.toRingHom
      (data.Φ.eval₂ (Polynomial.aeval (R := ℤ)
          (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom
        (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)) = 0 := by
    rw [h, hcomp]
    exact fibreEval_eq_zero N data k
  simpa using h0

private theorem adjoin_pair_subtype_eq_top {K L : Type*} [Field K] [Field L] [Algebra K L]
    (x y : L) :
    IntermediateField.adjoin K
        ({⟨x, IntermediateField.subset_adjoin K {x, y} (Set.mem_insert x {y})⟩,
          ⟨y, IntermediateField.subset_adjoin K {x, y} (Set.mem_insert_of_mem x rfl)⟩} :
          Set (IntermediateField.adjoin K ({x, y} : Set L))) = ⊤ := by
  rw [eq_top_iff]
  rintro ⟨z, hz⟩ -
  induction hz using IntermediateField.adjoin_induction with
  | mem z hzm =>
    rcases hzm with rfl | hzm
    · exact IntermediateField.subset_adjoin _ _ (Set.mem_insert _ _)
    · rcases hzm with rfl
      exact IntermediateField.subset_adjoin _ _ (Set.mem_insert_of_mem _ rfl)
  | algebraMap a => exact IntermediateField.algebraMap_mem _ a
  | add a b ha hb hia hib => exact add_mem hia hib
  | mul a b ha hb hia hib => exact mul_mem hia hib
  | inv a ha hia => exact inv_mem hia

private theorem isIntegral_adjoin_of_bivar_monic {K L : Type*} [Field K] [Field L] [Algebra K L]
    {Φ : Polynomial (Polynomial ℤ)} (hΦ : Φ.Monic) {x y : L}
    (h : Φ.eval₂ (Polynomial.aeval (R := ℤ) x).toRingHom y = 0) :
    IsIntegral (IntermediateField.adjoin K ({x} : Set L)) y := by
  set g : Polynomial ℤ →+* IntermediateField.adjoin K ({x} : Set L) :=
    (Polynomial.aeval (R := ℤ)
      (⟨x, IntermediateField.mem_adjoin_simple_self K x⟩ :
        IntermediateField.adjoin K ({x} : Set L))).toRingHom with hg
  have hcomp : (algebraMap (IntermediateField.adjoin K ({x} : Set L)) L).comp g
      = (Polynomial.aeval (R := ℤ) x).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · simp only [hg, RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
        AlgHom.coe_toRingHom, Polynomial.aeval_X]
      rfl
  refine ⟨Φ.map g, hΦ.map g, ?_⟩
  rw [Polynomial.eval₂_map, hcomp]
  exact h

private theorem barEval_laurent (N : ℕ) [NeZero N] (data : ModularPolynomialData N) :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ)
        (coeffEmb (AlgebraicClosure ℚ) jq)).toRingHom
      (coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq)) = 0 := by
  have hcomp : ((coeffEmb (AlgebraicClosure ℚ)).comp
      (Polynomial.aeval (R := ℤ) jq).toRingHom)
      = (Polynomial.aeval (R := ℤ) (coeffEmb (AlgebraicClosure ℚ) jq)).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
        AlgHom.coe_toRingHom, Polynomial.aeval_X]
  have h := Polynomial.hom_eval₂ data.Φ (Polynomial.aeval (R := ℤ) jq).toRingHom
    (coeffEmb (AlgebraicClosure ℚ)) (qExpand ℚ N jq)
  have h0 := data.eval_eq_zero
  rw [show evalAtJ = (Polynomial.aeval (R := ℤ) jq).toRingHom from rfl,
    show jqN N = qExpand ℚ N jq from rfl] at h0
  rw [h0, map_zero, hcomp] at h
  exact h.symm

private theorem barEval_subtype (N : ℕ) [NeZero N] (data : ModularPolynomialData N) :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom (jNBar N) = 0 := by
  have hcomp : (((laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)).val.toRingHom).comp
      (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom)
      = (Polynomial.aeval (R := ℤ)
          (coeffEmb (AlgebraicClosure ℚ) jq)).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
        AlgHom.coe_toRingHom, Polynomial.aeval_X]
      rfl
  have h := Polynomial.hom_eval₂ data.Φ
    (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom
    ((laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom)
    (jNBar N)
  apply Subtype.val_injective
  have h0 : (laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)).val.toRingHom
      (data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom (jNBar N)) = 0 := by
    rw [h, hcomp]
    exact barEval_laurent N data
  simpa using h0

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 200000 in
private theorem finiteDimensional_adjoin_jC (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) :
    FiniteDimensional
      (IntermediateField.adjoin k
        ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
      (modularFunctionFieldC k N) := by
  have hint : IsIntegral
      (IntermediateField.adjoin k
        ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
      (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) :=
    isIntegral_adjoin_of_bivar_monic data.monic (fibreEval_subtype k N data)
  have htop := adjoin_pair_subtype_eq_top (K := k) (jqModC k) (jqNModC k N)
  have htower := IntermediateField.adjoin_adjoin_left k
    ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))
    {⟨jqNModC k N, jqNModC_mem k N⟩}
  rw [Set.singleton_union] at htower
  have hpair : IntermediateField.adjoin k
      ({⟨jqModC k, jqModC_mem k N⟩, ⟨jqNModC k N, jqNModC_mem k N⟩} :
        Set (modularFunctionFieldC k N)) = ⊤ := htop
  rw [hpair] at htower
  have hFD : FiniteDimensional
      (IntermediateField.adjoin k
        ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
      (IntermediateField.adjoin
        (IntermediateField.adjoin k
          ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
        ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N))) :=
    IntermediateField.adjoin.finiteDimensional hint
  have h2 : IntermediateField.adjoin
      (IntermediateField.adjoin k
        ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
      ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N)) = ⊤ :=
    IntermediateField.restrictScalars_injective k
      (htower.trans IntermediateField.restrictScalars_top.symm)
  rw [h2] at hFD
  exact (IntermediateField.topEquiv (F := IntermediateField.adjoin k
    ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k
        N)))).toLinearEquiv.finiteDimensional

private theorem algebraMap_comp_aeval_adjoin_self {K L : Type*} [Field K] [Field L] [Algebra K L]
    (x : L) :
    (algebraMap (IntermediateField.adjoin K ({x} : Set L)) L).comp
      (Polynomial.aeval (R := ℤ)
        (IntermediateField.AdjoinSimple.gen K x)).toRingHom
      = (Polynomial.aeval (R := ℤ) x).toRingHom := by
  apply Polynomial.ringHom_ext
  · intro a
    simp only [eq_intCast, map_intCast]
  · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
      AlgHom.coe_toRingHom, Polynomial.aeval_X]
    rfl

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private def jLine (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    modularFunctionFieldC k N := ⟨jqModC k, jqModC_mem k N⟩

set_option synthInstance.maxHeartbeats 400000 in
private def jNLine (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    modularFunctionFieldC k N := ⟨jqNModC k N, jqNModC_mem k N⟩

private theorem transcendental_jLine (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    Transcendental k (jLine k N) := transcendental_jC k N

set_option synthInstance.maxHeartbeats 400000 in
private noncomputable def lineEquivC (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    RatFunc k ≃ₐ[k]
      (IntermediateField.adjoin k
        ({jLine k N} : Set (modularFunctionFieldC k N))) :=
  RatFunc.algEquivOfTranscendental _ (transcendental_jLine k N)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem lineEquivC_algebraMap (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (g : Polynomial k) :
    lineEquivC k N (algebraMap (Polynomial k) (RatFunc k) g)
      = Polynomial.aeval
          (IntermediateField.AdjoinSimple.gen k (jLine k N)) g :=
  RatFunc.algEquivOfTranscendental_algebraMap _ (transcendental_jLine k N) g

set_option maxSynthPendingDepth 3 in
set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem lineX (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    lineEquivC k N (algebraMap (Polynomial k) (RatFunc k) Polynomial.X)
      = IntermediateField.AdjoinSimple.gen k (jLine k N) := by
  rw [lineEquivC_algebraMap, Polynomial.aeval_X]

set_option maxSynthPendingDepth 3 in
set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem lineConst (k : Type*) [Field k] (N : ℕ) [NeZero N] (a : ℤ) :
    Polynomial.aeval (R := ℤ)
      (IntermediateField.AdjoinSimple.gen k (jLine k N)) (Polynomial.C a)
      = lineEquivC k N (algebraMap (Polynomial k) (RatFunc k)
          ((Polynomial.C a).map (Int.castRingHom k))) := by
  rw [Polynomial.aeval_C, Polynomial.map_C,
    show Polynomial.C ((Int.castRingHom k) a)
        = algebraMap k (Polynomial k) ((Int.castRingHom k) a) from rfl,
    ← IsScalarTower.algebraMap_apply k (Polynomial k) (RatFunc k),
    AlgEquiv.commutes]
  simp only [eq_intCast, map_intCast]

set_option maxSynthPendingDepth 3 in
set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem lineFun (k : Type*) [Field k] (N : ℕ) [NeZero N] (p : Polynomial ℤ) :
    Polynomial.aeval (R := ℤ)
      (IntermediateField.AdjoinSimple.gen k (jLine k N)) p
      = lineEquivC k N (algebraMap (Polynomial k) (RatFunc k)
          (p.map (Int.castRingHom k))) := by
  induction p using Polynomial.induction_on with
  | C a => exact lineConst k N a
  | add p q hp hq =>
    rw [Polynomial.map_add, map_add, map_add, map_add, hp, hq]
  | monomial n a _ =>
    simp only [Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_X, map_mul,
      map_pow, lineX, Polynomial.aeval_X]
    rw [lineConst k N a]

set_option maxSynthPendingDepth 3 in
set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem lineMapEq (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) :
    data.Φ.map
      ((Polynomial.aeval (R := ℤ)
        (IntermediateField.AdjoinSimple.gen k (jLine k N))).toRingHom)
      = ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map
          (algebraMap (Polynomial k) (RatFunc k))).map
        (lineEquivC k N).toAlgHom.toRingHom := by
  apply Polynomial.ext
  intro n
  rw [Polynomial.coeff_map, Polynomial.coeff_map, Polynomial.coeff_map,
    Polynomial.coeff_map]
  exact lineFun k N (data.Φ.coeff n)

set_option maxSynthPendingDepth 3 in
set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem linePsep (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N)
    (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable) :
    (data.Φ.map
      ((Polynomial.aeval (R := ℤ)
        (IntermediateField.AdjoinSimple.gen k (jLine k N))).toRingHom)).Separable := by
  rw [lineMapEq k N data]
  exact hsep.map

set_option maxSynthPendingDepth 3 in
set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem lineAevalZero (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) :
    Polynomial.aeval
      (R := IntermediateField.adjoin k
        ({jLine k N} : Set (modularFunctionFieldC k N)))
      (jNLine k N)
      (data.Φ.map
        ((Polynomial.aeval (R := ℤ)
          (IntermediateField.AdjoinSimple.gen k (jLine k N))).toRingHom)) = 0 := by
  rw [Polynomial.aeval_def, Polynomial.eval₂_map,
    algebraMap_comp_aeval_adjoin_self (jLine k N)]
  exact fibreEval_subtype k N data

set_option maxSynthPendingDepth 3 in
set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem lineDvd (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) :
    minpoly
      (IntermediateField.adjoin k
        ({jLine k N} : Set (modularFunctionFieldC k N)))
      (jNLine k N)
      ∣ data.Φ.map
        ((Polynomial.aeval (R := ℤ)
          (IntermediateField.AdjoinSimple.gen k (jLine k N))).toRingHom) :=
  minpoly.dvd
    (IntermediateField.adjoin k
      ({jLine k N} : Set (modularFunctionFieldC k N)))
    (jNLine k N)
    (lineAevalZero k N data)

set_option maxSynthPendingDepth 3 in
set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem isSeparable_jNC (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N)
    (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable) :
    IsSeparable
      (IntermediateField.adjoin k
        ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
      (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) :=
  (linePsep k N data hsep).of_dvd (lineDvd k N data)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem isSeparable_line_fibre (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N)
    (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable) :
    Algebra.IsSeparable
      (IntermediateField.adjoin k
        ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
      (modularFunctionFieldC k N) := by
  have hadj : Algebra.IsSeparable
      (IntermediateField.adjoin k
        ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
      (IntermediateField.adjoin
        (IntermediateField.adjoin k
          ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
        ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N))) :=
    (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable _ _).mpr
      (isSeparable_jNC k N data hsep)
  have htower := IntermediateField.adjoin_adjoin_left k
    ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))
    {⟨jqNModC k N, jqNModC_mem k N⟩}
  rw [Set.singleton_union] at htower
  have hpair : IntermediateField.adjoin k
      ({⟨jqModC k, jqModC_mem k N⟩, ⟨jqNModC k N, jqNModC_mem k N⟩} :
        Set (modularFunctionFieldC k N)) = ⊤ :=
    adjoin_pair_subtype_eq_top (K := k) (jqModC k) (jqNModC k N)
  rw [hpair] at htower
  have h2 : IntermediateField.adjoin
      (IntermediateField.adjoin k
        ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
      ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N)) = ⊤ :=
    IntermediateField.restrictScalars_injective k
      (htower.trans IntermediateField.restrictScalars_top.symm)
  rw [h2] at hadj
  haveI := hadj
  exact AlgEquiv.Algebra.isSeparable IntermediateField.topEquiv

end LineTier

section BarFinDim

private def jdBar (N : ℕ) [NeZero N] (d : ℕ) [NeZero d] (hd : d ∣ N) :
    laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N) :=
  ⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ d jq),
    coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jqd_mem_full N hd)⟩

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem barEvalD_subtype (N : ℕ) [NeZero N] (d : ℕ) [NeZero d] (hd : d ∣ N)
    (data : ModularPolynomialData d) :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom (jdBar N d hd) = 0 := by
  have hcomp : (((laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)).val.toRingHom).comp
      (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom)
      = (Polynomial.aeval (R := ℤ)
          (coeffEmb (AlgebraicClosure ℚ) jq)).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
        AlgHom.coe_toRingHom, Polynomial.aeval_X]
      rfl
  have h := Polynomial.hom_eval₂ data.Φ
    (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom
    ((laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom)
    (jdBar N d hd)
  apply Subtype.val_injective
  have h0 : (laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)).val.toRingHom
      (data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom (jdBar N d hd)) = 0 := by
    rw [h, hcomp]
    exact barEval_laurent d data
  simpa using h0

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem lbc_eq_adjoin_divisors (N : ℕ) [NeZero N] :
    laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)
      = IntermediateField.adjoin (AlgebraicClosure ℚ)
          (⇑(coeffEmb (AlgebraicClosure ℚ)) '' divisorExpansions N) := by
  refine le_antisymm (IntermediateField.adjoin_le_iff.mpr ?_)
    (IntermediateField.adjoin_le_iff.mpr ?_)
  · rintro x ⟨y, hy, rfl⟩
    have hy' : y ∈ IntermediateField.adjoin ℚ (divisorExpansions N) := hy
    induction hy' using IntermediateField.adjoin_induction with
    | mem z hz =>
      exact IntermediateField.subset_adjoin _ _ ⟨z, hz, rfl⟩
    | algebraMap a =>
      rw [eq_ratCast, map_ratCast]
      simp
    | add a b ha hb hia hib =>
      rw [map_add]; exact add_mem (hia ha) (hib hb)
    | mul a b ha hb hia hib =>
      rw [map_mul]; exact mul_mem (hia ha) (hib hb)
    | inv a ha hia =>
      rw [map_inv₀]; exact inv_mem (hia ha)
  · rintro x ⟨y, hy, rfl⟩
    exact coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
      (IntermediateField.subset_adjoin ℚ _ hy)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem adjoin_val_preimage_eq_top {K L : Type*} [Field K] [Field L] [Algebra K L]
    {F : IntermediateField K L} {S : Set L} (hF : F = IntermediateField.adjoin K S) :
    IntermediateField.adjoin K (Subtype.val ⁻¹' S : Set F) = ⊤ := by
  subst hF
  rw [eq_top_iff]
  rintro ⟨z, hz⟩ -
  induction hz using IntermediateField.adjoin_induction with
  | mem w hw => exact IntermediateField.subset_adjoin _ _ hw
  | algebraMap a => exact IntermediateField.algebraMap_mem _ a
  | add a b ha hb hia hib => exact add_mem hia hib
  | mul a b ha hb hia hib => exact mul_mem hia hib
  | inv a ha hia => exact inv_mem hia

private def barGenSet (N : ℕ) [NeZero N] :
    Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) :=
  Subtype.val ⁻¹' (⇑(coeffEmb (AlgebraicClosure ℚ)) '' divisorExpansions N)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem adjoin_barGenSet_eq_top (N : ℕ) [NeZero N] :
    IntermediateField.adjoin (AlgebraicClosure ℚ) (barGenSet N) = ⊤ :=
  adjoin_val_preimage_eq_top (lbc_eq_adjoin_divisors N)

private theorem barGenSet_finite (N : ℕ) [NeZero N] : (barGenSet N).Finite := by
  apply Set.Finite.preimage Subtype.val_injective.injOn
  apply Set.Finite.image
  have hsub : divisorExpansions N ⊆
      (fun d : {d // d ∈ N.divisors} =>
        @qExpand ℚ _ d.1 ⟨(Nat.pos_of_mem_divisors d.2).ne'⟩ jq) '' Set.univ := by
    rintro x ⟨d, hne, hd, hx⟩
    haveI := hne
    exact ⟨⟨d, Nat.mem_divisors.mpr ⟨hd, NeZero.ne N⟩⟩, Set.mem_univ _, hx.symm⟩
  exact ((Set.finite_univ (α := {d // d ∈ N.divisors})).image _).subset hsub

private theorem jBar_mem_barGenSet (N : ℕ) [NeZero N] : jBar N ∈ barGenSet N :=
  ⟨qExpand ℚ 1 jq, mem_divisorExpansions N (one_dvd N), by rw [qExpand_one_apply]; rfl⟩

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem barGenSet_integral (N : ℕ) [NeZero N]
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) :
    ∀ x ∈ barGenSet N,
      IsIntegral (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)))) x := by
  rintro ⟨xv, hxF⟩ hx
  obtain ⟨y, hy, hxy⟩ := hx
  obtain ⟨d, hdne, hd, rfl⟩ := hy
  haveI := hdne
  have hxel : (⟨xv, hxF⟩ : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) = jdBar N d hd := Subtype.ext hxy.symm
  rw [hxel]
  exact isIntegral_adjoin_of_bivar_monic (dataAll d hd).monic
    (barEvalD_subtype N d hd (dataAll d hd))

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem finiteDimensional_lineBar_of_dataAll (N : ℕ) [NeZero N]
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) :
    FiniteDimensional
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := by
  haveI : Finite ↥(barGenSet N) := (barGenSet_finite N).to_subtype
  have hint := barGenSet_integral N dataAll
  have htower := IntermediateField.adjoin_adjoin_left (AlgebraicClosure ℚ)
    ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N))) (barGenSet N)
  rw [Set.singleton_union, Set.insert_eq_self.mpr (jBar_mem_barGenSet N),
    adjoin_barGenSet_eq_top N] at htower
  have h2 : IntermediateField.adjoin
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))
      (barGenSet N) = ⊤ :=
    IntermediateField.restrictScalars_injective (AlgebraicClosure ℚ)
      (htower.trans IntermediateField.restrictScalars_top.symm)
  have hFD : FiniteDimensional
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))
      (IntermediateField.adjoin
        (IntermediateField.adjoin (AlgebraicClosure ℚ)
          ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
            (modularFunctionFieldFull N))))
        (barGenSet N)) :=
    IntermediateField.finiteDimensional_adjoin hint
  rw [h2] at hFD
  exact (IntermediateField.topEquiv (F := IntermediateField.adjoin (AlgebraicClosure ℚ)
    ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N))))).toLinearEquiv.finiteDimensional

end BarFinDim

end CharPModel
end ModularCurve

set_option autoImplicit false

open Polynomial

namespace ValuationSubring

variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)

private theorem closureConstantsAdjoin_eq_range_aeval (x : F) :
    Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x}) =
      (aeval (R := A) x).toRingHom.range := by
  apply le_antisymm
  · rw [Subring.closure_le]
    rintro y (⟨a, rfl⟩ | rfl)
    · refine ⟨C a, ?_⟩
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, aeval_C, RingHom.coe_comp,
        Function.comp_apply]
      rfl
    · exact ⟨X, by simp⟩
  · rintro y ⟨p, rfl⟩
    simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]
    induction p using Polynomial.induction_on with
    | C a =>
      rw [aeval_C]
      exact Subring.subset_closure (Or.inl ⟨a, rfl⟩)
    | add p q hp hq =>
      rw [map_add]
      exact Subring.add_mem _ hp hq
    | monomial n a h =>
      rw [pow_succ, ← mul_assoc, map_mul, aeval_X]
      exact Subring.mul_mem _ h (Subring.subset_closure (Or.inr rfl))

private theorem aeval_injective_of_transcendental {x : F} (hx : Transcendental K x) :
    Function.Injective (aeval (R := A) x) := by
  rw [injective_iff_map_eq_zero]
  intro p hp
  have hK : aeval x (p.map (algebraMap A K)) = 0 := by rwa [aeval_map_algebraMap]
  have hp' : p.map (algebraMap A K) = 0 :=
    (injective_iff_map_eq_zero _).mp (transcendental_iff_injective.mp hx) _ hK
  exact (Polynomial.map_injective (algebraMap A K) Subtype.val_injective)
    (by rw [hp', Polynomial.map_zero])

private theorem aeval_mem_closure (x : F) (p : A[X]) :
    aeval x p ∈ Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x}) := by
  rw [closureConstantsAdjoin_eq_range_aeval]
  exact ⟨p, rfl⟩

private noncomputable def polynomialEquivClosure {x : F} (hx : Transcendental K x) :
    A[X] ≃+* Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x}) :=
  RingEquiv.ofBijective
    ((aeval (R := A) x).toRingHom.codRestrict _ (A.aeval_mem_closure x))
    ⟨fun p q h => A.aeval_injective_of_transcendental hx (Subtype.ext_iff.mp h),
      fun y => by
        obtain ⟨p, hp⟩ : (y : F) ∈ (aeval (R := A) x).toRingHom.range := by
          rw [← closureConstantsAdjoin_eq_range_aeval]
          exact y.2
        exact ⟨p, Subtype.ext hp⟩⟩

@[simp]
private theorem polynomialEquivClosure_apply {x : F} (hx : Transcendental K x) (p : A[X]) :
    (A.polynomialEquivClosure hx p : F) = aeval x p := rfl

private theorem isIntegrallyClosed_closure {x : F} (hx : Transcendental K x) :
    IsIntegrallyClosed (Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x})) :=
  IsIntegrallyClosed.of_equiv (A.polynomialEquivClosure hx)

end ValuationSubring

namespace Subring

variable {F : Type*} [Field F]

private theorem isIntegral_iff_exists_monic_eval₂ (S : Subring F) (b : F) :
    IsIntegral S b ↔ ∃ p : Polynomial S, p.Monic ∧ Polynomial.eval₂ S.subtype b p = 0 :=
  Iff.rfl

private theorem exists_ideal_le_comap_eq_of_isIntegral {S B : Subring F} (hSB : S ≤ B)
    [IsIntegrallyClosed S] (hint : ∀ b : B, IsIntegral S (b : F))
    {p q : Ideal S} [p.IsPrime] [q.IsPrime] (hpq : p ≤ q)
    (Q : Ideal B) [Q.IsPrime] (hQ : Q.comap (Subring.inclusion hSB) = q) :
    ∃ P : Ideal B, P ≤ Q ∧ P.IsPrime ∧ P.comap (Subring.inclusion hSB) = p := by
  letI : Algebra S B := (Subring.inclusion hSB).toAlgebra
  have halg : ∀ s : S, algebraMap S B s = Subring.inclusion hSB s := fun _ => rfl
  haveI : FaithfulSMul S B := (faithfulSMul_iff_algebraMap_injective S B).mpr fun a b h => by
    rw [halg, halg] at h
    have h' : (a : F) = (b : F) := congrArg (fun y : B => (y : F)) h
    exact Subtype.ext h'
  haveI : Algebra.IsIntegral S B := ⟨fun b => by
    obtain ⟨f, hf, hfb⟩ := hint b
    refine ⟨f, hf, ?_⟩
    apply Subtype.val_injective
    change B.subtype (Polynomial.eval₂ (algebraMap S B) b f) = ((0 : B) : F)
    have hc : B.subtype.comp (algebraMap S B) = S.subtype := RingHom.ext fun _ => rfl
    rw [Polynomial.hom_eval₂, hc]
    exact hfb⟩
  haveI : Q.LiesOver q := ⟨by rw [Ideal.under_def, ← hQ]; rfl⟩
  obtain ⟨P, hPQ, hP, hPp⟩ := Ideal.exists_ideal_le_liesOver_of_le (p := p) (q := q) Q hpq
  exact ⟨P, hPQ, hP, by rw [hPp.over, Ideal.under_def]; rfl⟩

end Subring

set_option autoImplicit false

noncomputable section

open IsLocalRing

namespace AlgebraicCurve

namespace Place

variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)

private theorem algebraMap_mem (a : K) : algebraMap K F a ∈ w.toValuationSubring :=
    w.algebraMap_mem' a

private theorem algebraMap_mem_nonunits_iff (a : K) :
    algebraMap K F a ∈ w.toValuationSubring.nonunits ↔ a = 0 := by
  constructor
  · intro h
    rcases (ValuationSubring.mem_nonunits_iff_or _).mp h with h0 | hinv
    · exact (map_eq_zero _).mp h0
    · exact absurd (by simpa using w.algebraMap_mem a⁻¹) hinv
  · rintro rfl
    simp [ZeroMemClass.zero_mem]

private theorem mul_mem_nonunits {x y : F} (hx : x ∈ w.toValuationSubring.nonunits)
    (hy : y ∈ w.toValuationSubring) : x * y ∈ w.toValuationSubring.nonunits := by
  rw [ValuationSubring.mem_nonunits_iff] at hx ⊢
  rw [← ValuationSubring.valuation_le_one_iff] at hy
  calc w.toValuationSubring.valuation (x * y)
      = w.toValuationSubring.valuation x * w.toValuationSubring.valuation y := map_mul _ _ _
    _ ≤ w.toValuationSubring.valuation x * 1 := by gcongr
    _ = w.toValuationSubring.valuation x := mul_one _
    _ < 1 := hx

private theorem mem_of_ord_pos {f : F} (h : 0 < w.ord f) : f ∈ w.toValuationSubring := by
  have hf : f ≠ 0 := by rintro rfl; simp at h
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible w.toValuationSubring
  obtain ⟨u, hu⟩ := w.exists_unit_mul_zpow hf hπ
  rw [hu, show w.ord f = (((w.ord f).toNat : ℕ) : ℤ) from (Int.toNat_of_nonneg h.le).symm,
    zpow_natCast]
  exact mul_mem (u : w.toValuationSubring).2 (pow_mem (π : w.toValuationSubring).2 _)

private theorem mem_nonunits_iff_ord_pos {f : F} (hf : f ≠ 0) :
    f ∈ w.toValuationSubring.nonunits ↔ 0 < w.ord f := by
  constructor
  · intro h
    have hmem : f ∈ w.toValuationSubring := w.toValuationSubring.nonunits_subset h
    have h' : ((⟨f, hmem⟩ : w.toValuationSubring) : F) ∈ w.toValuationSubring.nonunits := h
    rw [ValuationSubring.coe_mem_nonunits_iff] at h'
    exact (w.mem_maximalIdeal_iff_ord_pos hf hmem).mp h'
  · intro h
    have hmem : f ∈ w.toValuationSubring := w.mem_of_ord_pos h
    have h' := (w.mem_maximalIdeal_iff_ord_pos hf hmem).mpr h
    rw [← ValuationSubring.coe_mem_nonunits_iff] at h'
    exact h'

private def HasValueAt (f : F) (a : K) : Prop :=
  f - algebraMap K F a ∈ w.toValuationSubring.nonunits

private theorem hasValueAt_iff (f : F) (a : K) :
    w.HasValueAt f a ↔ f - algebraMap K F a ∈ w.toValuationSubring.nonunits := Iff.rfl

private theorem hasValueAt_iff_ord_pos {f : F} {a : K} (h : f ≠ algebraMap K F a) :
    w.HasValueAt f a ↔ 0 < w.ord (f - algebraMap K F a) :=
  w.mem_nonunits_iff_ord_pos (sub_ne_zero.mpr h)

private theorem hasValueAt_of_ord_pos {f : F} {a : K} (h : 0 < w.ord (f - algebraMap K F a)) :
    w.HasValueAt f a := by
  have hne : f ≠ algebraMap K F a := by
    intro hfa; rw [hfa, sub_self] at h; simp at h
  exact (w.hasValueAt_iff_ord_pos hne).mpr h

private theorem hasValueAt_algebraMap (a : K) : w.HasValueAt (algebraMap K F a) a := by
  simp [HasValueAt, ZeroMemClass.zero_mem]

private theorem hasValueAt_zero_iff (f : F) : w.HasValueAt f 0 ↔ f ∈ w.toValuationSubring.nonunits
    := by
  simp [HasValueAt]

private theorem mem_of_hasValueAt {f : F} {a : K} (h : w.HasValueAt f a) : f ∈ w.toValuationSubring
    := by
  have h1 : f - algebraMap K F a ∈ w.toValuationSubring := w.toValuationSubring.nonunits_subset h
  simpa using add_mem h1 (w.algebraMap_mem a)

variable {w} in
private theorem HasValueAt.unique {f : F} {a b : K} (ha : w.HasValueAt f a) (hb : w.HasValueAt f b)
    :
    a = b := by
  have h : algebraMap K F (a - b) ∈ w.toValuationSubring.nonunits := by
    have := sub_mem hb ha
    rwa [sub_sub_sub_cancel_left, ← map_sub] at this
  exact sub_eq_zero.mp ((w.algebraMap_mem_nonunits_iff _).mp h)

variable {w} in
private theorem HasValueAt.add {f g : F} {a b : K} (hf : w.HasValueAt f a) (hg : w.HasValueAt g b) :
    w.HasValueAt (f + g) (a + b) := by
  have := add_mem hf hg
  rw [HasValueAt, map_add]
  convert this using 1
  ring

variable {w} in
private theorem HasValueAt.neg {f : F} {a : K} (hf : w.HasValueAt f a) : w.HasValueAt (-f) (-a) :=
    by
  have := neg_mem hf
  rw [HasValueAt, map_neg]
  convert this using 1
  ring

variable {w} in
private theorem HasValueAt.mul {f g : F} {a b : K} (hf : w.HasValueAt f a) (hg : w.HasValueAt g b) :
    w.HasValueAt (f * g) (a * b) := by
  have h1 : (f - algebraMap K F a) * g ∈ w.toValuationSubring.nonunits :=
    w.mul_mem_nonunits hf (w.mem_of_hasValueAt hg)
  have h2 : (g - algebraMap K F b) * algebraMap K F a ∈ w.toValuationSubring.nonunits :=
    w.mul_mem_nonunits hg (w.algebraMap_mem a)
  have := add_mem h1 h2
  rw [HasValueAt, map_mul]
  convert this using 1
  ring

variable {w} in
private theorem HasValueAt.inv {f : F} {a : K} (hf : w.HasValueAt f a) (ha : a ≠ 0) :
    w.HasValueAt f⁻¹ a⁻¹ := by
  have hf0 : f ≠ 0 := by
    rintro rfl
    have : w.HasValueAt (0 : F) 0 := by simpa using w.hasValueAt_algebraMap 0
    exact ha (hf.unique this)
  have hfu : f ∉ w.toValuationSubring.nonunits := fun hfn =>
    ha (hf.unique ((w.hasValueAt_zero_iff f).mpr hfn))
  have hfinv : f⁻¹ ∈ w.toValuationSubring := by
    by_contra hne
    exact hfu ((ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inr (by simpa using hne)))
  have hprod : (f - algebraMap K F a) * (f⁻¹ * algebraMap K F a⁻¹)
      ∈ w.toValuationSubring.nonunits :=
    w.mul_mem_nonunits hf (mul_mem hfinv (w.algebraMap_mem _))
  have := neg_mem hprod
  change f⁻¹ - algebraMap K F a⁻¹ ∈ w.toValuationSubring.nonunits
  convert this using 1
  have haF : algebraMap K F a ≠ 0 := by simpa using ha
  rw [map_inv₀]
  field_simp
  ring

variable {w} in
private theorem HasValueAt.div {f g : F} {a b : K} (hf : w.HasValueAt f a) (hg : w.HasValueAt g b)
    (hb : b ≠ 0) : w.HasValueAt (f / g) (a / b) := by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  exact hf.mul (hg.inv hb)

private theorem hasValueAt_iff_residue {f : F} (hf : f ∈ w.toValuationSubring) (a : K) :
    w.HasValueAt f a ↔
      residue w.toValuationSubring ⟨f, hf⟩ = algebraMap K w.ResidueField a := by
  have e : algebraMap K w.ResidueField a =
      residue w.toValuationSubring (algebraMap K w.toValuationSubring a) := rfl
  rw [e, ← sub_eq_zero, ← map_sub, residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff]
  rfl

private theorem exists_hasValueAt (hw : Function.Surjective (algebraMap K w.ResidueField)) {f : F}
    (hf : f ∈ w.toValuationSubring) : ∃ a : K, w.HasValueAt f a := by
  obtain ⟨a, ha⟩ := hw (residue w.toValuationSubring ⟨f, hf⟩)
  exact ⟨a, (w.hasValueAt_iff_residue hf a).mpr ha.symm⟩

private theorem surjective_algebraMap_residueField_of_isAlgClosed [IsAlgClosed K]
    [Module.Finite K w.ResidueField] : Function.Surjective (algebraMap K w.ResidueField) :=
  haveI : Algebra.IsIntegral K w.ResidueField := Algebra.IsIntegral.of_finite K w.ResidueField
  (IsAlgClosed.algebraMap_bijective_of_isIntegral (k := K) (K := w.ResidueField)).2

private theorem surjective_algebraMap_residueField_of_deg_eq_one [IsAlgClosed K] (h : w.deg = 1) :
    Function.Surjective (algebraMap K w.ResidueField) :=
  haveI : Module.Finite K w.ResidueField := Module.finite_of_finrank_eq_succ (n := 0) h
  w.surjective_algebraMap_residueField_of_isAlgClosed

variable (A : ValuationSubring K)

private def compSubring : Subring F where
  carrier := {f | ∃ a : A, w.HasValueAt f a}
  mul_mem' := by
    rintro f g ⟨a, ha⟩ ⟨b, hb⟩
    exact ⟨a * b, by simpa using ha.mul hb⟩
  one_mem' := ⟨1, by simpa using w.hasValueAt_algebraMap 1⟩
  add_mem' := by
    rintro f g ⟨a, ha⟩ ⟨b, hb⟩
    exact ⟨a + b, by simpa using ha.add hb⟩
  zero_mem' := ⟨0, by simpa using w.hasValueAt_algebraMap 0⟩
  neg_mem' := by
    rintro f ⟨a, ha⟩
    exact ⟨-a, by simpa using ha.neg⟩

variable {A} in
private theorem mem_compSubring_iff {f : F} : f ∈ w.compSubring A ↔ ∃ a : A, w.HasValueAt f a :=
  Iff.rfl

variable {A} in
private theorem mem_compSubring_of_hasValueAt {f : F} {a : K} (ha : a ∈ A) (h : w.HasValueAt f a) :
    f ∈ w.compSubring A :=
  ⟨⟨a, ha⟩, h⟩

private theorem compSubring_le : w.compSubring A ≤ w.toValuationSubring.toSubring := by
  rintro f ⟨a, ha⟩
  exact w.mem_of_hasValueAt ha

private theorem mem_compSubring_of_mem_nonunits {f : F} (hf : f ∈ w.toValuationSubring.nonunits) :
    f ∈ w.compSubring A :=
  ⟨0, by simpa [w.hasValueAt_zero_iff] using hf⟩

private theorem algebraMap_mem_compSubring_iff (a : K) : algebraMap K F a ∈ w.compSubring A ↔ a ∈ A
    := by
  constructor
  · rintro ⟨b, hb⟩
    rw [(w.hasValueAt_algebraMap a).unique hb]
    exact b.2
  · intro ha
    exact ⟨⟨a, ha⟩, w.hasValueAt_algebraMap a⟩

private def value : w.compSubring A →+* A where
  toFun f := Classical.choose f.2
  map_one' := Subtype.ext <|
    (Classical.choose_spec (w.compSubring A).one_mem).unique (by
      simpa using w.hasValueAt_algebraMap 1)
  map_mul' f g := Subtype.ext <|
    (Classical.choose_spec (mul_mem f.2 g.2)).unique (by
      simpa using (Classical.choose_spec f.2).mul (Classical.choose_spec g.2))
  map_zero' := Subtype.ext <|
    (Classical.choose_spec (w.compSubring A).zero_mem).unique (by
      simpa using w.hasValueAt_algebraMap 0)
  map_add' f g := Subtype.ext <|
    (Classical.choose_spec (add_mem f.2 g.2)).unique (by
      simpa using (Classical.choose_spec f.2).add (Classical.choose_spec g.2))

private theorem hasValueAt_value (f : w.compSubring A) : w.HasValueAt (f : F) (w.value A f : K) :=
  Classical.choose_spec f.2

variable {A} in
private theorem value_eq_of_hasValueAt {f : w.compSubring A} {a : A} (h : w.HasValueAt (f : F) a) :
    w.value A f = a :=
  Subtype.ext ((w.hasValueAt_value A f).unique h)

variable {A} in
private theorem ord_sub_value_pos {f : w.compSubring A} (hf : (f : F) ≠ algebraMap K F (w.value A
    f)) :
    0 < w.ord ((f : F) - algebraMap K F (w.value A f)) :=
  (w.hasValueAt_iff_ord_pos hf).mp (w.hasValueAt_value A f)

variable {A} in
private theorem value_eq_of_ord_pos {f : w.compSubring A} {a : A}
    (h : 0 < w.ord ((f : F) - algebraMap K F a)) : w.value A f = a :=
  w.value_eq_of_hasValueAt (w.hasValueAt_of_ord_pos h)

private theorem value_algebraMap (a : A) :
    w.value A ⟨algebraMap K F a, (w.algebraMap_mem_compSubring_iff A a).mpr a.2⟩ = a :=
  w.value_eq_of_hasValueAt (w.hasValueAt_algebraMap (a : K))

private theorem value_surjective : Function.Surjective (w.value A) :=
  fun a => ⟨_, w.value_algebraMap A a⟩

variable {A} in
private theorem value_eq_zero_of_mem_nonunits {f : w.compSubring A}
    (hf : (f : F) ∈ w.toValuationSubring.nonunits) : w.value A f = 0 :=
  w.value_eq_of_hasValueAt (by simpa [w.hasValueAt_zero_iff] using hf)

private def centre : Ideal (w.compSubring A) := (maximalIdeal A).comap (w.value A)

private instance centre_isPrime : (w.centre A).IsPrime := Ideal.comap_isPrime _ _

private instance centre_isMaximal : (w.centre A).IsMaximal :=
  Ideal.comap_isMaximal_of_surjective _ (w.value_surjective A)

variable {A} in
private theorem mem_centre_iff (f : w.compSubring A) : f ∈ w.centre A ↔ w.value A f ∈ maximalIdeal A
    :=
  Iff.rfl

variable {A} in
private theorem mem_centre_iff_of_hasValueAt {f : w.compSubring A} {a : A} (h : w.HasValueAt (f : F)
    a) :
    f ∈ w.centre A ↔ a ∈ maximalIdeal A := by
  rw [mem_centre_iff, w.value_eq_of_hasValueAt h]

variable {A} in
private theorem mem_centre_iff_of_ord_pos {f : w.compSubring A} {a : A}
    (h : 0 < w.ord ((f : F) - algebraMap K F a)) : f ∈ w.centre A ↔ a ∈ maximalIdeal A :=
  w.mem_centre_iff_of_hasValueAt (w.hasValueAt_of_ord_pos h)

variable {A} in
private theorem mem_centre_of_mem_nonunits {f : w.compSubring A}
    (hf : (f : F) ∈ w.toValuationSubring.nonunits) : f ∈ w.centre A := by
  rw [mem_centre_iff, w.value_eq_zero_of_mem_nonunits hf]
  exact Ideal.zero_mem _

variable {A} in
private theorem mem_centre_of_ord_pos {f : w.compSubring A} (hf : 0 < w.ord (f : F)) : f ∈ w.centre
    A :=
  w.mem_centre_of_mem_nonunits ((w.mem_nonunits_iff_ord_pos (by rintro h; simp [h] at hf)).mpr hf)

private theorem algebraMap_mem_centre_iff (a : A) :
    (⟨algebraMap K F a, (w.algebraMap_mem_compSubring_iff A a).mpr a.2⟩ : w.compSubring A)
        ∈ w.centre A ↔ a ∈ maximalIdeal A := by
  rw [mem_centre_iff, value_algebraMap]

private theorem mem_compSubring_or_inv_mem (hw : Function.Surjective (algebraMap K w.ResidueField))
    (f : F) : f ∈ w.compSubring A ∨ f⁻¹ ∈ w.compSubring A := by
  by_cases hf : f ∈ w.toValuationSubring
  · obtain ⟨c, hc⟩ := w.exists_hasValueAt hw hf
    by_cases hcA : c ∈ A
    · exact Or.inl ⟨⟨c, hcA⟩, hc⟩
    · right
      have hcA' : c⁻¹ ∈ A := (A.mem_or_inv_mem c).resolve_left hcA
      have hc0 : c ≠ 0 := fun h => hcA (h ▸ A.zero_mem)
      have hf0 : f ≠ 0 := by
        rintro rfl
        have : w.HasValueAt (0 : F) 0 := by simpa using w.hasValueAt_algebraMap 0
        exact hc0 (hc.unique this)
      have hfu : f ∉ w.toValuationSubring.nonunits := by
        intro hfn
        exact hc0 (hc.unique ((w.hasValueAt_zero_iff f).mpr hfn))
      have hfinv : f⁻¹ ∈ w.toValuationSubring := by
        by_contra hne
        exact hfu ((ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inr (by simpa using hne)))
      refine ⟨⟨c⁻¹, hcA'⟩, ?_⟩
      have hprod : (f - algebraMap K F c) * (f⁻¹ * algebraMap K F c⁻¹)
          ∈ w.toValuationSubring.nonunits :=
        w.mul_mem_nonunits hc (mul_mem hfinv (w.algebraMap_mem _))
      have := neg_mem hprod
      show f⁻¹ - algebraMap K F (c⁻¹ : K) ∈ w.toValuationSubring.nonunits
      convert this using 1
      have hcF : algebraMap K F c ≠ 0 := by simpa using hc0
      rw [map_inv₀]
      field_simp
      ring
  ·
    right
    refine w.mem_compSubring_of_mem_nonunits A ?_
    exact (ValuationSubring.inv_mem_nonunits_iff _).mpr (Or.inr hf)

private def compValuationSubring (hw : Function.Surjective (algebraMap K w.ResidueField)) :
    ValuationSubring F :=
  ValuationSubring.ofSubring (w.compSubring A) (w.mem_compSubring_or_inv_mem A hw)

@[simp]
private theorem compValuationSubring_toSubring (hw : Function.Surjective (algebraMap K
    w.ResidueField)) :
    (w.compValuationSubring A hw).toSubring = w.compSubring A := rfl

private theorem mem_compValuationSubring_iff (hw : Function.Surjective (algebraMap K
    w.ResidueField))
    (f : F) : f ∈ w.compValuationSubring A hw ↔ f ∈ w.compSubring A := Iff.rfl

private theorem mem_compSubring_of_isIntegral (hw : Function.Surjective (algebraMap K
    w.ResidueField))
    {S : Subring F} (hS : S ≤ w.compSubring A) {f : F} (hf : IsIntegral S f) :
    f ∈ w.compSubring A := by
  obtain ⟨p, hp, hpf⟩ := hf
  let V := w.compValuationSubring A hw
  let i : S →+* V := Subring.inclusion hS
  have hint : IsIntegral V f := by
    refine ⟨p.map i, hp.map i, ?_⟩
    rw [Polynomial.eval₂_map]
    exact hpf
  obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint
  rw [← hy]
  exact y.2

private theorem mem_compSubring_of_isIntegral' [IsAlgClosed K] {S : Subring F} (hS : S ≤
    w.compSubring A)
    {f : F} (hf : IsIntegral S f) : f ∈ w.compSubring A := by
  obtain ⟨p, hp, hpf⟩ := hf
  have hSO : ∀ s : S, (s : F) ∈ w.toValuationSubring := fun s => w.compSubring_le A (hS s.2)
  have hfO : f ∈ w.toValuationSubring := by
    refine w.mem_of_eval_monic_eq_zero (P := p.map S.subtype) (hp.map _) (fun i => ?_) ?_
    · rw [Polynomial.coeff_map]
      exact hSO _
    · rw [Polynomial.eval_map]
      exact hpf
  let vS : S →+* A := (w.value A).comp (Subring.inclusion hS)
  let ιS : S →+* w.toValuationSubring := S.subtype.codRestrict _ hSO
  have hres : (residue w.toValuationSubring).comp ιS =
      ((algebraMap K w.ResidueField).comp (algebraMap A K)).comp vS := by
    ext s
    change residue w.toValuationSubring ⟨s, hSO s⟩ =
      algebraMap K w.ResidueField ((w.value A ⟨s, hS s.2⟩ : A) : K)
    exact (w.hasValueAt_iff_residue (hSO s) _).mp (w.hasValueAt_value A ⟨s, hS s.2⟩)
  set r : w.ResidueField := residue w.toValuationSubring ⟨f, hfO⟩ with hr
  let Q : Polynomial A := p.map vS
  have hQ : Q.Monic := hp.map _
  have hzero : Polynomial.eval₂ ιS ⟨f, hfO⟩ p = 0 := by
    apply Subtype.val_injective
    change w.toValuationSubring.subtype (Polynomial.eval₂ ιS ⟨f, hfO⟩ p) = ((0 :
        w.toValuationSubring) : F)
    rw [Polynomial.hom_eval₂]
    exact hpf
  have hrootκ : Polynomial.eval₂ (algebraMap K w.ResidueField) r (Q.map (algebraMap A K)) = 0 := by
    rw [Polynomial.eval₂_map, Polynomial.eval₂_map, ← hres, hr, ← Polynomial.hom_eval₂, hzero,
      map_zero]
  have hint : IsIntegral K r := ⟨Q.map (algebraMap A K), hQ.map _, hrootκ⟩
  obtain ⟨c, hc⟩ : r ∈ (algebraMap K w.ResidueField).range :=
    minpoly.mem_range_of_degree_eq_one K r
      (IsAlgClosed.degree_eq_one_of_irreducible K (minpoly.irreducible hint))
  have hcroot : Polynomial.eval₂ (algebraMap A K) c Q = 0 := by
    apply (algebraMap K w.ResidueField).injective
    rw [Polynomial.hom_eval₂, ← Polynomial.eval₂_map, hc, hrootκ, map_zero]
  obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp (⟨Q, hQ, hcroot⟩ : IsIntegral A c)
  refine ⟨y, (w.hasValueAt_iff_residue hfO _).mpr ?_⟩
  rw [← hr, ← hc, ← hy]
  rfl

private theorem exists_unique_valueHom [IsAlgClosed K] (g : F) (B₀ : Subring F)
    (hint : ∀ b : B₀,
      ∃ p : Polynomial (Subring.closure (algebraMap K F '' (A : Set K) ∪ {g})),
        p.Monic ∧
          Polynomial.eval₂ (Subring.closure (algebraMap K F '' (A : Set K) ∪ {g})).subtype
            (b : F) p = 0)
    (hw : ∃ a : A, g - algebraMap K F (a : K) ∈ w.toValuationSubring.nonunits) :
    ∃! φ : B₀ →+* A, ∀ b : B₀,
      (b : F) - algebraMap K F ((φ b : A) : K) ∈ w.toValuationSubring.nonunits := by
  obtain ⟨a₀, ha₀⟩ := hw
  have hg : g ∈ w.compSubring A := w.mem_compSubring_of_hasValueAt a₀.2 ha₀
  have hS : Subring.closure (algebraMap K F '' (A : Set K) ∪ {g}) ≤ w.compSubring A := by
    rw [Subring.closure_le]
    rintro y (⟨c, hc, rfl⟩ | rfl)
    · exact (w.algebraMap_mem_compSubring_iff A c).mpr hc
    · exact hg
  have hB₀ : B₀ ≤ w.compSubring A := fun b hb => w.mem_compSubring_of_isIntegral' A hS (hint ⟨b,
      hb⟩)
  refine ⟨(w.value A).comp (Subring.inclusion hB₀), fun b => w.hasValueAt_value A ⟨b, hB₀ b.2⟩, ?_⟩
  intro ψ hψ
  refine RingHom.ext fun b => ?_
  have h1 : w.HasValueAt (b : F) ((ψ b : A) : K) := hψ b
  have h2 : ψ b = w.value A ⟨b, hB₀ b.2⟩ := Subtype.ext (h1.unique (w.hasValueAt_value A ⟨b, hB₀
      b.2⟩))
  exact h2

variable {A} in
private theorem residue_comp_value_surjective {B : Subring F} (hB : B ≤ w.compSubring A)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) :
    Function.Surjective
      (((IsLocalRing.residue A).comp (w.value A)).comp (Subring.inclusion hB)) := by
  intro x
  obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective x
  refine ⟨⟨algebraMap K F a, hconst a⟩, ?_⟩
  change IsLocalRing.residue A (w.value A ⟨algebraMap K F a, hB (hconst a)⟩) = _
  rw [w.value_eq_of_hasValueAt (w.hasValueAt_algebraMap (a : K))]

variable {A} in
private theorem ker_residue_comp_value {B : Subring F} (hB : B ≤ w.compSubring A) :
    RingHom.ker (((IsLocalRing.residue A).comp (w.value A)).comp (Subring.inclusion hB)) =
      (w.centre A).comap (Subring.inclusion hB) := by
  ext b
  rw [RingHom.mem_ker, Ideal.mem_comap, mem_centre_iff, RingHom.comp_apply, RingHom.comp_apply,
    IsLocalRing.residue_eq_zero_iff]

variable {A} in
private theorem centre_comap_isMaximal {B : Subring F} (hB : B ≤ w.compSubring A)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) :
    ((w.centre A).comap (Subring.inclusion hB)).IsMaximal := by
  rw [← w.ker_residue_comp_value hB]
  exact RingHom.ker_isMaximal_of_surjective _ (w.residue_comp_value_surjective hB hconst)

variable {A} in
private theorem sub_value_mem_centre_comap {B : Subring F} (hB : B ≤ w.compSubring A)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) (b : B) :
    b - ⟨algebraMap K F (w.value A ⟨b, hB b.2⟩ : K), hconst _⟩ ∈
      (w.centre A).comap (Subring.inclusion hB) := by
  rw [Ideal.mem_comap, mem_centre_iff]
  simp only [map_sub]
  have h1 : w.value A (Subring.inclusion hB ⟨algebraMap K F (w.value A ⟨b, hB b.2⟩ : K), hconst _⟩)
      = w.value A ⟨b, hB b.2⟩ :=
    w.value_eq_of_hasValueAt (w.hasValueAt_algebraMap _)
  have h2 : w.value A (Subring.inclusion hB b) = w.value A ⟨b, hB b.2⟩ := rfl
  rw [h1, h2, sub_self]
  exact Ideal.zero_mem _

variable {A} in
private theorem algebraMap_mem_centre_comap_iff {B : Subring F} (hB : B ≤ w.compSubring A)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) (a : A) :
    (⟨algebraMap K F a, hconst a⟩ : B) ∈ (w.centre A).comap (Subring.inclusion hB) ↔
      a ∈ maximalIdeal A := by
  rw [Ideal.mem_comap]
  exact w.algebraMap_mem_centre_iff A a

end Place

end AlgebraicCurve

set_option autoImplicit false

namespace ValuationSubring

variable {K : Type*} [Field K] (A : ValuationSubring K)

private theorem algebraMap_bijective_of_isIntegral_of_isAlgClosed [IsAlgClosed K]
    (R : Type*) [CommRing R] [IsDomain R] [Algebra A R] [FaithfulSMul A R]
    [Algebra.IsIntegral A R] : Function.Bijective (algebraMap A R) := by
  have hinj : Function.Injective (algebraMap A R) := FaithfulSMul.algebraMap_injective A R
  refine ⟨hinj, fun r => ?_⟩
  haveI : Algebra.IsAlgebraic A R := Algebra.IsIntegral.isAlgebraic
  let φ : R →ₐ[A] K := IsAlgClosed.lift
  have hφ : Function.Injective φ := by
    rw [injective_iff_map_eq_zero]
    intro x hx
    have hker : RingHom.ker φ.toRingHom = ⊥ := by
      refine Ideal.eq_bot_of_comap_eq_bot (R := A) ?_
      rw [eq_bot_iff]
      intro a ha
      rw [Ideal.mem_comap, RingHom.mem_ker] at ha
      change φ (algebraMap A R a) = 0 at ha
      rw [AlgHom.commutes] at ha
      have h0 : (a : K) = 0 := ha
      have ha0 : a = 0 := by exact_mod_cast h0
      rw [ha0]
      exact Ideal.zero_mem _
    have hmem : x ∈ RingHom.ker φ.toRingHom := hx
    rw [hker] at hmem
    exact Ideal.mem_bot.mp hmem
  have hint : IsIntegral A (φ r) := (Algebra.IsIntegral.isIntegral (R := A) r).map φ
  obtain ⟨a, ha⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint
  refine ⟨a, hφ ?_⟩
  rw [AlgHom.commutes, ha]

section Quotient

open Polynomial

variable {F : Type*} [Field F] [Algebra K F]

private abbrev constants : A →+* F := (algebraMap K F).comp A.subtype

variable {A}

private theorem exists_sub_constants_mem [IsAlgClosed K] {x : F} {B : Subring F}
    (hconst : ∀ a : A, A.constants a ∈ B) (hxB : x ∈ B)
    (hint : ∀ b : B, IsIntegral (Subring.closure (Set.range (A.constants (F := F)) ∪ {x})) (b : F))
    (𝔭 : Ideal B) [𝔭.IsPrime]
    (hbot : ∀ a : A, (⟨A.constants a, hconst a⟩ : B) ∈ 𝔭 → a = 0)
    (a₀ : A) (hx : (⟨x, hxB⟩ : B) - ⟨A.constants a₀, hconst a₀⟩ ∈ 𝔭) (b : B) :
    ∃ a : A, b - ⟨A.constants a, hconst a⟩ ∈ 𝔭 := by
  classical
  set S : Subring F := Subring.closure (Set.range (A.constants (F := F)) ∪ {x}) with hS
  have hSB : S ≤ B := by
    rw [hS, Subring.closure_le]
    rintro y (⟨a, rfl⟩ | rfl)
    exacts [hconst a, hxB]
  let cB : A →+* B := (A.constants (F := F)).codRestrict B hconst
  letI alg : Algebra A (B ⧸ 𝔭) := ((Ideal.Quotient.mk 𝔭).comp cB).toAlgebra
  have halg : ∀ a : A, algebraMap A (B ⧸ 𝔭) a = Ideal.Quotient.mk 𝔭 (cB a) := fun _ => rfl
  let ψ : S →+* B ⧸ 𝔭 := (Ideal.Quotient.mk 𝔭).comp (Subring.inclusion hSB)
  have step1 : ∀ (y : F) (hy : y ∈ S), ψ ⟨y, hy⟩ ∈ (algebraMap A (B ⧸ 𝔭)).range := by
    intro y hy
    induction hy using Subring.closure_induction with
    | mem y hy =>
      rcases hy with ⟨a, rfl⟩ | h
      · exact ⟨a, rfl⟩
      · have h' : x = y := (Set.mem_singleton_iff.mp h).symm
        subst h'
        refine ⟨a₀, ?_⟩
        rw [halg]
        change Ideal.Quotient.mk 𝔭 (cB a₀) = Ideal.Quotient.mk 𝔭 ⟨x, hxB⟩
        rw [Ideal.Quotient.eq]
        have := 𝔭.neg_mem hx
        rwa [neg_sub] at this
    | zero =>
      change ψ 0 ∈ _
      rw [map_zero]
      exact Subring.zero_mem _
    | one =>
      change ψ 1 ∈ _
      rw [map_one]
      exact Subring.one_mem _
    | add y z hy hz ihy ihz =>
      change ψ (⟨y, hy⟩ + ⟨z, hz⟩) ∈ _
      rw [map_add]
      exact Subring.add_mem _ ihy ihz
    | neg y hy ihy =>
      change ψ (-⟨y, hy⟩) ∈ _
      rw [map_neg]
      exact Subring.neg_mem _ ihy
    | mul y z hy hz ihy ihz =>
      change ψ (⟨y, hy⟩ * ⟨z, hz⟩) ∈ _
      rw [map_mul]
      exact Subring.mul_mem _ ihy ihz
  have step1' : ∀ s : S, ψ s ∈ (algebraMap A (B ⧸ 𝔭)).range := fun s => step1 s s.2
  haveI hintq : Algebra.IsIntegral A (B ⧸ 𝔭) := by
    refine ⟨fun y => ?_⟩
    obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective y
    obtain ⟨f, hf, hfb⟩ := hint b
    set g : Polynomial B := f.map (Subring.inclusion hSB) with hg
    have hgm : g.Monic := hf.map _
    have hgb : g.eval b = 0 := by
      apply Subtype.val_injective
      change B.subtype (eval b (f.map (Subring.inclusion hSB))) = ((0 : B) : F)
      rw [eval_map, hom_eval₂]
      exact hfb
    set gq : Polynomial (B ⧸ 𝔭) := g.map (Ideal.Quotient.mk 𝔭) with hgq
    have hgqm : gq.Monic := hgm.map _
    have hgqb : gq.eval (Ideal.Quotient.mk 𝔭 b) = 0 := by
      rw [hgq, eval_map, eval₂_hom, hgb, map_zero]
    have hlifts : gq ∈ Polynomial.lifts (algebraMap A (B ⧸ 𝔭)) := by
      rw [lifts_iff_coeff_lifts]
      intro n
      rw [hgq, coeff_map, hg, coeff_map]
      exact step1' (f.coeff n)
    obtain ⟨q, hqmap, -, hqm⟩ := lifts_and_degree_eq_and_monic hlifts hgqm
    refine ⟨q, hqm, ?_⟩
    rw [← eval_map, hqmap, hgqb]
  haveI : FaithfulSMul A (B ⧸ 𝔭) := by
    rw [faithfulSMul_iff_algebraMap_injective, injective_iff_map_eq_zero]
    intro a ha
    rw [halg, Ideal.Quotient.eq_zero_iff_mem] at ha
    exact hbot a ha
  obtain ⟨a, ha⟩ :=
    (A.algebraMap_bijective_of_isIntegral_of_isAlgClosed (B ⧸ 𝔭)).2 (Ideal.Quotient.mk 𝔭 b)
  refine ⟨a, ?_⟩
  rw [halg, Ideal.Quotient.eq] at ha
  have := 𝔭.neg_mem ha
  rwa [neg_sub] at this

private theorem constants_unique_mod {B : Subring F} (hconst : ∀ a : A, A.constants a ∈ B)
    (𝔭 : Ideal B) (hbot : ∀ a : A, (⟨A.constants a, hconst a⟩ : B) ∈ 𝔭 → a = 0)
    {a c : A} (h : (⟨A.constants a, hconst a⟩ : B) - ⟨A.constants c, hconst c⟩ ∈ 𝔭) : a = c := by
  have : (⟨A.constants (a - c), hconst (a - c)⟩ : B) ∈ 𝔭 := by
    convert h using 1
    apply Subtype.ext
    push_cast
    rw [map_sub]
  exact sub_eq_zero.mp (hbot _ this)

end Quotient

end ValuationSubring

set_option autoImplicit false

noncomputable section

open IsLocalRing IsDedekindDomain

namespace Subring

variable {F : Type*} [Field F] {B : Subring F}

private theorem exists_valuationSubring_dominating (𝔭 : Ideal B) [𝔭.IsPrime] :
    ∃ O : ValuationSubring F, B ≤ O.toSubring ∧ ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭 := by
  let L := Localization.AtPrime 𝔭
  have hunit : ∀ y : 𝔭.primeCompl, IsUnit (B.subtype y) := by
    intro y
    refine isUnit_iff_ne_zero.mpr fun h => y.2 ?_
    have : (y : B) = 0 := Subtype.ext h
    rw [this]
    exact 𝔭.zero_mem
  let f : L →+* F := IsLocalization.lift hunit
  have hf : ∀ b : B, f (algebraMap B L b) = b := fun b => IsLocalization.lift_eq hunit b
  obtain ⟨O, hO, hloc⟩ := IsLocalRing.exists_factor_valuationRing f
  refine ⟨O, fun b hb => ?_, fun b => ?_⟩
  · have := hO (algebraMap B L ⟨b, hb⟩)
    rwa [hf] at this
  ·
    let z : O := ⟨f (algebraMap B L b), hO _⟩
    have hz : f.codRestrict O.toSubring hO (algebraMap B L b) = z := rfl
    have key : IsUnit z ↔ b ∉ 𝔭 := by
      rw [← hz, isUnit_map_iff (f.codRestrict O.toSubring hO),
        IsLocalization.AtPrime.isUnit_to_map_iff L 𝔭 b]
      rfl
    have hzF : (z : F) = b := hf b
    rw [← hzF, ValuationSubring.coe_mem_nonunits_iff, IsLocalRing.mem_maximalIdeal,
        mem_nonunits_iff,
      key, not_not]

private theorem ne_top_of_dominating {𝔭 : Ideal B} {O : ValuationSubring F}
    (hdom : ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭) (h𝔭 : 𝔭 ≠ ⊥) : O ≠ ⊤ := by
  intro htop
  apply h𝔭
  rw [eq_bot_iff]
  intro b hb
  have hn : (b : F) ∈ O.nonunits := (hdom b).mpr hb
  rcases (ValuationSubring.mem_nonunits_iff_or _).mp hn with h0 | hinv
  · exact (Ideal.mem_bot).mpr (Subtype.ext h0)
  · exact absurd (htop ▸ ValuationSubring.mem_top _) hinv

private theorem algebraMap_mem_of_dominating {K : Type*} [Field K] [Algebra K F] (A :
    ValuationSubring K)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) {𝔭 : Ideal B} {O : ValuationSubring F}
    (hle : B ≤ O.toSubring) (hdom : ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭)
    (hbot : ∀ a : A, (⟨algebraMap K F a, hconst a⟩ : B) ∈ 𝔭 → a = 0) (c : K) :
    algebraMap K F c ∈ O := by
  by_cases hc : c ∈ A
  · exact hle (hconst ⟨c, hc⟩)
  · have hcinv : c⁻¹ ∈ A := (A.mem_or_inv_mem c).resolve_left hc
    have hc0 : c ≠ 0 := fun h => hc (h ▸ A.zero_mem)
    have hnot : (⟨algebraMap K F (c⁻¹ : K), hconst ⟨c⁻¹, hcinv⟩⟩ : B) ∉ 𝔭 := fun h =>
      inv_ne_zero hc0 (by simpa using congrArg Subtype.val (hbot ⟨c⁻¹, hcinv⟩ h))
    have hnu : algebraMap K F c⁻¹ ∉ O.nonunits := fun h => hnot ((hdom _).mp h)
    rw [map_inv₀, ValuationSubring.inv_mem_nonunits_iff, not_or] at hnu
    exact not_not.mp hnu.2

end Subring

namespace ValuationSubring

variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)

private def centreOver (hO : ∀ r : R, algebraMap R F r ∈ O) : Ideal R :=
  (IsLocalRing.maximalIdeal O).comap ((algebraMap R F).codRestrict O.toSubring hO)

private instance centreOver_isPrime (hO : ∀ r : R, algebraMap R F r ∈ O) : (O.centreOver hO).IsPrime
    :=
  Ideal.comap_isPrime _ _

omit [IsDedekindDomain R] [IsFractionRing R F] in
private theorem mem_centreOver_iff (hO : ∀ r : R, algebraMap R F r ∈ O) {r : R} :
    r ∈ O.centreOver hO ↔ algebraMap R F r ∈ O.nonunits := by
  rw [centreOver, Ideal.mem_comap, ← ValuationSubring.coe_mem_nonunits_iff]
  rfl

omit [IsDedekindDomain R] [IsFractionRing R F] in
private theorem inv_algebraMap_mem (hO : ∀ r : R, algebraMap R F r ∈ O) {s : R}
    (hs : s ∉ O.centreOver hO) : (algebraMap R F s)⁻¹ ∈ O := by
  rw [mem_centreOver_iff, ValuationSubring.mem_nonunits_iff, not_lt] at hs
  have hy : O.valuation (algebraMap R F s) ≤ 1 := (O.valuation_le_one_iff _).mpr (hO s)
  have h1 : O.valuation (algebraMap R F s) = 1 := le_antisymm hy hs
  apply (O.valuation_le_one_iff _).mp
  rw [map_inv₀, h1, inv_one]

private theorem centreOver_ne_bot (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) :
    O.centreOver hO ≠ ⊥ := by
  intro hbot
  apply hne
  refine SetLike.ext fun x => ⟨fun _ => ValuationSubring.mem_top x, fun _ => ?_⟩
  obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective (A := R) x
  rw [div_eq_mul_inv]
  refine O.mul_mem _ _ (hO a) (O.inv_algebraMap_mem hO fun hmem => ?_)
  rw [hbot, Ideal.mem_bot] at hmem
  exact nonZeroDivisors.ne_zero hb hmem

private def centreHeightOneSpectrum (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) :
    HeightOneSpectrum R :=
  ⟨O.centreOver hO, inferInstance, O.centreOver_ne_bot hO hne⟩

private theorem valuationSubringAtPrime_centre_le (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤)
    :
    HeightOneSpectrum.valuationSubringAtPrime F (O.centreHeightOneSpectrum hO hne) ≤ O := by
  rintro x ⟨a, s, hs, rfl⟩
  exact O.mul_mem _ _ (hO a) (O.inv_algebraMap_mem hO hs)

private theorem eq_valuationSubringAtPrime_centre (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤)
    :
    O = HeightOneSpectrum.valuationSubringAtPrime F (O.centreHeightOneSpectrum hO hne) :=
  (ValuationSubring.eq_of_le_of_ne_top _ (O.valuationSubringAtPrime_centre_le hO hne) hne).symm

private theorem isPrincipalIdealRing_of_dedekind_le (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠
    ⊤) :
    IsPrincipalIdealRing O := by
  rw [O.eq_valuationSubringAtPrime_centre hO hne]
  infer_instance

end ValuationSubring

namespace AlgebraicCurve

namespace Place

variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]

private def ofValuationSubringOver (O : ValuationSubring F) (hO : ∀ r : R, algebraMap R F r ∈ O)
    (hne : O ≠ ⊤) (hK : ∀ c : K, algebraMap K F c ∈ O) : Place K F where
  toValuationSubring := O
  algebraMap_mem' := hK
  ne_top' := hne
  isPrincipalIdealRing' := O.isPrincipalIdealRing_of_dedekind_le hO hne

@[simp]
private theorem ofValuationSubringOver_toValuationSubring (O : ValuationSubring F)
    (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) (hK : ∀ c : K, algebraMap K F c ∈ O) :
    (ofValuationSubringOver O hO hne hK).toValuationSubring = O := rfl

private theorem mem_nonunits_ofValuationSubringOver_iff (O : ValuationSubring F)
    (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) (hK : ∀ c : K, algebraMap K F c ∈ O)
    {B : Subring F} {𝔭 : Ideal B} (hdom : ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭) (b : B) :
    (b : F) ∈ (ofValuationSubringOver O hO hne hK).toValuationSubring.nonunits ↔ b ∈ 𝔭 :=
  hdom b

end Place

end AlgebraicCurve

set_option autoImplicit false

open IsLocalRing Polynomial

namespace Valuation

variable {R Γ₀ : Type*} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀]

private theorem exists_ne_map_eq_of_sum_eq_zero {ι : Type*} [DecidableEq ι] (v : Valuation R Γ₀)
    {s : Finset ι} {f : ι → R} (hs : ∑ i ∈ s, f i = 0) {j : ι} (hj : j ∈ s)
    (hj0 : v (f j) ≠ 0) (hmax : ∀ i ∈ s, v (f i) ≤ v (f j)) :
    ∃ i ∈ s, i ≠ j ∧ v (f i) = v (f j) := by
  by_contra h
  push Not at h
  have hlt : ∀ i ∈ s \ {j}, v (f i) < v (f j) := by
    intro i hi
    rw [Finset.mem_sdiff, Finset.mem_singleton] at hi
    exact lt_of_le_of_ne (hmax i hi.1) (h i hi.1 hi.2)
  have := v.map_sum_eq_of_lt hj hlt
  rw [hs, map_zero] at this
  exact hj0 this.symm

end Valuation

namespace ValuationSubring

variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]

private theorem natCast_mem_ker (ℓ : ℕ) [CharP k ℓ] (red : A →+* k) :
    ((ℓ : ℕ) : A) ∈ RingHom.ker red := by
  rw [RingHom.mem_ker, map_natCast, CharP.cast_eq_zero]

private theorem natCast_mem_maximalIdeal (ℓ : ℕ) [CharP k ℓ] (red : A →+* k) :
    ((ℓ : ℕ) : A) ∈ maximalIdeal A :=
  IsLocalRing.le_maximalIdeal (RingHom.ker_ne_top red) (A.natCast_mem_ker ℓ red)

private theorem isUnit_intCast_of_not_dvd (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k)
    {m : ℤ} (hm : ¬ (ℓ : ℤ) ∣ m) : IsUnit ((m : ℤ) : A) := by
  have hprime : Prime (ℓ : ℤ) := Nat.prime_iff_prime_int.mp Fact.out
  obtain ⟨a, b, hab⟩ := (Irreducible.coprime_iff_not_dvd hprime.irreducible).mpr hm
  have hA : (a : A) * ((ℓ : ℕ) : A) + (b : A) * (m : A) = 1 := by
    have := congrArg (Int.cast : ℤ → A) hab
    push_cast at this
    exact this
  have hℓm : (a : A) * ((ℓ : ℕ) : A) ∈ maximalIdeal A :=
    Ideal.mul_mem_left _ _ (A.natCast_mem_maximalIdeal ℓ red)
  have hu : IsUnit ((b : A) * (m : A)) := by
    by_contra hnu
    have hmem : (b : A) * (m : A) ∈ maximalIdeal A := (IsLocalRing.mem_maximalIdeal _).mpr hnu
    have h1 : (1 : A) ∈ maximalIdeal A := hA ▸ Ideal.add_mem _ hℓm hmem
    exact (IsLocalRing.maximalIdeal.isMaximal A).ne_top (Ideal.eq_top_of_isUnit_mem _ h1 isUnit_one)
  exact isUnit_of_mul_isUnit_right hu

private theorem map_intCast_eq_zero_of_not_isUnit (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k)
    {m : ℤ} (hm : ¬ IsUnit ((m : ℤ) : A)) : red (m : A) = 0 := by
  have hdvd : (ℓ : ℤ) ∣ m := by
    by_contra h
    exact hm (A.isUnit_intCast_of_not_dvd ℓ red h)
  obtain ⟨c, rfl⟩ := hdvd
  rw [map_intCast]
  push_cast
  rw [CharP.cast_eq_zero k ℓ, zero_mul]

private theorem map_eq_zero_of_rat_mem_maximalIdeal (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ]
    (red : A →+* k) (φ : ℚ →+* K) (r : ℚ) (hrA : φ r ∈ A)
    (hr : (⟨φ r, hrA⟩ : A) ∈ maximalIdeal A) : red ⟨φ r, hrA⟩ = 0 := by
  have hnum : (⟨φ r, hrA⟩ : A) * ((r.den : ℕ) : A) = ((r.num : ℤ) : A) := by
    apply Subtype.ext
    change φ r * (((r.den : ℕ) : A) : K) = (((r.num : ℤ) : A) : K)
    push_cast
    rw [← map_natCast φ, ← map_intCast φ, ← map_mul, Rat.mul_den_eq_num]
  have hnum_mem : ((r.num : ℤ) : A) ∈ maximalIdeal A := hnum ▸ Ideal.mul_mem_right _ _ hr
  have hnum0 : red ((r.num : ℤ) : A) = 0 :=
    A.map_intCast_eq_zero_of_not_isUnit ℓ red ((IsLocalRing.mem_maximalIdeal _).mp hnum_mem)
  have hden : ¬ (ℓ : ℤ) ∣ (r.den : ℤ) := by
    intro h
    have hℓnum : (ℓ : ℤ) ∣ r.num := by
      by_contra h'
      have hu : IsUnit ((r.num : ℤ) : A) := A.isUnit_intCast_of_not_dvd ℓ red h'
      exact (IsLocalRing.mem_maximalIdeal _).mp hnum_mem hu
    have h1 : (ℓ : ℤ) ∣ (Int.gcd r.num (r.den : ℤ) : ℤ) := Int.dvd_coe_gcd hℓnum h
    have hg : Int.gcd r.num (r.den : ℤ) = 1 := by
      simpa [Int.gcd, Int.natAbs_natCast] using r.reduced
    rw [hg] at h1
    have := Int.eq_one_of_dvd_one (by positivity) h1
    have hℓ1 : ℓ = 1 := by exact_mod_cast this
    exact (Fact.out : ℓ.Prime).one_lt.ne' hℓ1
  have hden0 : red ((r.den : ℕ) : A) ≠ 0 := by
    rw [map_natCast]
    intro h0
    rw [CharP.cast_eq_zero_iff k ℓ] at h0
    exact hden (by exact_mod_cast h0)
  have := congrArg red hnum
  rw [map_mul, hnum0] at this
  exact (mul_eq_zero.mp this).resolve_right hden0

private theorem exists_pow_valuation_eq_of_isRoot (φ : ℚ →+* K) {x : K} (hx0 : x ≠ 0)
    {p : ℚ[X]} (hp0 : p ≠ 0) (hpx : p.eval₂ φ x = 0) :
    ∃ n : ℕ, 0 < n ∧ ∃ r : ℚ, r ≠ 0 ∧ A.valuation (x ^ n) = A.valuation (φ r) := by
  classical
  set v := A.valuation with hv
  let f : ℕ → K := fun i => φ (p.coeff i) * x ^ i
  have hsum : ∑ i ∈ p.support, f i = 0 := by
    rw [eval₂_eq_sum, Polynomial.sum_def] at hpx
    exact hpx
  have hvx : v x ≠ 0 := (v.ne_zero_iff).mpr hx0
  have hf0 : ∀ i ∈ p.support, v (f i) ≠ 0 := by
    intro i hi
    refine (v.ne_zero_iff).mpr (mul_ne_zero ?_ (pow_ne_zero _ hx0))
    exact (map_ne_zero φ).mpr (mem_support_iff.mp hi)
  obtain ⟨j, hj, hjmax⟩ :=
    Finset.exists_max_image p.support (fun i => v (f i)) (support_nonempty.mpr hp0)
  obtain ⟨i, hi, hij, heq⟩ := v.exists_ne_map_eq_of_sum_eq_zero hsum hj (hf0 j hj) hjmax
  obtain ⟨a, b, hab, ha, hb, heq'⟩ :
      ∃ a b : ℕ, a < b ∧ a ∈ p.support ∧ b ∈ p.support ∧ v (f a) = v (f b) := by
    rcases lt_or_gt_of_ne hij with h | h
    · exact ⟨i, j, h, hi, hj, heq⟩
    · exact ⟨j, i, h, hj, hi, heq.symm⟩
  have hca0 : v (φ (p.coeff a)) ≠ 0 := (v.ne_zero_iff).mpr ((map_ne_zero φ).mpr (mem_support_iff.mp
      ha))
  have hcb0 : v (φ (p.coeff b)) ≠ 0 := (v.ne_zero_iff).mpr ((map_ne_zero φ).mpr (mem_support_iff.mp
      hb))
  have h1 : v (φ (p.coeff a)) * v x ^ a = (v (φ (p.coeff b)) * v x ^ (b - a)) * v x ^ a := by
    have e : v x ^ b = v x ^ (b - a) * v x ^ a := by rw [← pow_add, Nat.sub_add_cancel hab.le]
    have := heq'
    simp only [f, map_mul, map_pow] at this
    rw [this, e, ← mul_assoc]
  have h2 : v (φ (p.coeff a)) = v (φ (p.coeff b)) * v x ^ (b - a) :=
    mul_right_cancel₀ (pow_ne_zero _ hvx) h1
  refine ⟨b - a, Nat.sub_pos_of_lt hab, p.coeff a / p.coeff b,
    div_ne_zero (mem_support_iff.mp ha) (mem_support_iff.mp hb), ?_⟩
  rw [map_div₀, map_div₀, map_pow, h2, mul_div_cancel_left₀ _ hcb0]

private theorem ker_eq_maximalIdeal_of_isAlgebraic [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]
    (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) :
    RingHom.ker red = maximalIdeal A := by
  refine le_antisymm (IsLocalRing.le_maximalIdeal (RingHom.ker_ne_top red)) ?_
  intro x hx
  rw [RingHom.mem_ker]
  rcases eq_or_ne x 0 with rfl | hx0
  · exact map_zero red
  have hxK : (x : K) ≠ 0 := by simpa [ne_eq, ZeroMemClass.coe_eq_zero] using hx0
  obtain ⟨p, hp0, hpx⟩ := Algebra.IsAlgebraic.isAlgebraic (R := ℚ) (x : K)
  obtain ⟨n, hn, r, hr0, hval⟩ :=
    A.exists_pow_valuation_eq_of_isRoot (algebraMap ℚ K) hxK hp0 (by rwa [← aeval_def])
  obtain ⟨u, hu⟩ := (A.valuation_eq_iff _ _).mp hval
  have hcoe : ((((u⁻¹ : Aˣ) : A) * x ^ n : A) : K) = algebraMap ℚ K r := by
    push_cast
    rw [← hu, ← mul_assoc, ← MulMemClass.coe_mul, Units.inv_mul, OneMemClass.coe_one, one_mul]
  have hrA : algebraMap ℚ K r ∈ A := hcoe ▸ SetLike.coe_mem _
  have hxn : x ^ n = (u : A) * ⟨algebraMap ℚ K r, hrA⟩ := by
    apply Subtype.ext
    push_cast
    exact hu.symm
  have hrm : (⟨algebraMap ℚ K r, hrA⟩ : A) ∈ maximalIdeal A := by
    have hxnm : x ^ n ∈ maximalIdeal A := Ideal.pow_mem_of_mem _ hx n hn
    rw [hxn] at hxnm
    exact ((IsLocalRing.maximalIdeal.isMaximal A).isPrime.mem_or_mem hxnm).resolve_left
      (fun h => (IsLocalRing.mem_maximalIdeal _).mp h u.isUnit)
  have hr0' : red ⟨algebraMap ℚ K r, hrA⟩ = 0 :=
    A.map_eq_zero_of_rat_mem_maximalIdeal ℓ red (algebraMap ℚ K) r hrA hrm
  have : red (x ^ n) = 0 := by rw [hxn, map_mul, hr0', mul_zero]
  rw [map_pow] at this
  exact pow_eq_zero_iff hn.ne' |>.mp this

private theorem exists_mul_eq_one_of_map_ne_zero [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]
    (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) {a : A} (ha : red a ≠ 0) :
    ∃ b : A, red a * red b = 1 := by
  have hunit : IsUnit a := by
    by_contra h
    have : a ∈ RingHom.ker red := by
      rw [A.ker_eq_maximalIdeal_of_isAlgebraic ℓ red]
      exact (IsLocalRing.mem_maximalIdeal _).mpr h
    exact ha this
  obtain ⟨u, rfl⟩ := hunit
  exact ⟨((u⁻¹ : Aˣ) : A), by rw [← map_mul, Units.mul_inv, map_one]⟩

private theorem ker_eq_maximalIdeal_apply [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]
    (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) (a : A) :
    red a = 0 ↔ a ∈ maximalIdeal A := by
  rw [← RingHom.mem_ker, A.ker_eq_maximalIdeal_of_isAlgebraic ℓ red]

end ValuationSubring

set_option autoImplicit false

noncomputable section

open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial

namespace AlgebraicCurve

variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F}

private theorem isPrincipalIdealRing_adjoin_singleton (hj : Transcendental K j) :
    IsPrincipalIdealRing (Algebra.adjoin K ({j} : Set F)) :=
  IsPrincipalIdealRing.of_surjective (Polynomial.algEquivOfTranscendental K j hj).toRingHom
    (Polynomial.algEquivOfTranscendental K j hj).surjective

private theorem isDedekindDomain_adjoin_singleton (hj : Transcendental K j) :
    IsDedekindDomain (Algebra.adjoin K ({j} : Set F)) :=
  haveI := isPrincipalIdealRing_adjoin_singleton hj
  inferInstance

private theorem isDedekindDomain_integralClosure_adjoin (hj : Transcendental K j)
    [FiniteDimensional K⟮j⟯ F] [Algebra.IsSeparable K⟮j⟯ F] :
    IsDedekindDomain (integralClosure (Algebra.adjoin K ({j} : Set F)) F) :=
  haveI := isDedekindDomain_adjoin_singleton hj
  integralClosure.isDedekindDomain (Algebra.adjoin K ({j} : Set F)) K⟮j⟯ F

private theorem isFractionRing_integralClosure_adjoin (hj : Transcendental K j)
    [FiniteDimensional K⟮j⟯ F] :
    IsFractionRing (integralClosure (Algebra.adjoin K ({j} : Set F)) F) F :=
  haveI := isDedekindDomain_adjoin_singleton hj
  integralClosure.isFractionRing_of_finite_extension (A := Algebra.adjoin K ({j} : Set F)) K⟮j⟯ F

private theorem integralClosure_adjoin_le_valuationSubring (O : ValuationSubring F)
    (hK : ∀ c : K, algebraMap K F c ∈ O) (hjO : j ∈ O)
    (r : integralClosure (Algebra.adjoin K ({j} : Set F)) F) : (r : F) ∈ O := by
  let O' : Subalgebra K F :=
    { O.toSubring with
      algebraMap_mem' := hK }
  have hle : Algebra.adjoin K ({j} : Set F) ≤ O' :=
    Algebra.adjoin_le (Set.singleton_subset_iff.mpr hjO)
  let φ : Algebra.adjoin K ({j} : Set F) →+* O :=
    (Subalgebra.val _).toRingHom.codRestrict O.toSubring (fun y => hle y.2)
  obtain ⟨p, hp, hpr⟩ : IsIntegral (Algebra.adjoin K ({j} : Set F)) (r : F) := r.2
  have hint : IsIntegral O (r : F) := by
    refine ⟨p.map φ, hp.map φ, ?_⟩
    rw [eval₂_map]
    exact hpr
  obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint
  rw [← hy]
  exact y.2

private theorem algebraMap_mem_integralClosure_adjoin (c : K) :
    algebraMap K F c ∈ integralClosure (Algebra.adjoin K ({j} : Set F)) F := by
  rw [mem_integralClosure_iff, IsScalarTower.algebraMap_apply K (Algebra.adjoin K ({j} : Set F)) F]
  exact isIntegral_algebraMap

private theorem self_mem_integralClosure_adjoin :
    j ∈ integralClosure (Algebra.adjoin K ({j} : Set F)) F := by
  rw [mem_integralClosure_iff]
  have : j = algebraMap (Algebra.adjoin K ({j} : Set F)) F ⟨j, Algebra.self_mem_adjoin_singleton K
      j⟩ :=
    rfl
  rw [this]
  exact isIntegral_algebraMap

private theorem le_integralClosure_adjoin_of_isIntegral {S B : Subring F}
    (hS : S ≤ (Algebra.adjoin K ({j} : Set F)).toSubring)
    (hint : ∀ b : B, IsIntegral S (b : F)) (b : B) :
    (b : F) ∈ integralClosure (Algebra.adjoin K ({j} : Set F)) F := by
  rw [mem_integralClosure_iff]
  obtain ⟨p, hp, hpb⟩ := hint b
  let φ : S →+* Algebra.adjoin K ({j} : Set F) :=
    S.subtype.codRestrict (Algebra.adjoin K ({j} : Set F)).toSubring (fun y => hS y.2)
  refine ⟨p.map φ, hp.map φ, ?_⟩
  rw [eval₂_map]
  exact hpb

end AlgebraicCurve

set_option autoImplicit false

open Polynomial

namespace ValuationSubring

variable {K : Type*} [Field K] (A : ValuationSubring K) {k : Type*} [Field k]

private theorem isAlgClosed_of_surjective [IsAlgClosed K] (red : A →+* k)
    (hred : Function.Surjective red) : IsAlgClosed k := by
  refine IsAlgClosed.of_exists_root k fun p hp hirr => ?_
  have hlifts : p ∈ Polynomial.lifts red := (lifts_iff_coeff_lifts p).mpr fun n => hred _
  obtain ⟨P, hPp, hPdeg, hP⟩ := lifts_and_degree_eq_and_monic hlifts hp
  have hdegK : (P.map (algebraMap A K)).degree ≠ 0 := by
    rw [hP.degree_map, hPdeg]
    exact (degree_pos_of_irreducible hirr).ne'
  obtain ⟨x, hx⟩ := IsAlgClosed.exists_root (P.map (algebraMap A K)) hdegK
  have hint : IsIntegral A x := ⟨P, hP, by rwa [IsRoot.def, eval_map] at hx⟩
  obtain ⟨y, rfl⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint
  have hy : P.eval y = 0 := by
    apply IsFractionRing.injective A K
    rw [map_zero, ← Polynomial.eval₂_at_apply, ← eval_map]
    exact hx
  refine ⟨red y, ?_⟩
  rw [← hPp, eval_map, Polynomial.eval₂_at_apply, hy, map_zero]

end ValuationSubring

set_option autoImplicit false

namespace RingHom

variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)

private def imagePrime (𝔮 : Ideal B) : Ideal π.range := 𝔮.map π.rangeRestrict

variable {π} in
private theorem rangeRestrict_mem_imagePrime_iff {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (b : B) :
    π.rangeRestrict b ∈ π.imagePrime 𝔮 ↔ b ∈ 𝔮 := by
  rw [imagePrime, ← Ideal.mem_comap, Ideal.comap_map_of_surjective _ π.rangeRestrict_surjective,
    ← RingHom.ker, ker_rangeRestrict, sup_eq_left.mpr hker]

variable {π} in
private theorem mk_mem_imagePrime_iff {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (b : B)
    (hb : π b ∈ π.range := π.mem_range_self b) :
    (⟨π b, hb⟩ : π.range) ∈ π.imagePrime 𝔮 ↔ b ∈ 𝔮 :=
  rangeRestrict_mem_imagePrime_iff hker b

variable {π} in
private theorem mem_imagePrime_iff {𝔮 : Ideal B} (y : π.range) :
    y ∈ π.imagePrime 𝔮 ↔ ∃ b ∈ 𝔮, π.rangeRestrict b = y := by
  rw [imagePrime, Ideal.mem_map_iff_of_surjective _ π.rangeRestrict_surjective]

variable {π} in
private theorem imagePrime_ne_top {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (h𝔮 : 𝔮 ≠ ⊤) :
    π.imagePrime 𝔮 ≠ ⊤ := by
  intro htop
  apply h𝔮
  rw [Ideal.eq_top_iff_one, ← rangeRestrict_mem_imagePrime_iff hker, map_one, htop]
  exact Submodule.mem_top

variable {π} in
private theorem imagePrime_isPrime {𝔮 : Ideal B} [𝔮.IsPrime] (hker : ker π ≤ 𝔮) :
    (π.imagePrime 𝔮).IsPrime :=
  Ideal.map_isPrime_of_surjective π.rangeRestrict_surjective (by rwa [ker_rangeRestrict])

variable {π} in
private theorem imagePrime_isMaximal {𝔮 : Ideal B} [h : 𝔮.IsMaximal] (hker : ker π ≤ 𝔮) :
    (π.imagePrime 𝔮).IsMaximal :=
  (Ideal.map_eq_top_or_isMaximal_of_surjective _ π.rangeRestrict_surjective h).resolve_left
    (imagePrime_ne_top hker h.ne_top)

variable {π} in
private theorem eq_zero_of_const_mem_imagePrime {A k : Type*} [CommRing A] [CommRing k]
    (σ : A →+* B) (red : A →+* k) (ι : k →+* C) (hcompat : ∀ a : A, π (σ a) = ι (red a))
    (hred : Function.Surjective red) {𝔮 : Ideal B} (hker : ker π ≤ 𝔮)
    (h𝔮 : ∀ a : A, σ a ∈ 𝔮 → red a = 0) (c : k) (hc : ι c ∈ π.range)
    (hmem : (⟨ι c, hc⟩ : π.range) ∈ π.imagePrime 𝔮) : c = 0 := by
  obtain ⟨a, rfl⟩ := hred c
  refine h𝔮 a ((rangeRestrict_mem_imagePrime_iff hker (σ a)).mp ?_)
  convert hmem using 1
  exact Subtype.ext (hcompat a)

variable {π} in
private theorem const_mem_range {A k : Type*} [CommRing A] [CommRing k]
    (σ : A →+* B) (red : A →+* k) (ι : k →+* C) (hcompat : ∀ a : A, π (σ a) = ι (red a))
    (hred : Function.Surjective red) (c : k) : ι c ∈ π.range := by
  obtain ⟨a, rfl⟩ := hred c
  exact ⟨σ a, hcompat a⟩

end RingHom

namespace AlgebraicCurve

namespace Place

variable {K F : Type*} [Field K] [Field F] [Algebra K F]

private theorem eq_zero_of_X_sub_C_dvd_C {R : Type*} [CommRing R] {a₀ a : R}
    (h : (Polynomial.X - Polynomial.C a₀) ∣ Polynomial.C a) : a = 0 := by
  obtain ⟨g, hg⟩ := h
  have := congrArg (Polynomial.eval a₀) hg
  simpa using this

private theorem exists_place_centre_comap_eq [IsAlgClosed K] (A : ValuationSubring K) {j : F}
    (hj : Transcendental K j) [FiniteDimensional K⟮j⟯ F] [Algebra.IsSeparable K⟮j⟯ F]
    {B : Subring F} (hconst : ∀ a : A, algebraMap K F a ∈ B) (hjB : j ∈ B)
    (hint : ∀ b : B,
      IsIntegral (Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {j})) (b : F))
    (𝔮 : Ideal B) [𝔮.IsPrime]
    (h𝔮A : ∀ a : A, (⟨algebraMap K F a, hconst a⟩ : B) ∈ 𝔮 ↔ a ∈ IsLocalRing.maximalIdeal A)
    (a₀ : A) (hja : (⟨j, hjB⟩ : B) - ⟨algebraMap K F a₀, hconst a₀⟩ ∈ 𝔮) :
    ∃ (w : Place K F) (hB : B ≤ w.compSubring A),
      (w.centre A).comap (Subring.inclusion hB) = 𝔮 ∧ w.HasValueAt j a₀ := by
  classical
  set S : Subring F := Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {j})
    with hSdef
  have hSB : S ≤ B := by
    rw [hSdef, Subring.closure_le]
    rintro y (⟨a, rfl⟩ | rfl)
    exacts [hconst a, hjB]
  haveI : IsIntegrallyClosed S := A.isIntegrallyClosed_closure hj
  have hjS : j ∈ S := Subring.subset_closure (Or.inr rfl)
  have hcS : ∀ a : A, algebraMap K F a ∈ S := fun a => Subring.subset_closure (Or.inl ⟨a, rfl⟩)
  let e := A.polynomialEquivClosure hj
  have heX : (e Polynomial.X : F) = j := by
    rw [ValuationSubring.polynomialEquivClosure_apply, Polynomial.aeval_X]
  have heC : ∀ a : A, (e (Polynomial.C a) : F) = algebraMap K F a := fun a => by
    rw [ValuationSubring.polynomialEquivClosure_apply, Polynomial.aeval_C]
    rfl
  have hegen : e (Polynomial.X - Polynomial.C a₀) = ⟨j, hjS⟩ - ⟨algebraMap K F a₀, hcS a₀⟩ := by
    apply Subtype.ext
    rw [map_sub]
    push_cast
    rw [heX, heC]
  let p₀ : Ideal (Polynomial A) := Ideal.span {Polynomial.X - Polynomial.C a₀}
  haveI hp₀ : p₀.IsPrime := by
    rw [← Ideal.Quotient.isDomain_iff_prime]
    exact (Polynomial.quotientSpanXSubCAlgEquiv a₀).toMulEquiv.isDomain_iff.mpr inferInstance
  let p : Ideal S := p₀.map e.toRingHom
  haveI hp : p.IsPrime := Ideal.map_isPrime_of_equiv e
  have hp_span : p = Ideal.span {(⟨j, hjS⟩ : S) - ⟨algebraMap K F a₀, hcS a₀⟩} := by
    change Ideal.map e.toRingHom (Ideal.span _) = _
    rw [Ideal.map_span, Set.image_singleton]
    exact congrArg (fun y => Ideal.span {y}) hegen
  let q : Ideal S := 𝔮.comap (Subring.inclusion hSB)
  have hpq : p ≤ q := by
    rw [hp_span, Ideal.span_le, Set.singleton_subset_iff]
    change Subring.inclusion hSB (⟨j, hjS⟩ - ⟨algebraMap K F a₀, hcS a₀⟩) ∈ 𝔮
    rw [map_sub]
    exact hja
  obtain ⟨𝔭, h𝔭𝔮, h𝔭, h𝔭p⟩ :=
    Subring.exists_ideal_le_comap_eq_of_isIntegral hSB hint hpq 𝔮 rfl
  haveI := h𝔭
  have hj𝔭 : (⟨j, hjB⟩ : B) - ⟨algebraMap K F a₀, hconst a₀⟩ ∈ 𝔭 := by
    have : (⟨j, hjS⟩ : S) - ⟨algebraMap K F a₀, hcS a₀⟩ ∈ 𝔭.comap (Subring.inclusion hSB) := by
      rw [h𝔭p, hp_span]
      exact Ideal.subset_span rfl
    rw [Ideal.mem_comap, map_sub] at this
    exact this
  have hbot : ∀ a : A, (⟨algebraMap K F a, hconst a⟩ : B) ∈ 𝔭 → a = 0 := by
    intro a ha
    have h1 : (⟨algebraMap K F a, hcS a⟩ : S) ∈ 𝔭.comap (Subring.inclusion hSB) := by
      rw [Ideal.mem_comap]
      exact ha
    rw [h𝔭p, hp_span, Ideal.mem_span_singleton'] at h1
    obtain ⟨g, hg⟩ := h1
    have h3 : e (Polynomial.C a) = ⟨algebraMap K F a, hcS a⟩ := Subtype.ext (heC a)
    have h4 : e.symm g * (Polynomial.X - Polynomial.C a₀) = Polynomial.C a := by
      apply e.injective
      rw [map_mul, e.apply_symm_apply, hegen, h3, hg]
    exact eq_zero_of_X_sub_C_dvd_C ⟨e.symm g, by rw [mul_comm]; exact h4.symm⟩
  have hj_ne : j - algebraMap K F a₀ ≠ 0 := by
    intro h
    apply hj
    rw [sub_eq_zero] at h
    rw [h]
    exact isAlgebraic_algebraMap (a₀ : K)
  have h𝔭ne : 𝔭 ≠ ⊥ := by
    intro h
    rw [h, Ideal.mem_bot] at hj𝔭
    exact hj_ne (by simpa using congrArg Subtype.val hj𝔭)
  obtain ⟨O, hle, hdom⟩ := Subring.exists_valuationSubring_dominating 𝔭
  have hne : O ≠ ⊤ := Subring.ne_top_of_dominating hdom h𝔭ne
  have hK : ∀ c : K, algebraMap K F c ∈ O :=
    Subring.algebraMap_mem_of_dominating A hconst hle hdom hbot
  let R := integralClosure (Algebra.adjoin K ({j} : Set F)) F
  haveI : IsDedekindDomain R := isDedekindDomain_integralClosure_adjoin hj
  haveI : IsFractionRing R F := isFractionRing_integralClosure_adjoin hj
  have hO : ∀ r : R, algebraMap R F r ∈ O := fun r =>
    integralClosure_adjoin_le_valuationSubring O hK (hle hjB) r
  let w : Place K F := Place.ofValuationSubringOver O hO hne hK
  have hval : w.HasValueAt j a₀ := by
    have := (hdom (⟨j, hjB⟩ - ⟨algebraMap K F a₀, hconst a₀⟩)).mpr hj𝔭
    simp at this
    exact this
  have hS_le : S ≤ w.compSubring A := by
    rw [hSdef, Subring.closure_le]
    rintro y (⟨a, rfl⟩ | rfl)
    · exact (w.algebraMap_mem_compSubring_iff A _).mpr a.2
    · exact w.mem_compSubring_of_hasValueAt a₀.2 hval
  have hB : B ≤ w.compSubring A := fun b hb => w.mem_compSubring_of_isIntegral' A hS_le (hint ⟨b,
      hb⟩)
  refine ⟨w, hB, ?_, hval⟩
  have h𝔭𝔓 : 𝔭 ≤ (w.centre A).comap (Subring.inclusion hB) := fun x hx =>
    w.mem_centre_of_mem_nonunits ((hdom x).mpr hx)
  ext b
  obtain ⟨a, hab⟩ := ValuationSubring.exists_sub_constants_mem hconst hjB hint 𝔭 hbot a₀ hj𝔭 b
  have hab' : b - ⟨algebraMap K F a, hconst a⟩ ∈ 𝔭 := hab
  have key : ∀ (I : Ideal B), 𝔭 ≤ I →
      (b ∈ I ↔ (⟨algebraMap K F a, hconst a⟩ : B) ∈ I) := by
    intro I hI
    constructor
    · intro hb
      have := I.sub_mem hb (hI hab')
      rwa [sub_sub_cancel] at this
    · intro ha
      have := I.add_mem (hI hab') ha
      rwa [sub_add_cancel] at this
  rw [key _ h𝔭𝔓, key _ h𝔭𝔮, w.algebraMap_mem_centre_comap_iff hB hconst, h𝔮A]

end Place

end AlgebraicCurve

namespace AlgebraicCurve

namespace Place

variable {K E : Type*} [Field K] [Field E] [Algebra K E]

private theorem finite_residueField_of_adjoin_simple_eq_top_of_mem {x : E} (hx : Transcendental K x)
    (htop : IntermediateField.adjoin K ({x} : Set E) = ⊤) (v : Place K E)
    (hxv : x ∈ v.toValuationSubring) : Module.Finite K v.ResidueField := by
  classical
  haveI : IsDedekindDomain (Algebra.adjoin K ({x} : Set E)) := isDedekindDomain_adjoin_singleton hx
  haveI : FaithfulSMul (Algebra.adjoin K ({x} : Set E)) E :=
    (faithfulSMul_iff_algebraMap_injective _ E).mpr Subtype.val_injective
  haveI : IsFractionRing (Algebra.adjoin K ({x} : Set E)) E := by
    refine IsFractionRing.of_field (Algebra.adjoin K ({x} : Set E)) E (fun z => ?_)
    have hz : z ∈ IntermediateField.adjoin K ({x} : Set E) := by
      rw [htop]
      exact IntermediateField.mem_top
    obtain ⟨r, hr, s, hs, rfl⟩ := IntermediateField.mem_adjoin_iff_div.mp hz
    exact ⟨⟨r, hr⟩, ⟨s, hs⟩, rfl⟩
  set O := v.toValuationSubring with hOdef
  have hO : ∀ r : Algebra.adjoin K ({x} : Set E), algebraMap _ E r ∈ O := by
    intro r
    have hle : Algebra.adjoin K ({x} : Set E) ≤
        { O.toSubring with algebraMap_mem' := v.algebraMap_mem' } :=
      Algebra.adjoin_le (Set.singleton_subset_iff.mpr hxv)
    exact hle r.2
  have hne : O ≠ ⊤ := v.ne_top'
  let xO : O := ⟨x, hxv⟩
  let xbar : v.ResidueField := IsLocalRing.residue O xO
  have hcomp : (IsLocalRing.residue O).comp (algebraMap K O) = algebraMap K v.ResidueField :=
    RingHom.ext fun _ => rfl
  have hres_aeval : ∀ p : K[X], IsLocalRing.residue O (Polynomial.aeval xO p) =
      Polynomial.aeval xbar p := fun p => by
    rw [Polynomial.aeval_def, Polynomial.aeval_def, Polynomial.hom_eval₂, hcomp]
  have hcoe_aeval : ∀ p : K[X], ((Polynomial.aeval xO p : O) : E) = Polynomial.aeval x p :=
    fun p => by
    have := Polynomial.aeval_algHom_apply (IsScalarTower.toAlgHom K O E) xO p
    exact this.symm
  let e := Polynomial.algEquivOfTranscendental K x hx
  have hcoe_e : ∀ p : K[X], ((e p : Algebra.adjoin K ({x} : Set E)) : E) = Polynomial.aeval x p :=
    fun p => by
    rw [Polynomial.algEquivOfTranscendental_apply, Polynomial.aeval_subalgebra_coe]
  have hOe : ∀ p : K[X], (⟨((e p : Algebra.adjoin K ({x} : Set E)) : E), hO (e p)⟩ : O) =
      Polynomial.aeval xO p := fun p => Subtype.ext (by rw [hcoe_aeval, hcoe_e])
  obtain ⟨f, hf𝔭, hf0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot (O.centreOver_ne_bot hO hne)
  obtain ⟨g, rfl⟩ := e.surjective f
  have hg0 : g ≠ 0 := fun h => hf0 (by rw [h, map_zero])
  have hgbar : Polynomial.aeval xbar g = 0 := by
    rw [← hres_aeval, IsLocalRing.residue_eq_zero_iff, ← hOe,
      ← ValuationSubring.coe_mem_nonunits_iff]
    exact (O.mem_centreOver_iff hO).mp hf𝔭
  have halg : IsAlgebraic K xbar := ⟨g, hg0, hgbar⟩
  have hint : IsIntegral K xbar := halg.isIntegral
  haveI : FiniteDimensional K K⟮xbar⟯ := IntermediateField.adjoin.finiteDimensional hint
  have htop' : K⟮xbar⟯ = ⊤ := by
    rw [eq_top_iff]
    intro y _
    obtain ⟨z, rfl⟩ := IsLocalRing.residue_surjective y
    have hz : (z : E) ∈ IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime E
        (O.centreHeightOneSpectrum hO hne) := by
      rw [← O.eq_valuationSubringAtPrime_centre hO hne]
      exact z.2
    obtain ⟨a, s, hs, hz'⟩ := hz
    obtain ⟨ga, rfl⟩ := e.surjective a
    obtain ⟨gs, rfl⟩ := e.surjective s
    have hsn : ((e gs : Algebra.adjoin K ({x} : Set E)) : E) ∉ O.nonunits := fun h =>
      hs ((O.mem_centreOver_iff hO).mpr h)
    have hres_s : IsLocalRing.residue O (Polynomial.aeval xO gs) ≠ 0 := by
      rw [Ne, IsLocalRing.residue_eq_zero_iff, ← hOe, ← ValuationSubring.coe_mem_nonunits_iff]
      exact hsn
    have hs0 : ((e gs : Algebra.adjoin K ({x} : Set E)) : E) ≠ 0 := fun h =>
      hsn (h ▸ (zero_mem O.nonunits))
    have hmul : z * Polynomial.aeval xO gs = Polynomial.aeval xO ga := by
      rw [← hOe, ← hOe]
      apply Subtype.ext
      change (z : E) * _ = _
      push_cast
      rw [hz']
      exact inv_mul_cancel_right₀ hs0 _
    have hzq : IsLocalRing.residue O z =
        Polynomial.aeval xbar ga / Polynomial.aeval xbar gs := by
      rw [eq_div_iff (by rwa [← hres_aeval]), ← hres_aeval, ← hres_aeval, ← map_mul, hmul]
    rw [hzq]
    refine div_mem ?_ ?_ <;>
      exact IntermediateField.algebra_adjoin_le_adjoin K _ (Polynomial.aeval_mem_adjoin_singleton K
          _)
  have : FiniteDimensional K (⊤ : IntermediateField K v.ResidueField) := by
    rw [← htop']
    infer_instance
  exact IntermediateField.topEquiv.toLinearEquiv.finiteDimensional

private theorem _root_.IntermediateField.adjoin_simple_inv_eq (x : E) :
    IntermediateField.adjoin K ({x⁻¹} : Set E) = IntermediateField.adjoin K ({x} : Set E) := by
  apply le_antisymm
  · rw [IntermediateField.adjoin_simple_le_iff]
    exact inv_mem (IntermediateField.mem_adjoin_simple_self K x)
  · rw [IntermediateField.adjoin_simple_le_iff]
    have h := inv_mem (IntermediateField.mem_adjoin_simple_self K x⁻¹)
    rwa [inv_inv] at h

private theorem finite_residueField_of_adjoin_simple_eq_top {x : E} (hx : Transcendental K x)
    (htop : IntermediateField.adjoin K ({x} : Set E) = ⊤) (v : Place K E) :
    Module.Finite K v.ResidueField := by
  by_cases hxv : x ∈ v.toValuationSubring
  · exact finite_residueField_of_adjoin_simple_eq_top_of_mem hx htop v hxv
  ·
    have hxinv : x⁻¹ ∈ v.toValuationSubring := (v.toValuationSubring.mem_or_inv_mem x).resolve_left
        hxv
    have hx' : Transcendental K x⁻¹ := fun h => hx (by simpa using h.inv)
    have htop' : IntermediateField.adjoin K ({x⁻¹} : Set E) = ⊤ := by
      rw [IntermediateField.adjoin_simple_inv_eq x, htop]
    exact finite_residueField_of_adjoin_simple_eq_top_of_mem hx' htop' v hxinv

private theorem finiteResidue_of_adjoin_simple_eq_top {x : E} (hx : Transcendental K x)
    (htop : IntermediateField.adjoin K ({x} : Set E) = ⊤) (v : Place K E) : v.FiniteResidue :=
  ⟨finite_residueField_of_adjoin_simple_eq_top hx htop v⟩

end Place

end AlgebraicCurve

namespace ValuationSubring

variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]

private theorem eq_of_forall_mem_nonunits_iff {O₁ O₂ : ValuationSubring F}
    (h₁ : ∀ r : R, algebraMap R F r ∈ O₁) (hne₁ : O₁ ≠ ⊤)
    (h₂ : ∀ r : R, algebraMap R F r ∈ O₂) (hne₂ : O₂ ≠ ⊤)
    (h : ∀ r : R, algebraMap R F r ∈ O₁.nonunits ↔ algebraMap R F r ∈ O₂.nonunits) :
    O₁ = O₂ := by
  have hc : O₁.centreHeightOneSpectrum h₁ hne₁ = O₂.centreHeightOneSpectrum h₂ hne₂ := by
    ext r
    change r ∈ O₁.centreOver h₁ ↔ r ∈ O₂.centreOver h₂
    rw [mem_centreOver_iff, mem_centreOver_iff]
    exact h r
  rw [O₁.eq_valuationSubringAtPrime_centre h₁ hne₁, O₂.eq_valuationSubringAtPrime_centre h₂ hne₂,
    hc]

end ValuationSubring

namespace AlgebraicCurve

namespace Place

variable {K F : Type*} [Field K] [Field F] [Algebra K F]

private theorem eq_of_forall_mem_nonunits_iff (R : Type*) [CommRing R] [IsDedekindDomain R]
    [Algebra R F] [IsFractionRing R F] {v₁ v₂ : Place K F}
    (h₁ : ∀ r : R, algebraMap R F r ∈ v₁.toValuationSubring)
    (h₂ : ∀ r : R, algebraMap R F r ∈ v₂.toValuationSubring)
    (h : ∀ r : R, algebraMap R F r ∈ v₁.toValuationSubring.nonunits ↔
      algebraMap R F r ∈ v₂.toValuationSubring.nonunits) : v₁ = v₂ :=
  Place.ext (ValuationSubring.eq_of_forall_mem_nonunits_iff h₁ v₁.ne_top' h₂ v₂.ne_top' h)

private theorem eq_of_forall_mem_nonunits_iff_of_surjective (R : Type*) [CommRing R]
    [IsDedekindDomain R]
    [Algebra R F] [IsFractionRing R F] {v₁ v₂ : Place K F}
    (h₁ : ∀ r : R, algebraMap R F r ∈ v₁.toValuationSubring)
    (h₂ : ∀ r : R, algebraMap R F r ∈ v₂.toValuationSubring)
    {ι : Type*} (f : ι → F) (hsurj : ∀ r : R, ∃ i, f i = algebraMap R F r)
    (h : ∀ i, f i ∈ v₁.toValuationSubring.nonunits ↔ f i ∈ v₂.toValuationSubring.nonunits) :
    v₁ = v₂ :=
  eq_of_forall_mem_nonunits_iff R h₁ h₂ fun r => by
    obtain ⟨i, hi⟩ := hsurj r
    rw [← hi]
    exact h i

variable (K) in
private theorem integralClosure_adjoin_le_of_forall_isIntegral_mem {j : F} {S : Subring F}
    (hK : ∀ c : K, algebraMap K F c ∈ S) (hj : j ∈ S)
    (hS : ∀ x : F, (∃ p : Polynomial S, p.Monic ∧ Polynomial.eval₂ S.subtype x p = 0) → x ∈ S)
    (r : integralClosure (Algebra.adjoin K ({j} : Set F)) F) : (r : F) ∈ S := by
  let S' : Subalgebra K F := { S with algebraMap_mem' := hK }
  have hle : Algebra.adjoin K ({j} : Set F) ≤ S' := Algebra.adjoin_le (Set.singleton_subset_iff.mpr
      hj)
  let φ : Algebra.adjoin K ({j} : Set F) →+* S :=
    (Subalgebra.val _).toRingHom.codRestrict S (fun y => hle y.2)
  obtain ⟨p, hp, hpr⟩ : IsIntegral (Algebra.adjoin K ({j} : Set F)) (r : F) := r.2
  refine hS r ⟨p.map φ, hp.map φ, ?_⟩
  rw [Polynomial.eval₂_map]
  exact hpr

private theorem exists_eq_of_integralClosure_adjoin {j : F} {B : Type*} (π : B → F) {S : Subring F}
    (hrange : ∀ x, x ∈ S ↔ ∃ b, π b = x)
    (hK : ∀ c : K, algebraMap K F c ∈ S) (hj : j ∈ S)
    (hS : ∀ x : F, (∃ p : Polynomial S, p.Monic ∧ Polynomial.eval₂ S.subtype x p = 0) → x ∈ S)
    (r : integralClosure (Algebra.adjoin K ({j} : Set F)) F) :
    ∃ b, π b = algebraMap (integralClosure (Algebra.adjoin K ({j} : Set F)) F) F r :=
  (hrange r).mp (integralClosure_adjoin_le_of_forall_isIntegral_mem K hK hj hS r)

end Place

end AlgebraicCurve

namespace ModularCurve
namespace CharPModel

open AlgebraicCurve AlgebraicCurve.Place

section SpecializationConstruction

variable {A : ValuationSubring (AlgebraicClosure ℚ)} {N : ℕ} [NeZero N]
  {ℓ : ℕ} [Fact ℓ.Prime] {k : Type*} [Field k] [CharP k ℓ] {red : A →+* k}

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.bfin_le_compSubring (fm : FibreModel N A ℓ k red)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    fm.BFin ≤ (w.compSubring A : Subring (laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N))) := by
  have hS : affineBaseFin N A ≤ w.compSubring A := by
    refine Subring.closure_le.mpr ?_
    rintro x (⟨a, rfl⟩ | rfl)
    · exact (w.algebraMap_mem_compSubring_iff A _).mpr a.2
    · exact hwFin
  exact fun x hx => w.mem_compSubring_of_isIntegral' A hS (fm.integralFin ⟨x, hx⟩)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.constFin_mem' (fm : FibreModel N A ℓ k red) :
    ∀ a : A, algebraMap (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) a ∈ fm.BFin :=
  fm.constFin_mem

private noncomputable def FibreModel.centreFin (fm : FibreModel N A ℓ k red)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) : Ideal fm.BFin :=
  (w.centre A).comap (Subring.inclusion (fm.bfin_le_compSubring w hwFin))

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.centreFin_isMaximal (fm : FibreModel N A ℓ k red)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    (fm.centreFin w hwFin).IsMaximal :=
  w.centre_comap_isMaximal (fm.bfin_le_compSubring w hwFin) fm.constFin_mem'

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.ker_piFin_le_centreFin (fm : FibreModel N A ℓ k red)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    RingHom.ker fm.piFin ≤ fm.centreFin w hwFin := by
  rw [fm.ker_piFin, Ideal.span_le]
  rintro x ⟨a, ha, rfl⟩
  show _ ∈ (w.centre A).comap (Subring.inclusion (fm.bfin_le_compSubring w hwFin))
  rw [Ideal.mem_comap]
  exact (w.algebraMap_mem_centre_iff A a).mpr ha

include ℓ in
set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem red_eq_zero_of_mem_maximalIdeal
    {a : A} (ha : a ∈ IsLocalRing.maximalIdeal A) : red a = 0 := by
  have hker := @ValuationSubring.ker_eq_maximalIdeal_of_isAlgebraic _ _ A _ _
    (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ) ℓ _ _ red
  exact RingHom.mem_ker.mp (hker ▸ ha)

private noncomputable def lineClosure (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    Subalgebra (Algebra.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))
      (modularFunctionFieldC k N) :=
  integralClosure (Algebra.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))
    (modularFunctionFieldC k N)

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.exists_spFin (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (data : ModularPolynomialData N)
    (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    ∃ v' : Place k (modularFunctionFieldC k N),
      ∀ b : fm.BFin, (fm.piFin b : modularFunctionFieldC k N) ∈
        v'.toValuationSubring.nonunits ↔ b ∈ fm.centreFin w hwFin := by
  haveI hmax : (fm.centreFin w hwFin).IsMaximal := fm.centreFin_isMaximal w hwFin
  have hker := fm.ker_piFin_le_centreFin w hwFin
  haveI hPmax : (fm.piFin.imagePrime (fm.centreFin w hwFin)).IsMaximal :=
    fm.piFin.imagePrime_isMaximal hker
  haveI hPprime : (fm.piFin.imagePrime (fm.centreFin w hwFin)).IsPrime := hPmax.isPrime
  obtain ⟨O, hle, hdom⟩ := Subring.exists_valuationSubring_dominating
    (B := fm.piFin.range) (fm.piFin.imagePrime (fm.centreFin w hwFin))
  have hPne : fm.piFin.imagePrime (fm.centreFin w hwFin) ≠ ⊥ := by
    have hmem : (⟨jBar N, fm.jBar_mem⟩ : fm.BFin) -
        ⟨constantsHom N A (w.value A ⟨jBar N, hwFin⟩), fm.constFin_mem _⟩ ∈
        fm.centreFin w hwFin :=
      w.sub_value_mem_centre_comap (fm.bfin_le_compSubring w hwFin) fm.constFin_mem' _
    have hy : fm.piFin.rangeRestrict
        ((⟨jBar N, fm.jBar_mem⟩ : fm.BFin) -
          ⟨constantsHom N A (w.value A ⟨jBar N, hwFin⟩), fm.constFin_mem _⟩) ∈
        fm.piFin.imagePrime (fm.centreFin w hwFin) :=
      (fm.piFin.rangeRestrict_mem_imagePrime_iff hker _).mpr hmem
    intro hbot
    rw [hbot, Ideal.mem_bot] at hy
    have hval : fm.piFin ((⟨jBar N, fm.jBar_mem⟩ : fm.BFin) -
        ⟨constantsHom N A (w.value A ⟨jBar N, hwFin⟩), fm.constFin_mem _⟩) = 0 := by
      have := congrArg Subtype.val hy
      simpa using this
    rw [map_sub] at hval
    have hj : fm.piFin ⟨jBar N, fm.jBar_mem⟩ = jLine k N := fm.piFin_j
    have hc : fm.piFin ⟨constantsHom N A (w.value A ⟨jBar N, hwFin⟩), fm.constFin_mem _⟩
        = algebraMap k (modularFunctionFieldC k N) (red (w.value A ⟨jBar N, hwFin⟩)) :=
      fm.piFin_const _
    rw [hj, hc, sub_eq_zero] at hval
    exact (transcendental_jLine k N) (hval ▸ isAlgebraic_algebraMap _)
  have hne : O ≠ ⊤ := Subring.ne_top_of_dominating hdom hPne
  have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piFin.range := by
    intro c
    obtain ⟨a, rfl⟩ := hred c
    exact ⟨⟨constantsHom N A a, fm.constFin_mem a⟩, (fm.piFin_const a).symm ▸ rfl⟩
  have hK : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ O := by
    intro c
    obtain ⟨a, rfl⟩ := hred c
    exact hle (hconstR (red a))
  haveI hFD : FiniteDimensional
      (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))
      (modularFunctionFieldC k N) := finiteDimensional_adjoin_jC k N data
  haveI hSep : Algebra.IsSeparable
      (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))
      (modularFunctionFieldC k N) := isSeparable_line_fibre k N data hsep
  haveI hDed : IsDedekindDomain (lineClosure k N) :=
    isDedekindDomain_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLine k N)
  haveI hFrac : IsFractionRing (lineClosure k N) (modularFunctionFieldC k N) :=
    isFractionRing_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLine k N)
  have hjO : (jLine k N : modularFunctionFieldC k N) ∈ O := by
    have h := hle (fm.piFin.mem_range_self ⟨jBar N, fm.jBar_mem⟩)
    have hj : fm.piFin ⟨jBar N, fm.jBar_mem⟩ = jLine k N := fm.piFin_j
    rwa [hj] at h
  refine ⟨Place.ofValuationSubringOver (R := lineClosure k N)
    O (fun r => integralClosure_adjoin_le_valuationSubring O hK hjO r) hne hK, ?_⟩
  intro b
  exact (hdom (fm.piFin.rangeRestrict b)).trans
    (fm.piFin.rangeRestrict_mem_imagePrime_iff hker b)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem transcendental_jLineInv (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    Transcendental k (((jLine k N)⁻¹ : modularFunctionFieldC k N)) := by
  intro h
  exact transcendental_jLine k N (by simpa using h.inv)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.binf_le_compSubring (fm : FibreModel N A ℓ k red)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    fm.BInf ≤ (w.compSubring A : Subring (laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N))) := by
  have hS : affineBaseInf N A ≤ w.compSubring A := by
    refine Subring.closure_le.mpr ?_
    rintro x (⟨a, rfl⟩ | rfl)
    · exact (w.algebraMap_mem_compSubring_iff A _).mpr a.2
    · exact hwInf
  exact fun x hx => w.mem_compSubring_of_isIntegral' A hS (fm.integralInf ⟨x, hx⟩)

private noncomputable def FibreModel.centreInf (fm : FibreModel N A ℓ k red)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) : Ideal fm.BInf :=
  (w.centre A).comap (Subring.inclusion (fm.binf_le_compSubring w hwInf))

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.centreInf_isMaximal (fm : FibreModel N A ℓ k red)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    (fm.centreInf w hwInf).IsMaximal :=
  w.centre_comap_isMaximal (fm.binf_le_compSubring w hwInf) fm.constInf_mem

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.ker_piInf_le_centreInf (fm : FibreModel N A ℓ k red)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    RingHom.ker fm.piInf ≤ fm.centreInf w hwInf := by
  rw [fm.ker_piInf, Ideal.span_le]
  rintro x ⟨a, ha, rfl⟩
  show _ ∈ (w.centre A).comap (Subring.inclusion (fm.binf_le_compSubring w hwInf))
  rw [Ideal.mem_comap]
  exact (w.algebraMap_mem_centre_iff A a).mpr ha

private noncomputable def lineClosureInf (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    Subalgebra (Algebra.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N))))
      (modularFunctionFieldC k N) :=
  integralClosure (Algebra.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N))))
    (modularFunctionFieldC k N)

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.exists_spInf (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (data : ModularPolynomialData N)
    (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    ∃ v' : Place k (modularFunctionFieldC k N),
      ∀ b : fm.BInf, (fm.piInf b : modularFunctionFieldC k N) ∈
        v'.toValuationSubring.nonunits ↔ b ∈ fm.centreInf w hwInf := by
  haveI hmax : (fm.centreInf w hwInf).IsMaximal := fm.centreInf_isMaximal w hwInf
  have hker := fm.ker_piInf_le_centreInf w hwInf
  haveI hPmax : (fm.piInf.imagePrime (fm.centreInf w hwInf)).IsMaximal :=
    fm.piInf.imagePrime_isMaximal hker
  haveI hPprime : (fm.piInf.imagePrime (fm.centreInf w hwInf)).IsPrime := hPmax.isPrime
  obtain ⟨O, hle, hdom⟩ := Subring.exists_valuationSubring_dominating
    (B := fm.piInf.range) (fm.piInf.imagePrime (fm.centreInf w hwInf))
  have hPne : fm.piInf.imagePrime (fm.centreInf w hwInf) ≠ ⊥ := by
    have hmem : (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) -
        ⟨constantsHom N A (w.value A ⟨(jBar N)⁻¹, hwInf⟩), fm.constInf_mem _⟩ ∈
        fm.centreInf w hwInf :=
      w.sub_value_mem_centre_comap (fm.binf_le_compSubring w hwInf) fm.constInf_mem _
    have hy : fm.piInf.rangeRestrict
        ((⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) -
          ⟨constantsHom N A (w.value A ⟨(jBar N)⁻¹, hwInf⟩), fm.constInf_mem _⟩) ∈
        fm.piInf.imagePrime (fm.centreInf w hwInf) :=
      (fm.piInf.rangeRestrict_mem_imagePrime_iff hker _).mpr hmem
    intro hbot
    rw [hbot, Ideal.mem_bot] at hy
    have hval : fm.piInf ((⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) -
        ⟨constantsHom N A (w.value A ⟨(jBar N)⁻¹, hwInf⟩), fm.constInf_mem _⟩) = 0 := by
      have := congrArg Subtype.val hy
      simpa using this
    rw [map_sub] at hval
    have hj : fm.piInf ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ = (jLine k N)⁻¹ := fm.piInf_jInv
    have hc : fm.piInf ⟨constantsHom N A (w.value A ⟨(jBar N)⁻¹, hwInf⟩), fm.constInf_mem _⟩
        = algebraMap k (modularFunctionFieldC k N)
            (red (w.value A ⟨(jBar N)⁻¹, hwInf⟩)) := fm.piInf_const _
    rw [hj, hc, sub_eq_zero] at hval
    exact (transcendental_jLineInv k N) (hval ▸ isAlgebraic_algebraMap _)
  have hne : O ≠ ⊤ := Subring.ne_top_of_dominating hdom hPne
  have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piInf.range := by
    intro c
    obtain ⟨a, rfl⟩ := hred c
    exact ⟨⟨constantsHom N A a, fm.constInf_mem a⟩, (fm.piInf_const a).symm ▸ rfl⟩
  have hK : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ O := by
    intro c
    obtain ⟨a, rfl⟩ := hred c
    exact hle (hconstR (red a))
  haveI hFD : FiniteDimensional
      (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N))))
      (modularFunctionFieldC k N) := by
    rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)]
    exact finiteDimensional_adjoin_jC k N data
  haveI hSep : Algebra.IsSeparable
      (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N))))
      (modularFunctionFieldC k N) := by
    rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)]
    exact isSeparable_line_fibre k N data hsep
  haveI hDed : IsDedekindDomain (lineClosureInf k N) :=
    isDedekindDomain_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLineInv k N)
  haveI hFrac : IsFractionRing (lineClosureInf k N) (modularFunctionFieldC k N) :=
    isFractionRing_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLineInv k N)
  have hjO : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ O := by
    have h := hle (fm.piInf.mem_range_self ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩)
    have hj : fm.piInf ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ = (jLine k N)⁻¹ := fm.piInf_jInv
    rwa [hj] at h
  refine ⟨Place.ofValuationSubringOver (R := lineClosureInf k N)
    O (fun r => integralClosure_adjoin_le_valuationSubring O hK hjO r) hne hK, ?_⟩
  intro b
  exact (hdom (fm.piInf.rangeRestrict b)).trans
    (fm.piInf.rangeRestrict_mem_imagePrime_iff hker b)

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.chart_dichotomy (_fm : FibreModel N A ℓ k red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) :
    (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
        ∈ w.compSubring A ∨
      ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
        ∈ w.compSubring A := by
  haveI hFD : FiniteDimensional
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) :=
    finiteDimensional_lineBar_of_dataAll N dataAll
  haveI h1 : Module.Finite
      ((w.restrict (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))).ResidueField)
      w.ResidueField :=
    rf_finite_residueField w
  haveI h2 : Module.Finite (AlgebraicClosure ℚ)
      ((w.restrict (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))).ResidueField) := by
    have htop : IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({⟨jBar N, IntermediateField.mem_adjoin_simple_self _ (jBar N)⟩} :
          Set (IntermediateField.adjoin (AlgebraicClosure ℚ)
            ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionFieldFull N))))) = ⊤ := by
      have h := adjoin_val_preimage_eq_top (K := AlgebraicClosure ℚ)
        (F := IntermediateField.adjoin (AlgebraicClosure ℚ)
          ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
            (modularFunctionFieldFull N))))
        (S := {jBar N}) rfl
      have hset : (Subtype.val ⁻¹' {jBar N} :
          Set (IntermediateField.adjoin (AlgebraicClosure ℚ)
            ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionFieldFull N)))))
          = {⟨jBar N, IntermediateField.mem_adjoin_simple_self _ (jBar N)⟩} := by
        ext z
        simp only [Set.mem_preimage, Set.mem_singleton_iff]
        exact ⟨fun hz => Subtype.ext hz, fun hz => by rw [hz]⟩
      rwa [hset] at h
    exact AlgebraicCurve.Place.finite_residueField_of_adjoin_simple_eq_top
      (transcendental_subtype _ (IntermediateField.mem_adjoin_simple_self _ (jBar N))
        (transcendental_jBar N)) htop _
  haveI h3 : Module.Finite (AlgebraicClosure ℚ) w.ResidueField :=
    Module.Finite.trans
      ((w.restrict (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))).ResidueField)
      w.ResidueField
  exact w.mem_compSubring_or_inv_mem A
    (w.surjective_algebraMap_residueField_of_isAlgClosed) (jBar N)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem fibreEvalSwap_subtype (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ)
        (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom
      (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) = 0 := by
  have hcomp : ((modularFunctionFieldC k N).val.toRingHom).comp
      (Polynomial.aeval (R := ℤ)
        (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom
      = (Polynomial.aeval (R := ℤ) (jqNModC k N)).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
        AlgHom.coe_toRingHom, Polynomial.aeval_X]
      rfl
  have h := Polynomial.hom_eval₂ data.Φ
    (Polynomial.aeval (R := ℤ)
      (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom
    ((modularFunctionFieldC k N).val.toRingHom)
    (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)
  apply Subtype.val_injective
  have h0 : (modularFunctionFieldC k N).val.toRingHom
      (data.Φ.eval₂ (Polynomial.aeval (R := ℤ)
        (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom
        (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)) = 0 := by
    rw [h, hcomp]
    exact fibreEvalSwap_eq_zero N data hsym k
  simpa using h0

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem barEvalSwap_laurent (N : ℕ) [NeZero N] (data : ModularPolynomialData N)
    (hsym : EvalSymm data.Φ) :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ)
        (coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq))).toRingHom
      (coeffEmb (AlgebraicClosure ℚ) jq) = 0 := by
  have hswap0 : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (qExpand ℚ N jq)).toRingHom jq
      = 0 := by
    rw [show qExpand ℚ N jq = jqN N from rfl, hsym (jqN N) jq]
    have h0 := data.eval_eq_zero
    rw [show evalAtJ = (Polynomial.aeval (R := ℤ) jq).toRingHom from rfl] at h0
    exact h0
  have hcomp : ((coeffEmb (AlgebraicClosure ℚ)).comp
      (Polynomial.aeval (R := ℤ) (qExpand ℚ N jq)).toRingHom)
      = (Polynomial.aeval (R := ℤ)
          (coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq))).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
        AlgHom.coe_toRingHom, Polynomial.aeval_X]
  have h := Polynomial.hom_eval₂ data.Φ
    (Polynomial.aeval (R := ℤ) (qExpand ℚ N jq)).toRingHom
    (coeffEmb (AlgebraicClosure ℚ)) jq
  rw [hswap0, map_zero, hcomp] at h
  exact h.symm

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem barEvalSwap_subtype (N : ℕ) [NeZero N] (data : ModularPolynomialData N)
    (hsym : EvalSymm data.Φ) :
    data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom (jBar N) = 0 := by
  have hcomp : (((laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)).val.toRingHom).comp
      (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom)
      = (Polynomial.aeval (R := ℤ)
          (coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq))).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,
        AlgHom.coe_toRingHom, Polynomial.aeval_X]
      rfl
  have h := Polynomial.hom_eval₂ data.Φ
    (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom
    ((laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom)
    (jBar N)
  apply Subtype.val_injective
  have h0 : (laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)).val.toRingHom
      (data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom (jBar N)) = 0 := by
    rw [h, hcomp]
    exact barEvalSwap_laurent N data hsym
  simpa using h0

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem transcendental_jNC (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) :
    Transcendental k (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) := by
  intro halg
  haveI hFD : FiniteDimensional k
      (IntermediateField.adjoin k
        ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N))) :=
    IntermediateField.adjoin.finiteDimensional halg.isIntegral
  have h2 : IsIntegral
      (IntermediateField.adjoin k
        ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N)))
      (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) :=
    isIntegral_adjoin_of_bivar_monic data.monic (fibreEvalSwap_subtype k N data hsym)
  have h3 : IsIntegral k (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) := by
    haveI : Algebra.IsIntegral k
        (IntermediateField.adjoin k
          ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N))) :=
      Algebra.IsIntegral.of_finite _ _
    exact isIntegral_trans _ h2
  exact (transcendental_jC k N) h3.isAlgebraic

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem transcendental_jNBar (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) :
    Transcendental (AlgebraicClosure ℚ) (jNBar N) := by
  intro halg
  haveI hFD : FiniteDimensional (AlgebraicClosure ℚ)
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jNBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)))) :=
    IntermediateField.adjoin.finiteDimensional halg.isIntegral
  have h2 : IsIntegral
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jNBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))
      (jBar N) :=
    isIntegral_adjoin_of_bivar_monic data.monic (barEvalSwap_subtype N data hsym)
  have h3 : IsIntegral (AlgebraicClosure ℚ) (jBar N) := by
    haveI : Algebra.IsIntegral (AlgebraicClosure ℚ)
        (IntermediateField.adjoin (AlgebraicClosure ℚ)
          ({jNBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
            (modularFunctionFieldFull N)))) :=
      Algebra.IsIntegral.of_finite _ _
    exact isIntegral_trans _ h2
  exact (transcendental_jBar N) h3.isAlgebraic

private theorem jBar_ne_const (N : ℕ) [NeZero N] (c : AlgebraicClosure ℚ) :
    jBar N ≠ algebraMap (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) c :=
  fun h => transcendental_jBar N (h ▸ isAlgebraic_algebraMap c)

private theorem jLine_ne_const (k : Type*) [Field k] (N : ℕ) [NeZero N] (c : k) :
    jLine k N ≠ algebraMap k (modularFunctionFieldC k N) c :=
  fun h => transcendental_jLine k N (h ▸ isAlgebraic_algebraMap c)

private theorem jLine_ne_zero (k : Type*) [Field k] (N : ℕ) [NeZero N] :
    (jLine k N : modularFunctionFieldC k N) ≠ 0 :=
  fun h => transcendental_jLine k N (h ▸ isAlgebraic_zero)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem mem_of_ord_nonneg {k' F' : Type*} [Field k'] [Field F'] [Algebra k' F']
    (v : Place k' F') {x : F'} (hx : x ≠ 0) (h : 0 ≤ v.ord x) :
    x ∈ v.toValuationSubring := by
  by_contra hmem
  rcases v.toValuationSubring.mem_or_inv_mem x with hx' | hinv
  · exact hmem hx'
  have hinv_nu : x⁻¹ ∈ v.toValuationSubring.nonunits := by
    refine (ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inr ?_)
    rwa [inv_inv]
  have hpos : 0 < v.ord x⁻¹ :=
    (v.mem_nonunits_iff_ord_pos (inv_ne_zero hx)).mp hinv_nu
  rw [v.ord_inv] at hpos
  exact absurd h (not_le.mpr (neg_pos.mp hpos))

open Classical in
private noncomputable def FibreModel.sp (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable) :
    Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) →
    Place k (modularFunctionFieldC k N) :=
  fun w =>
    if h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) ∈ w.compSubring A then
      (fm.exists_spFin hred (dataAll N (dvd_refl N)) hsep w h).choose
    else
      (fm.exists_spInf hred (dataAll N (dvd_refl N)) hsep w
        ((fm.chart_dichotomy dataAll w).resolve_left h)).choose

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_spec_fin (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    ∀ b : fm.BFin, (fm.piFin b : modularFunctionFieldC k N) ∈
      (fm.sp hred dataAll hsep w).toValuationSubring.nonunits ↔
        b ∈ fm.centreFin w h := by
  have hsp : fm.sp hred dataAll hsep w
      = (fm.exists_spFin hred (dataAll N (dvd_refl N)) hsep w h).choose := by
    unfold FibreModel.sp
    rw [dif_pos h]
  rw [hsp]
  exact (fm.exists_spFin hred (dataAll N (dvd_refl N)) hsep w h).choose_spec

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_spec_inf (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    ∀ b : fm.BInf, (fm.piInf b : modularFunctionFieldC k N) ∈
      (fm.sp hred dataAll hsep w).toValuationSubring.nonunits ↔
        b ∈ fm.centreInf w ((fm.chart_dichotomy dataAll w).resolve_left h) := by
  have hsp : fm.sp hred dataAll hsep w
      = (fm.exists_spInf hred (dataAll N (dvd_refl N)) hsep w
          ((fm.chart_dichotomy dataAll w).resolve_left h)).choose := by
    unfold FibreModel.sp
    rw [dif_neg h]
  rw [hsp]
  exact (fm.exists_spInf hred (dataAll N (dvd_refl N)) hsep w
    ((fm.chart_dichotomy dataAll w).resolve_left h)).choose_spec

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.value_jInv_mem_maximalIdeal (fm : FibreModel N A ℓ k red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    w.value A ⟨(jBar N)⁻¹, (fm.chart_dichotomy dataAll w).resolve_left h⟩ ∈
      IsLocalRing.maximalIdeal A := by
  have hinv := (fm.chart_dichotomy dataAll w).resolve_left h
  by_contra hcu
  have hcu' : IsUnit (w.value A ⟨(jBar N)⁻¹, hinv⟩) := by
    by_contra hn
    exact hcu ((IsLocalRing.mem_maximalIdeal _).mpr hn)
  obtain ⟨u, hu⟩ := hcu'
  have hc0 : ((w.value A ⟨(jBar N)⁻¹, hinv⟩ : A) : AlgebraicClosure ℚ) ≠ 0 := by
    intro h0
    apply hcu
    have hz : w.value A ⟨(jBar N)⁻¹, hinv⟩ = 0 := Subtype.ext h0
    rw [hz]
    exact zero_mem _
  have hmul : ((u : A) : AlgebraicClosure ℚ) * (((u⁻¹ : Aˣ) : A) : AlgebraicClosure ℚ)
      = 1 := by
    exact_mod_cast congrArg (Subtype.val) (Units.mul_inv u)
  have hd : (((u⁻¹ : Aˣ) : A) : AlgebraicClosure ℚ)
      = ((w.value A ⟨(jBar N)⁻¹, hinv⟩ : A) : AlgebraicClosure ℚ)⁻¹ := by
    rw [← hu] at hc0 ⊢
    exact eq_inv_of_mul_eq_one_right (by rw [mul_comm] at hmul ⊢; exact hmul)
  have hv := (w.hasValueAt_value A ⟨(jBar N)⁻¹, hinv⟩).inv hc0
  rw [inv_inv, ← hd] at hv
  exact h (w.mem_compSubring_of_hasValueAt ((u⁻¹ : Aˣ) : A).2 hv)

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_ord_jLine_neg (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    (fm.sp hred dataAll hsep w).ord (jLine k N) < 0 := by
  have hinv := (fm.chart_dichotomy dataAll w).resolve_left h
  have hcent : (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) ∈
      fm.centreInf w hinv := by
    show _ ∈ (w.centre A).comap (Subring.inclusion (fm.binf_le_compSubring w hinv))
    rw [Ideal.mem_comap]
    exact (w.mem_centre_iff _).mpr (fm.value_jInv_mem_maximalIdeal dataAll w h)
  have hnu := (fm.sp_spec_inf hred dataAll hsep w h ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩).mpr hcent
  rw [show fm.piInf ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ = (jLine k N)⁻¹ from fm.piInf_jInv] at hnu
  have hpos : 0 < (fm.sp hred dataAll hsep w).ord ((jLine k N : modularFunctionFieldC k N))⁻¹ :=
    ((fm.sp hred dataAll hsep w).mem_nonunits_iff_ord_pos
      (inv_ne_zero (jLine_ne_zero k N))).mp hnu
  rw [(fm.sp hred dataAll hsep w).ord_inv] at hpos
  exact neg_pos.mp hpos

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_d0_j (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (a : A)
    (hord : 0 < w.ord (jBar N - algebraMap (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
      (a : AlgebraicClosure ℚ))) :
    0 < (fm.sp hred dataAll hsep w).ord
      (jLine k N - algebraMap k (modularFunctionFieldC k N) (red a)) := by
  by_cases h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A
  · have hmem : (⟨jBar N, fm.jBar_mem⟩ - ⟨constantsHom N A a, fm.constFin_mem a⟩ :
        fm.BFin) ∈ fm.centreFin w h := by
      show _ ∈ (w.centre A).comap (Subring.inclusion (fm.bfin_le_compSubring w h))
      rw [Ideal.mem_comap]
      exact w.mem_centre_of_ord_pos hord
    have hnu := (fm.sp_spec_fin hred dataAll hsep w h _).mpr hmem
    rw [map_sub, fm.piFin_j, fm.piFin_const a] at hnu
    exact ((fm.sp hred dataAll hsep w).mem_nonunits_iff_ord_pos
      (sub_ne_zero.mpr (jLine_ne_const k N (red a)))).mp hnu
  · exfalso
    apply h
    have hval : w.HasValueAt (jBar N) (a : AlgebraicClosure ℚ) := by
      rw [hasValueAt_iff]
      exact (w.mem_nonunits_iff_ord_pos
        (sub_ne_zero.mpr (jBar_ne_const N (a : AlgebraicClosure ℚ)))).mpr hord
    exact w.mem_compSubring_of_hasValueAt a.2 hval

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_d0_j_pole (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hpole : ∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
      (a : AlgebraicClosure ℚ)) ≤ 0) :
    (fm.sp hred dataAll hsep w).ord (jLine k N) < 0 := by
  by_cases h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A
  · exfalso
    have ha₀ := w.ord_sub_value_pos (f := ⟨jBar N, h⟩)
      (jBar_ne_const N (w.value A ⟨jBar N, h⟩ : AlgebraicClosure ℚ))
    exact absurd ha₀ (not_lt.mpr (hpole (w.value A ⟨jBar N, h⟩)))
  · exact fm.sp_ord_jLine_neg hred dataAll hsep w h

private theorem jNBar_ne_const (N : ℕ) [NeZero N] (data : ModularPolynomialData N)
    (hsym : EvalSymm data.Φ) (c : AlgebraicClosure ℚ) :
    jNBar N ≠ algebraMap (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) c :=
  fun h => transcendental_jNBar N data hsym (h ▸ isAlgebraic_algebraMap c)

private theorem jNLine_ne_const (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) (c : k) :
    jNLine k N ≠ algebraMap k (modularFunctionFieldC k N) c := by
  intro h
  have htr : Transcendental k (jNLine k N) := transcendental_jNC k N data hsym
  exact htr (h ▸ isAlgebraic_algebraMap c)

private theorem jNLine_ne_zero (k : Type*) [Field k] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) :
    (jNLine k N : modularFunctionFieldC k N) ≠ 0 := by
  intro h
  have htr : Transcendental k (jNLine k N) := transcendental_jNC k N data hsym
  exact htr (h ▸ isAlgebraic_zero)

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem aeval_mem_subring {F' : Type*} [Field F'] (S : Subring F') {x : F'} (hx : x ∈ S)
    (p : Polynomial ℤ) : Polynomial.aeval (R := ℤ) x p ∈ S := by
  have hcomp : (S.subtype).comp
      (Polynomial.aeval (R := ℤ) (⟨x, hx⟩ : S)).toRingHom
      = (Polynomial.aeval (R := ℤ) x).toRingHom := by
    apply Polynomial.ringHom_ext
    · intro a
      simp only [eq_intCast, map_intCast]
    · rw [RingHom.comp_apply]
      rw [show (Polynomial.aeval (R := ℤ) (⟨x, hx⟩ : S)).toRingHom Polynomial.X
          = (⟨x, hx⟩ : S) from Polynomial.aeval_X _]
      rw [show (Polynomial.aeval (R := ℤ) x).toRingHom Polynomial.X = x
          from Polynomial.aeval_X _]
      rfl
  have h := congrArg (fun φ : Polynomial ℤ →+* F' => φ p) hcomp
  simp only [RingHom.coe_comp, Function.comp_apply] at h
  rw [show Polynomial.aeval (R := ℤ) x p
      = (Polynomial.aeval (R := ℤ) x).toRingHom p from rfl, ← h]
  exact SetLike.coe_mem _

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem ord_nonneg_of_mem' {k' F' : Type*} [Field k'] [Field F'] [Algebra k' F']
    (v : Place k' F') {x : F'} (hx : x ≠ 0) (h : x ∈ v.toValuationSubring) :
    0 ≤ v.ord x := by
  by_contra hneg
  have hpos : 0 < v.ord x⁻¹ := by
    rw [v.ord_inv]
    exact neg_pos.mpr (not_le.mp hneg)
  have hnu : x⁻¹ ∈ v.toValuationSubring.nonunits :=
    (v.mem_nonunits_iff_ord_pos (inv_ne_zero hx)).mpr hpos
  rcases (ValuationSubring.mem_nonunits_iff_or _).mp hnu with h0 | hninv
  · exact inv_ne_zero hx h0
  · rw [inv_inv] at hninv
    exact hninv h

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_d0_jN (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsym : EvalSymm (dataAll N (dvd_refl N)).Φ)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (a : A)
    (hord : 0 < w.ord (jNBar N - algebraMap (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
      (a : AlgebraicClosure ℚ))) :
    0 < (fm.sp hred dataAll hsep w).ord
      (jNLine k N - algebraMap k (modularFunctionFieldC k N) (red a)) := by
  by_cases h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A
  · have hmem : (⟨jNBar N, fm.jNBar_mem⟩ - ⟨constantsHom N A a, fm.constFin_mem a⟩ :
        fm.BFin) ∈ fm.centreFin w h := by
      show _ ∈ (w.centre A).comap (Subring.inclusion (fm.bfin_le_compSubring w h))
      rw [Ideal.mem_comap]
      exact w.mem_centre_of_ord_pos hord
    have hnu := (fm.sp_spec_fin hred dataAll hsep w h _).mpr hmem
    rw [map_sub, fm.piFin_jN, fm.piFin_const a] at hnu
    exact ((fm.sp hred dataAll hsep w).mem_nonunits_iff_ord_pos
      (sub_ne_zero.mpr (jNLine_ne_const k N (dataAll N (dvd_refl N)) hsym (red a)))).mp hnu
  · exfalso
    apply h
    have hvN : (jNBar N : laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) ∈ w.compSubring A := by
      refine w.mem_compSubring_of_hasValueAt a.2 ?_
      rw [hasValueAt_iff]
      exact (w.mem_nonunits_iff_ord_pos (sub_ne_zero.mpr
        (jNBar_ne_const N (dataAll N (dvd_refl N)) hsym
          (a : AlgebraicClosure ℚ)))).mpr hord
    have hS : Subring.closure
        (Set.range ((algebraMap (AlgebraicClosure ℚ)
          (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))).comp
            A.subtype) ∪ {jNBar N}) ≤ w.compSubring A := by
      refine Subring.closure_le.mpr ?_
      rintro x (⟨a', rfl⟩ | rfl)
      · exact (w.algebraMap_mem_compSubring_iff A _).mpr a'.2
      · exact hvN
    refine w.mem_compSubring_of_isIntegral' A hS ?_
    refine ⟨(dataAll N (dvd_refl N)).Φ.map
      ((Polynomial.aeval (R := ℤ)
        (⟨jNBar N, Subring.subset_closure (Set.mem_union_right _ rfl)⟩ :
          Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ)
            (laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N}))).toRingHom),
      (dataAll N (dvd_refl N)).monic.map _, ?_⟩
    rw [Polynomial.eval₂_map]
    have hcomp : ((algebraMap
        (Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ)
          (laurentBaseChange (AlgebraicClosure ℚ)
            (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N}))
        (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))).comp
        ((Polynomial.aeval (R := ℤ)
          (⟨jNBar N, Subring.subset_closure (Set.mem_union_right _ rfl)⟩ :
            Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ)
              (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N}))).toRingHom))
        = (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom := by
      apply Polynomial.ringHom_ext
      · intro b
        simp only [eq_intCast, map_intCast]
      · rw [RingHom.comp_apply]
        rw [show (Polynomial.aeval (R := ℤ)
            (⟨jNBar N, Subring.subset_closure (Set.mem_union_right _ rfl)⟩ :
              Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ)
                (laurentBaseChange (AlgebraicClosure ℚ)
                  (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N}))).toRingHom
            Polynomial.X
            = (⟨jNBar N, Subring.subset_closure (Set.mem_union_right _ rfl)⟩ :
              Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ)
                (laurentBaseChange (AlgebraicClosure ℚ)
                  (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N}))
          from Polynomial.aeval_X _]
        rw [show (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom Polynomial.X = jNBar N
          from Polynomial.aeval_X _]
        rfl
    rw [hcomp]
    exact barEvalSwap_subtype N (dataAll N (dvd_refl N)) hsym

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_d0_jN_pole (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsym : EvalSymm (dataAll N (dvd_refl N)).Φ)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hpole : ∀ a : A, w.ord (jNBar N - algebraMap (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
      (a : AlgebraicClosure ℚ)) ≤ 0) :
    (fm.sp hred dataAll hsep w).ord (jNLine k N) < 0 := by
  by_cases h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A
  · exfalso
    have hvN : (jNBar N : laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) ∈ w.compSubring A :=
      fm.bfin_le_compSubring w h fm.jNBar_mem
    have ha₀ := w.ord_sub_value_pos (f := ⟨jNBar N, hvN⟩)
      (jNBar_ne_const N (dataAll N (dvd_refl N)) hsym
        (w.value A ⟨jNBar N, hvN⟩ : AlgebraicClosure ℚ))
    exact absurd ha₀ (not_lt.mpr (hpole (w.value A ⟨jNBar N, hvN⟩)))
  · have hjneg := fm.sp_ord_jLine_neg hred dataAll hsep w h
    by_contra hge
    have hmemN : (jNLine k N : modularFunctionFieldC k N) ∈
        (fm.sp hred dataAll hsep w).toValuationSubring :=
      mem_of_ord_nonneg _ (jNLine_ne_zero k N (dataAll N (dvd_refl N)) hsym)
        (not_lt.mp hge)
    have hmemJ : (jLine k N : modularFunctionFieldC k N) ∈
        (fm.sp hred dataAll hsep w).toValuationSubring := by
      refine (fm.sp hred dataAll hsep w).mem_of_eval_monic_eq_zero
        (P := (dataAll N (dvd_refl N)).Φ.map
          ((Polynomial.aeval (R := ℤ) (jNLine k N)).toRingHom))
        ((dataAll N (dvd_refl N)).monic.map _) (fun i => ?_) ?_
      · rw [Polynomial.coeff_map]
        exact aeval_mem_subring
          (fm.sp hred dataAll hsep w).toValuationSubring.toSubring hmemN _
      · rw [Polynomial.eval_map]
        exact fibreEvalSwap_subtype k N (dataAll N (dvd_refl N)) hsym
    exact absurd (ord_nonneg_of_mem' _ (jLine_ne_zero k N) hmemJ) (not_le.mpr hjneg)

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.piFin_mem_valuationSubring (fm : FibreModel N A ℓ k red)
    (v' : Place k (modularFunctionFieldC k N))
    (hjO : (jLine k N : modularFunctionFieldC k N) ∈ v'.toValuationSubring)
    (b : fm.BFin) :
    (fm.piFin b : modularFunctionFieldC k N) ∈ v'.toValuationSubring := by
  obtain ⟨p, hp, hpe⟩ := fm.integralFin b
  have hABle : affineBaseFin N A ≤ fm.BFin := by
    refine Subring.closure_le.mpr ?_
    rintro x (⟨a, rfl⟩ | rfl)
    · exact fm.constFin_mem a
    · exact fm.jBar_mem
  have hψO : ∀ (x : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
      (hx : x ∈ affineBaseFin N A),
      fm.piFin ⟨x, hABle hx⟩ ∈ v'.toValuationSubring := by
    intro x hx
    induction hx using Subring.closure_induction with
    | mem y hy =>
      rcases hy with ⟨a, rfl⟩ | rfl
      · rw [show ∀ h : constantsHom N A a ∈ fm.BFin,
            fm.piFin ⟨constantsHom N A a, h⟩
              = algebraMap k (modularFunctionFieldC k N) (red a)
          from fun _ => fm.piFin_const a]
        exact v'.algebraMap_mem' (red a)
      · rw [show ∀ h : jBar N ∈ fm.BFin, fm.piFin ⟨jBar N, h⟩ = jLine k N
          from fun _ => fm.piFin_j]
        exact hjO
    | one =>
      have h1 : fm.piFin ⟨1, hABle (one_mem _)⟩ = 1 := by
        rw [show (⟨1, hABle (one_mem _)⟩ : fm.BFin) = 1 from Subtype.ext rfl, map_one]
      exact h1 ▸ one_mem _
    | zero =>
      have h0 : fm.piFin ⟨0, hABle (zero_mem _)⟩ = 0 := by
        rw [show (⟨0, hABle (zero_mem _)⟩ : fm.BFin) = 0 from Subtype.ext rfl, map_zero]
      exact h0 ▸ zero_mem _
    | add y z hy hz ihy ihz =>
      have ha : fm.piFin ⟨y + z, hABle (add_mem hy hz)⟩
          = fm.piFin ⟨y, hABle hy⟩ + fm.piFin ⟨z, hABle hz⟩ := by
        rw [show (⟨y + z, hABle (add_mem hy hz)⟩ : fm.BFin)
            = ⟨y, hABle hy⟩ + ⟨z, hABle hz⟩ from Subtype.ext rfl, map_add]
      exact ha ▸ add_mem ihy ihz
    | neg y hy ihy =>
      have hn : fm.piFin ⟨-y, hABle (neg_mem hy)⟩ = -fm.piFin ⟨y, hABle hy⟩ := by
        rw [show (⟨-y, hABle (neg_mem hy)⟩ : fm.BFin)
            = -(⟨y, hABle hy⟩ : fm.BFin) from Subtype.ext rfl, map_neg]
      exact hn ▸ neg_mem ihy
    | mul y z hy hz ihy ihz =>
      have hm : fm.piFin ⟨y * z, hABle (mul_mem hy hz)⟩
          = fm.piFin ⟨y, hABle hy⟩ * fm.piFin ⟨z, hABle hz⟩ := by
        rw [show (⟨y * z, hABle (mul_mem hy hz)⟩ : fm.BFin)
            = ⟨y, hABle hy⟩ * ⟨z, hABle hz⟩ from Subtype.ext rfl, map_mul]
      exact hm ▸ mul_mem ihy ihz
  have hq : Polynomial.eval₂ (Subring.inclusion hABle) b p = 0 := by
    apply Subtype.val_injective
    have h := Polynomial.hom_eval₂ p (Subring.inclusion hABle) fm.BFin.subtype b
    have hcomp : (fm.BFin.subtype).comp (Subring.inclusion hABle)
        = (affineBaseFin N A).subtype := by
      apply RingHom.ext
      intro x
      rfl
    rw [hcomp] at h
    calc (↑(Polynomial.eval₂ (Subring.inclusion hABle) b p) :
            laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
        = fm.BFin.subtype (Polynomial.eval₂ (Subring.inclusion hABle) b p) := rfl
      _ = Polynomial.eval₂ ((affineBaseFin N A).subtype) (fm.BFin.subtype b) p := h
      _ = 0 := hpe
  refine v'.mem_of_eval_monic_eq_zero
    (P := p.map (fm.piFin.comp (Subring.inclusion hABle))) (hp.map _) (fun i => ?_) ?_
  · rw [Polynomial.coeff_map]
    exact hψO _ (p.coeff i).2
  · rw [Polynomial.eval_map]
    have h := Polynomial.hom_eval₂ p (Subring.inclusion hABle) fm.piFin b
    rw [← h, hq, map_zero]

set_option maxHeartbeats 3200000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.exists_sp_eq_fin (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (v' : Place k (modularFunctionFieldC k N))
    (hjO : (jLine k N : modularFunctionFieldC k N) ∈ v'.toValuationSubring) :
    ∃ w, fm.sp hred dataAll hsep w = v' := by
  haveI : IsAlgClosed k := A.isAlgClosed_of_surjective red hred
  haveI hFD : FiniteDimensional
      (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))
      (modularFunctionFieldC k N) := finiteDimensional_adjoin_jC k N (dataAll N (dvd_refl N))
  haveI h1 : Module.Finite
      ((v'.restrict (IntermediateField.adjoin k
        ({jLine k N} : Set (modularFunctionFieldC k N)))).ResidueField)
      v'.ResidueField :=
    rf_finite_residueField v'
  haveI h2 : Module.Finite k
      ((v'.restrict (IntermediateField.adjoin k
        ({jLine k N} : Set (modularFunctionFieldC k N)))).ResidueField) := by
    have htop : IntermediateField.adjoin k
        ({⟨jLine k N, IntermediateField.mem_adjoin_simple_self _ (jLine k N)⟩} :
          Set (IntermediateField.adjoin k
            ({jLine k N} : Set (modularFunctionFieldC k N)))) = ⊤ := by
      have h := adjoin_val_preimage_eq_top (K := k)
        (F := IntermediateField.adjoin k
          ({jLine k N} : Set (modularFunctionFieldC k N)))
        (S := {jLine k N}) rfl
      have hset : (Subtype.val ⁻¹' {jLine k N} :
          Set (IntermediateField.adjoin k
            ({jLine k N} : Set (modularFunctionFieldC k N))))
          = {⟨jLine k N, IntermediateField.mem_adjoin_simple_self _ (jLine k N)⟩} := by
        ext z
        simp only [Set.mem_preimage, Set.mem_singleton_iff]
        exact ⟨fun hz => Subtype.ext hz, fun hz => by rw [hz]⟩
      rwa [hset] at h
    exact AlgebraicCurve.Place.finite_residueField_of_adjoin_simple_eq_top
      (transcendental_subtype _ (IntermediateField.mem_adjoin_simple_self _ (jLine k N))
        (transcendental_jLine k N)) htop _
  haveI h3 : Module.Finite k v'.ResidueField :=
    Module.Finite.trans
      ((v'.restrict (IntermediateField.adjoin k
        ({jLine k N} : Set (modularFunctionFieldC k N)))).ResidueField)
      v'.ResidueField
  have hsurj : Function.Surjective (algebraMap k v'.ResidueField) :=
    v'.surjective_algebraMap_residueField_of_isAlgClosed
  let φ : fm.BFin →+* v'.toValuationSubring :=
    fm.piFin.codRestrict v'.toValuationSubring (fm.piFin_mem_valuationSubring v' hjO)
  let ρ := (IsLocalRing.residue (v'.toValuationSubring : Type _)).comp φ
  haveI : (RingHom.ker ρ).IsPrime := RingHom.ker_isPrime ρ
  have h𝔮A : ∀ a : A, (⟨constantsHom N A a, fm.constFin_mem a⟩ : fm.BFin) ∈ RingHom.ker ρ
      ↔ a ∈ IsLocalRing.maximalIdeal A := by
    intro a
    rw [RingHom.mem_ker]
    have hφc : φ ⟨constantsHom N A a, fm.constFin_mem a⟩
        = ⟨algebraMap k (modularFunctionFieldC k N) (red a),
           v'.algebraMap_mem' (red a)⟩ := by
      apply Subtype.ext
      exact fm.piFin_const a
    rw [show ρ ⟨constantsHom N A a, fm.constFin_mem a⟩
        = IsLocalRing.residue _ (φ ⟨constantsHom N A a, fm.constFin_mem a⟩) from rfl,
      hφc, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff]
    constructor
    · intro h
      have h0 : v'.HasValueAt (algebraMap k (modularFunctionFieldC k N) (red a)) 0 := by
        rw [hasValueAt_zero_iff]
        exact h
      have hza : red a = 0 := ((v'.hasValueAt_algebraMap (red a)).unique h0)
      exact (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _
        (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ)
        ℓ _ _ red a).mp hza
    · intro ha
      have hza : red a = 0 := (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _
        (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ)
        ℓ _ _ red a).mpr ha
      show algebraMap k (modularFunctionFieldC k N) (red a) ∈
        v'.toValuationSubring.nonunits
      rw [hza, map_zero]
      exact (ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inl rfl)
  obtain ⟨c, hc⟩ := v'.exists_hasValueAt hsurj hjO
  obtain ⟨a₀, rfl⟩ := hred c
  have hja : (⟨jBar N, fm.jBar_mem⟩ : fm.BFin)
      - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩ ∈ RingHom.ker ρ := by
    rw [RingHom.mem_ker]
    rw [show ρ (⟨jBar N, fm.jBar_mem⟩ - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩)
        = IsLocalRing.residue _
            (φ (⟨jBar N, fm.jBar_mem⟩ - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩))
      from rfl, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff]
    have hval : ((φ (⟨jBar N, fm.jBar_mem⟩
        - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩) : v'.toValuationSubring) :
          modularFunctionFieldC k N)
        = jLine k N - algebraMap k (modularFunctionFieldC k N) (red a₀) := by
      show (fm.piFin (⟨jBar N, fm.jBar_mem⟩
        - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩) : modularFunctionFieldC k N) = _
      rw [map_sub, fm.piFin_j, fm.piFin_const a₀]
      rfl
    rw [hval]
    exact hc
  haveI hFDbar : FiniteDimensional
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) :=
    finiteDimensional_lineBar_of_dataAll N dataAll
  haveI hCZ : CharZero (IntermediateField.adjoin (AlgebraicClosure ℚ)
      ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)))) :=
    charZero_of_injective_algebraMap
      (algebraMap (AlgebraicClosure ℚ) _).injective
  haveI hSepBar : Algebra.IsSeparable
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) :=
    inferInstance
  obtain ⟨w, hB, hcent, hval⟩ := AlgebraicCurve.Place.exists_place_centre_comap_eq A
    (transcendental_jBar N) fm.constFin_mem fm.jBar_mem fm.integralFin
    (RingHom.ker ρ) h𝔮A a₀ hja
  refine ⟨w, ?_⟩
  have hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A :=
    w.mem_compSubring_of_hasValueAt a₀.2 hval
  have hspec := fm.sp_spec_fin hred dataAll hsep w hwFin
  have hcent' : fm.centreFin w hwFin = RingHom.ker ρ := hcent
  have hjOu : (jLine k N : modularFunctionFieldC k N) ∈
      (fm.sp hred dataAll hsep w).toValuationSubring := by
    have h1 : (⟨jBar N, fm.jBar_mem⟩ : fm.BFin)
        - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩ ∈ fm.centreFin w hwFin := by
      rw [hcent']
      exact hja
    have h2 := (hspec _).mpr h1
    rw [map_sub, fm.piFin_j, fm.piFin_const a₀] at h2
    have h3 := (fm.sp hred dataAll hsep w).toValuationSubring.nonunits_subset h2
    have h4 := add_mem h3
      ((fm.sp hred dataAll hsep w).algebraMap_mem' (red a₀))
    simpa [jLine] using h4
  have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piFin.range := by
    intro c
    obtain ⟨a, rfl⟩ := hred c
    exact ⟨⟨constantsHom N A a, fm.constFin_mem a⟩, (fm.piFin_const a).symm ▸ rfl⟩
  haveI hSepLine : Algebra.IsSeparable
      (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))
      (modularFunctionFieldC k N) :=
    isSeparable_line_fibre k N (dataAll N (dvd_refl N)) hsep
  haveI hDed : IsDedekindDomain (lineClosure k N) :=
    isDedekindDomain_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLine k N)
  haveI hFrac : IsFractionRing (lineClosure k N) (modularFunctionFieldC k N) :=
    isFractionRing_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLine k N)
  refine AlgebraicCurve.Place.eq_of_forall_mem_nonunits_iff_of_surjective
    (lineClosure k N)
    (fun r => integralClosure_adjoin_le_valuationSubring _
      (fun c => (fm.sp hred dataAll hsep w).algebraMap_mem' c) hjOu r)
    (fun r => integralClosure_adjoin_le_valuationSubring _
      (fun c => v'.algebraMap_mem' c) hjO r)
    (fun b : fm.BFin => (fm.piFin b : modularFunctionFieldC k N))
    (AlgebraicCurve.Place.exists_eq_of_integralClosure_adjoin
      (fun b : fm.BFin => (fm.piFin b : modularFunctionFieldC k N))
      (fun x => RingHom.mem_range) hconstR
      ⟨⟨jBar N, fm.jBar_mem⟩, fm.piFin_j⟩ fm.intClosed_piFin)
    (fun b => ?_)
  rw [hspec b, hcent', RingHom.mem_ker,
    show ρ b = IsLocalRing.residue _ (φ b) from rfl,
    IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff]
  rfl

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.piInf_mem_valuationSubring (fm : FibreModel N A ℓ k red)
    (v' : Place k (modularFunctionFieldC k N))
    (hjO : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ v'.toValuationSubring)
    (b : fm.BInf) :
    (fm.piInf b : modularFunctionFieldC k N) ∈ v'.toValuationSubring := by
  obtain ⟨p, hp, hpe⟩ := fm.integralInf b
  have hABle : affineBaseInf N A ≤ fm.BInf := by
    refine Subring.closure_le.mpr ?_
    rintro x (⟨a, rfl⟩ | rfl)
    · exact fm.constInf_mem a
    · exact fm.jInvBar_mem
  have hψO : ∀ (x : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
      (hx : x ∈ affineBaseInf N A),
      fm.piInf ⟨x, hABle hx⟩ ∈ v'.toValuationSubring := by
    intro x hx
    induction hx using Subring.closure_induction with
    | mem y hy =>
      rcases hy with ⟨a, rfl⟩ | rfl
      · rw [show ∀ h : constantsHom N A a ∈ fm.BInf,
            fm.piInf ⟨constantsHom N A a, h⟩
              = algebraMap k (modularFunctionFieldC k N) (red a)
          from fun _ => fm.piInf_const a]
        exact v'.algebraMap_mem' (red a)
      · rw [show ∀ h : (jBar N)⁻¹ ∈ fm.BInf, fm.piInf ⟨(jBar N)⁻¹, h⟩ = (jLine k N)⁻¹
          from fun _ => fm.piInf_jInv]
        exact hjO
    | one =>
      have h1 : fm.piInf ⟨1, hABle (one_mem _)⟩ = 1 := by
        rw [show (⟨1, hABle (one_mem _)⟩ : fm.BInf) = 1 from Subtype.ext rfl, map_one]
      exact h1 ▸ one_mem _
    | zero =>
      have h0 : fm.piInf ⟨0, hABle (zero_mem _)⟩ = 0 := by
        rw [show (⟨0, hABle (zero_mem _)⟩ : fm.BInf) = 0 from Subtype.ext rfl, map_zero]
      exact h0 ▸ zero_mem _
    | add y z hy hz ihy ihz =>
      have ha : fm.piInf ⟨y + z, hABle (add_mem hy hz)⟩
          = fm.piInf ⟨y, hABle hy⟩ + fm.piInf ⟨z, hABle hz⟩ := by
        rw [show (⟨y + z, hABle (add_mem hy hz)⟩ : fm.BInf)
            = ⟨y, hABle hy⟩ + ⟨z, hABle hz⟩ from Subtype.ext rfl, map_add]
      exact ha ▸ add_mem ihy ihz
    | neg y hy ihy =>
      have hn : fm.piInf ⟨-y, hABle (neg_mem hy)⟩ = -fm.piInf ⟨y, hABle hy⟩ := by
        rw [show (⟨-y, hABle (neg_mem hy)⟩ : fm.BInf)
            = -(⟨y, hABle hy⟩ : fm.BInf) from Subtype.ext rfl, map_neg]
      exact hn ▸ neg_mem ihy
    | mul y z hy hz ihy ihz =>
      have hm : fm.piInf ⟨y * z, hABle (mul_mem hy hz)⟩
          = fm.piInf ⟨y, hABle hy⟩ * fm.piInf ⟨z, hABle hz⟩ := by
        rw [show (⟨y * z, hABle (mul_mem hy hz)⟩ : fm.BInf)
            = ⟨y, hABle hy⟩ * ⟨z, hABle hz⟩ from Subtype.ext rfl, map_mul]
      exact hm ▸ mul_mem ihy ihz
  have hq : Polynomial.eval₂ (Subring.inclusion hABle) b p = 0 := by
    apply Subtype.val_injective
    have h := Polynomial.hom_eval₂ p (Subring.inclusion hABle) fm.BInf.subtype b
    have hcomp : (fm.BInf.subtype).comp (Subring.inclusion hABle)
        = (affineBaseInf N A).subtype := by
      apply RingHom.ext
      intro x
      rfl
    rw [hcomp] at h
    calc (↑(Polynomial.eval₂ (Subring.inclusion hABle) b p) :
            laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
        = fm.BInf.subtype (Polynomial.eval₂ (Subring.inclusion hABle) b p) := rfl
      _ = Polynomial.eval₂ ((affineBaseInf N A).subtype) (fm.BInf.subtype b) p := h
      _ = 0 := hpe
  refine v'.mem_of_eval_monic_eq_zero
    (P := p.map (fm.piInf.comp (Subring.inclusion hABle))) (hp.map _) (fun i => ?_) ?_
  · rw [Polynomial.coeff_map]
    exact hψO _ (p.coeff i).2
  · rw [Polynomial.eval_map]
    have h := Polynomial.hom_eval₂ p (Subring.inclusion hABle) fm.piInf b
    rw [← h, hq, map_zero]

set_option maxHeartbeats 3200000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.exists_sp_eq_inf (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (v' : Place k (modularFunctionFieldC k N))
    (hjinvO : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ v'.toValuationSubring)
    (hjO : ¬ (jLine k N : modularFunctionFieldC k N) ∈ v'.toValuationSubring) :
    ∃ w, fm.sp hred dataAll hsep w = v' := by
  let φ : fm.BInf →+* v'.toValuationSubring :=
    fm.piInf.codRestrict v'.toValuationSubring (fm.piInf_mem_valuationSubring v' hjinvO)
  let ρ := (IsLocalRing.residue (v'.toValuationSubring : Type _)).comp φ
  haveI : (RingHom.ker ρ).IsPrime := RingHom.ker_isPrime ρ
  have h𝔮A : ∀ a : A, (⟨constantsHom N A a, fm.constInf_mem a⟩ : fm.BInf) ∈ RingHom.ker ρ
      ↔ a ∈ IsLocalRing.maximalIdeal A := by
    intro a
    rw [RingHom.mem_ker]
    have hφc : φ ⟨constantsHom N A a, fm.constInf_mem a⟩
        = ⟨algebraMap k (modularFunctionFieldC k N) (red a),
           v'.algebraMap_mem' (red a)⟩ := by
      apply Subtype.ext
      exact fm.piInf_const a
    rw [show ρ ⟨constantsHom N A a, fm.constInf_mem a⟩
        = IsLocalRing.residue _ (φ ⟨constantsHom N A a, fm.constInf_mem a⟩) from rfl,
      hφc, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff]
    constructor
    · intro h
      have h0 : v'.HasValueAt (algebraMap k (modularFunctionFieldC k N) (red a)) 0 := by
        rw [hasValueAt_zero_iff]
        exact h
      have hza : red a = 0 := ((v'.hasValueAt_algebraMap (red a)).unique h0)
      exact (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _
        (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ)
        ℓ _ _ red a).mp hza
    · intro ha
      have hza : red a = 0 := (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _
        (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ)
        ℓ _ _ red a).mpr ha
      show algebraMap k (modularFunctionFieldC k N) (red a) ∈
        v'.toValuationSubring.nonunits
      rw [hza, map_zero]
      exact (ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inl rfl)
  have hjnu : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈
      v'.toValuationSubring.nonunits := by
    refine (ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inr ?_)
    rwa [inv_inv]
  have hja : (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf)
      - ⟨constantsHom N A 0, fm.constInf_mem 0⟩ ∈ RingHom.ker ρ := by
    rw [RingHom.mem_ker]
    rw [show ρ (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ - ⟨constantsHom N A 0, fm.constInf_mem 0⟩)
        = IsLocalRing.residue _
            (φ (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ - ⟨constantsHom N A 0, fm.constInf_mem 0⟩))
      from rfl, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff]
    have hval : ((φ (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩
        - ⟨constantsHom N A 0, fm.constInf_mem 0⟩) : v'.toValuationSubring) :
          modularFunctionFieldC k N)
        = ((jLine k N)⁻¹ : modularFunctionFieldC k N) := by
      show (fm.piInf (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩
        - ⟨constantsHom N A 0, fm.constInf_mem 0⟩) : modularFunctionFieldC k N) = _
      rw [map_sub, fm.piInf_jInv, fm.piInf_const 0, map_zero, map_zero, sub_zero]
      rfl
    rw [hval]
    exact hjnu
  have htrinv : Transcendental (AlgebraicClosure ℚ)
      ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) := by
    intro halg
    exact transcendental_jBar N (inv_inv (jBar N) ▸ halg.inv)
  haveI hFDbar : FiniteDimensional
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({(jBar N)⁻¹} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := by
    rw [IntermediateField.adjoin_simple_inv_eq (jBar N)]
    exact finiteDimensional_lineBar_of_dataAll N dataAll
  haveI hCZ : CharZero (IntermediateField.adjoin (AlgebraicClosure ℚ)
      ({(jBar N)⁻¹} : Set (laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)))) :=
    charZero_of_injective_algebraMap
      (algebraMap (AlgebraicClosure ℚ) _).injective
  haveI hSepBar : Algebra.IsSeparable
      (IntermediateField.adjoin (AlgebraicClosure ℚ)
        ({(jBar N)⁻¹} : Set (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N))))
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) :=
    inferInstance
  obtain ⟨w, hB, hcent, hval⟩ := AlgebraicCurve.Place.exists_place_centre_comap_eq A
    htrinv fm.constInf_mem fm.jInvBar_mem fm.integralInf
    (RingHom.ker ρ) h𝔮A 0 (by simpa using hja)
  refine ⟨w, ?_⟩
  have hval0 : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.toValuationSubring.nonunits := by
    have h := hval
    rw [HasValueAt] at h
    rwa [show ((0 : A) : AlgebraicClosure ℚ) = 0 from rfl, map_zero, sub_zero] at h
  have hwInf : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A := by
    intro hmem
    obtain ⟨c, hc⟩ := (w.mem_compSubring_iff (A := A)).mp hmem
    have hjne : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) ≠ 0 :=
      fun h => transcendental_jBar N (h ▸ isAlgebraic_zero)
    have hjmem : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) ∈ w.toValuationSubring := by
      have h1 := w.toValuationSubring.nonunits_subset hc
      have h2 := add_mem h1 (w.algebraMap_mem' (c : AlgebraicClosure ℚ))
      simpa using h2
    have h𝔪 : (⟨(jBar N)⁻¹, w.toValuationSubring.nonunits_subset hval0⟩ :
        w.toValuationSubring) ∈ IsLocalRing.maximalIdeal _ := by
      rw [← ValuationSubring.coe_mem_nonunits_iff]
      exact hval0
    have hone : (⟨jBar N, hjmem⟩ : w.toValuationSubring) *
        ⟨(jBar N)⁻¹, w.toValuationSubring.nonunits_subset hval0⟩
        = 1 := by
      apply Subtype.ext
      show (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) * (jBar N)⁻¹ = 1
      exact mul_inv_cancel₀ hjne
    have htop : (1 : w.toValuationSubring) ∈ IsLocalRing.maximalIdeal _ := by
      rw [← hone]
      exact Ideal.mul_mem_left _ _ h𝔪
    exact (IsLocalRing.maximalIdeal.isMaximal _).ne_top (Ideal.eq_top_of_isUnit_mem _ htop
        isUnit_one)
  have hspec := fm.sp_spec_inf hred dataAll hsep w hwInf
  have hcent' : fm.centreInf w ((fm.chart_dichotomy dataAll w).resolve_left hwInf)
      = RingHom.ker ρ := hcent
  have hjinvOu : (((jLine k N)⁻¹ : modularFunctionFieldC k N)) ∈
      (fm.sp hred dataAll hsep w).toValuationSubring := by
    have h1 : (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf)
        - ⟨constantsHom N A 0, fm.constInf_mem 0⟩ ∈
          fm.centreInf w ((fm.chart_dichotomy dataAll w).resolve_left hwInf) := by
      rw [hcent']
      exact hja
    have h2 := (hspec _).mpr h1
    rw [map_sub, fm.piInf_jInv, fm.piInf_const 0, map_zero, map_zero, sub_zero] at h2
    exact (fm.sp hred dataAll hsep w).toValuationSubring.nonunits_subset h2
  have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piInf.range := by
    intro c
    obtain ⟨a, rfl⟩ := hred c
    exact ⟨⟨constantsHom N A a, fm.constInf_mem a⟩, (fm.piInf_const a).symm ▸ rfl⟩
  haveI hSepLine : Algebra.IsSeparable
      (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N))))
      (modularFunctionFieldC k N) := by
    rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)]
    exact isSeparable_line_fibre k N (dataAll N (dvd_refl N)) hsep
  haveI hFDLine : FiniteDimensional
      (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N))))
      (modularFunctionFieldC k N) := by
    rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)]
    exact finiteDimensional_adjoin_jC k N (dataAll N (dvd_refl N))
  haveI hDed : IsDedekindDomain (lineClosureInf k N) :=
    isDedekindDomain_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLineInv k N)
  haveI hFrac : IsFractionRing (lineClosureInf k N) (modularFunctionFieldC k N) :=
    isFractionRing_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLineInv k N)
  refine AlgebraicCurve.Place.eq_of_forall_mem_nonunits_iff_of_surjective
    (lineClosureInf k N)
    (fun r => integralClosure_adjoin_le_valuationSubring _
      (fun c => (fm.sp hred dataAll hsep w).algebraMap_mem' c) hjinvOu r)
    (fun r => integralClosure_adjoin_le_valuationSubring _
      (fun c => v'.algebraMap_mem' c) hjinvO r)
    (fun b : fm.BInf => (fm.piInf b : modularFunctionFieldC k N))
    (AlgebraicCurve.Place.exists_eq_of_integralClosure_adjoin
      (fun b : fm.BInf => (fm.piInf b : modularFunctionFieldC k N))
      (fun x => RingHom.mem_range) hconstR
      ⟨⟨(jBar N)⁻¹, fm.jInvBar_mem⟩, fm.piInf_jInv⟩ fm.intClosed_piInf)
    (fun b => ?_)
  rw [hspec b, hcent', RingHom.mem_ker,
    show ρ b = IsLocalRing.residue _ (φ b) from rfl,
    IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff]
  rfl

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_d4 (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable) :
    Function.Surjective (fm.sp hred dataAll hsep) := by
  intro v'
  by_cases hjO : (jLine k N : modularFunctionFieldC k N) ∈ v'.toValuationSubring
  · exact fm.exists_sp_eq_fin hred dataAll hsep v' hjO
  · exact fm.exists_sp_eq_inf hred dataAll hsep v'
      ((v'.toValuationSubring.mem_or_inv_mem _).resolve_left hjO) hjO

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.exists_specializationMap_assembled
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsym : EvalSymm (dataAll N (dvd_refl N)).Φ)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (fm : FibreModel N A ℓ k red) :
    ∃ sp : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) →
        Place k (modularFunctionFieldC k N),
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)), ∀ a : A,
        0 < w.ord (jBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) →
        0 < (sp w).ord ((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) -
            algebraMap k (modularFunctionFieldC k N) (red a))) ∧
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)),
        (∀ a : A,
          w.ord (jBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) →
        (sp w).ord ((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)) < 0) ∧
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)), ∀ a : A,
        0 < w.ord (jNBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) →
        0 < (sp w).ord ((⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) -
            algebraMap k (modularFunctionFieldC k N) (red a))) ∧
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)),
        (∀ a : A,
          w.ord (jNBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) →
        (sp w).ord ((⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)) < 0) ∧
      Function.Surjective sp :=
  ⟨fm.sp hred dataAll hsep,
   fun w a h => fm.sp_d0_j hred dataAll hsep w a h,
   fun w h => fm.sp_d0_j_pole hred dataAll hsep w h,
   fun w a h => fm.sp_d0_jN hred dataAll hsym hsep w a h,
   fun w h => fm.sp_d0_jN_pole hred dataAll hsym hsep w h,
   fm.sp_d4 hred dataAll hsep⟩

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_hasValueAt_inf (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A)
    (b : fm.BInf) (a : A)
    (hb : w.HasValueAt (b : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) :
    (fm.sp hred dataAll hsep w).HasValueAt
      (fm.piInf b : modularFunctionFieldC k N) (red a) := by
  have hinv := (fm.chart_dichotomy dataAll w).resolve_left h
  set b' : fm.BInf := b - ⟨constantsHom N A a, fm.constInf_mem a⟩ with hb'
  have hcentmem : b' ∈ fm.centreInf w hinv := by
    rw [FibreModel.centreInf, Ideal.mem_comap]
    refine (w.mem_centre_iff_of_hasValueAt (a := (0 : A)) ?_).mpr (zero_mem _)
    show w.HasValueAt ((b' : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N))) ((0 : A) : AlgebraicClosure ℚ)
    show (b' : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
        - algebraMap _ _ ((0 : A) : AlgebraicClosure ℚ) ∈ w.toValuationSubring.nonunits
    rw [show (((0 : A) : AlgebraicClosure ℚ)) = 0 from rfl, map_zero, sub_zero]
    show ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
        - constantsHom N A a) ∈ w.toValuationSubring.nonunits
    exact hb
  have h2 := (fm.sp_spec_inf hred dataAll hsep w h b').mpr hcentmem
  rw [hb', map_sub, fm.piInf_const a] at h2
  exact h2

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_piInf_nonunits_iff (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A)
    (b : fm.BInf) :
    (fm.piInf b : modularFunctionFieldC k N) ∈
        (fm.sp hred dataAll hsep w).toValuationSubring.nonunits ↔
      w.value A (Subring.inclusion
          (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b)
        ∈ IsLocalRing.maximalIdeal A := by
  rw [fm.sp_spec_inf hred dataAll hsep w h b]
  rw [FibreModel.centreInf, Ideal.mem_comap]
  exact w.mem_centre_iff _

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_jLineInv_mem (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A) :
    (((jLine k N)⁻¹ : modularFunctionFieldC k N)) ∈
      (fm.sp hred dataAll hsep w).toValuationSubring := by
  have hneg := fm.sp_ord_jLine_neg hred dataAll hsep w h
  refine mem_of_ord_nonneg _ (inv_ne_zero (jLine_ne_zero k N)) ?_
  rw [(fm.sp hred dataAll hsep w).ord_inv]
  exact (neg_pos.mpr hneg).le

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.fibre_place_ext_inf_impl (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (v₁ v₂ : Place k (modularFunctionFieldC k N))
    (h₁ : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ v₁.toValuationSubring)
    (h₂ : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ v₂.toValuationSubring)
    (hagree : ∀ b : fm.BInf,
      ((fm.piInf b : modularFunctionFieldC k N) ∈ v₁.toValuationSubring.nonunits ↔
        (fm.piInf b : modularFunctionFieldC k N) ∈ v₂.toValuationSubring.nonunits)) :
    v₁ = v₂ := by
  have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piInf.range := by
    intro c
    obtain ⟨a, rfl⟩ := hred c
    exact ⟨⟨constantsHom N A a, fm.constInf_mem a⟩, (fm.piInf_const a).symm ▸ rfl⟩
  haveI hSepLine : Algebra.IsSeparable
      (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N))))
      (modularFunctionFieldC k N) := by
    rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)]
    exact isSeparable_line_fibre k N (dataAll N (dvd_refl N)) hsep
  haveI hFDLine : FiniteDimensional
      (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N))))
      (modularFunctionFieldC k N) := by
    rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)]
    exact finiteDimensional_adjoin_jC k N (dataAll N (dvd_refl N))
  haveI hDed : IsDedekindDomain (lineClosureInf k N) :=
    isDedekindDomain_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLineInv k N)
  haveI hFrac : IsFractionRing (lineClosureInf k N) (modularFunctionFieldC k N) :=
    isFractionRing_integralClosure_adjoin (K := k)
      (F := modularFunctionFieldC k N) (transcendental_jLineInv k N)
  exact AlgebraicCurve.Place.eq_of_forall_mem_nonunits_iff_of_surjective
    (lineClosureInf k N)
    (fun r => integralClosure_adjoin_le_valuationSubring _
      (fun c => v₁.algebraMap_mem' c) h₁ r)
    (fun r => integralClosure_adjoin_le_valuationSubring _
      (fun c => v₂.algebraMap_mem' c) h₂ r)
    (fun b : fm.BInf => (fm.piInf b : modularFunctionFieldC k N))
    (AlgebraicCurve.Place.exists_eq_of_integralClosure_adjoin
      (fun b : fm.BInf => (fm.piInf b : modularFunctionFieldC k N))
      (fun x => RingHom.mem_range) hconstR
      ⟨⟨(jBar N)⁻¹, fm.jInvBar_mem⟩, fm.piInf_jInv⟩ fm.intClosed_piInf)
    hagree

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem not_jBar_mem_compSubring_of_forall_ord_le
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hpole : ∀ a : A,
      w.ord (jBar N - algebraMap (AlgebraicClosure ℚ)
        (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
        (a : AlgebraicClosure ℚ)) ≤ 0) :
    ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A := by
  intro hmem
  have ha₀ := w.ord_sub_value_pos (f := ⟨jBar N, hmem⟩)
    (jBar_ne_const N (w.value A ⟨jBar N, hmem⟩ : AlgebraicClosure ℚ))
  exact absurd ha₀ (not_lt.mpr (hpole (w.value A ⟨jBar N, hmem⟩)))

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.exists_specializationMap_dict_impl
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsym : EvalSymm (dataAll N (dvd_refl N)).Φ)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (fm : FibreModel N A ℓ k red) :
    ∃ sp : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) →
        Place k (modularFunctionFieldC k N),
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)), ∀ a : A,
        0 < w.ord (jBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) →
        0 < (sp w).ord ((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) -
            algebraMap k (modularFunctionFieldC k N) (red a))) ∧
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)),
        (∀ a : A,
          w.ord (jBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) →
        (sp w).ord ((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)) < 0) ∧
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)), ∀ a : A,
        0 < w.ord (jNBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) →
        0 < (sp w).ord ((⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) -
            algebraMap k (modularFunctionFieldC k N) (red a))) ∧
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)),
        (∀ a : A,
          w.ord (jNBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) →
        (sp w).ord ((⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)) < 0) ∧
      Function.Surjective sp ∧
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)),
        (∀ a : A,
          w.ord (jBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) →
        ∀ b : fm.BInf, ∀ a : A,
          ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) -
              algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                  (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ))
            ∈ w.toValuationSubring.nonunits →
          ((fm.piInf b : modularFunctionFieldC k N) -
              algebraMap k (modularFunctionFieldC k N) (red a))
            ∈ (sp w).toValuationSubring.nonunits) ∧
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)),
        (∀ a : A,
          w.ord (jBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) →
        (((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N))⁻¹
          ∈ (sp w).toValuationSubring)) ∧
      (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
          (modularFunctionFieldFull N)),
        (∀ a : A,
          w.ord (jBar N -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) →
        ∀ b : fm.BInf,
          ((fm.piInf b : modularFunctionFieldC k N)
              ∈ (sp w).toValuationSubring.nonunits ↔
            ∃ a : A, a ∈ IsLocalRing.maximalIdeal A ∧
              ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) -
                  algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
                      (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ))
                ∈ w.toValuationSubring.nonunits)) :=
  ⟨fm.sp hred dataAll hsep,
   fun w a h => fm.sp_d0_j hred dataAll hsep w a h,
   fun w h => fm.sp_d0_j_pole hred dataAll hsep w h,
   fun w a h => fm.sp_d0_jN hred dataAll hsym hsep w a h,
   fun w h => fm.sp_d0_jN_pole hred dataAll hsym hsep w h,
   fm.sp_d4 hred dataAll hsep,
   fun w hpole b a hb => fm.sp_hasValueAt_inf hred dataAll hsep w
     (not_jBar_mem_compSubring_of_forall_ord_le w hpole) b a hb,
   fun w hpole => fm.sp_jLineInv_mem hred dataAll hsep w
     (not_jBar_mem_compSubring_of_forall_ord_le w hpole),
   fun w hpole b => by
     have h := not_jBar_mem_compSubring_of_forall_ord_le w hpole
     constructor
     · intro hnu
       have hval := (fm.sp_piInf_nonunits_iff hred dataAll hsep w h b).mp hnu
       exact ⟨w.value A (Subring.inclusion
           (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b),
         hval,
         w.hasValueAt_value A (Subring.inclusion
           (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b)⟩
     · rintro ⟨a, ha𝔪, hval⟩
       have ht : ((fm.piInf b : modularFunctionFieldC k N) -
           algebraMap k (modularFunctionFieldC k N) (red a))
           ∈ (fm.sp hred dataAll hsep w).toValuationSubring.nonunits :=
         fm.sp_hasValueAt_inf hred dataAll hsep w h b a hval
       have hred0 : red a = 0 := (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _
         (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ)
         ℓ _ _ red a).mpr ha𝔪
       rwa [hred0, map_zero, sub_zero] at ht⟩

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in
private theorem FibreModel.sp_piInf_nonunits_iff_of_hasValueAt (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A)
    (b : fm.BInf) (a : A)
    (hb : w.HasValueAt (b : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) :
    (fm.piInf b : modularFunctionFieldC k N) ∈
        (fm.sp hred dataAll hsep w).toValuationSubring.nonunits ↔
      a ∈ IsLocalRing.maximalIdeal A := by
  rw [fm.sp_piInf_nonunits_iff hred dataAll hsep w h b,
    w.value_eq_of_hasValueAt (f := Subring.inclusion
      (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b) hb]

noncomputable def FibreModel.spPlace (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable) :
    Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) → Place k (modularFunctionFieldC k N) :=
  fm.sp hred dataAll hsep

noncomputable def FibreModel.spDiv (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable) :
    Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N) →
      Divisor k (modularFunctionFieldC k N) :=
  Finsupp.mapDomain (fm.spPlace hred dataAll hsep)

def FibreModel.SpDivPreservesPrincipal (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable) : Prop :=
  (∀ D ∈ Divisor.degZero (K := AlgebraicClosure ℚ) (F := modularFunctionFieldBar N),
      fm.spDiv hred dataAll hsep D ∈
        Divisor.degZero (K := k) (F := modularFunctionFieldC k N)) ∧
  (∀ D ∈ Divisor.degZero (K := AlgebraicClosure ℚ) (F := modularFunctionFieldBar N),
      D ∈ Divisor.principal (K := AlgebraicClosure ℚ) (F := modularFunctionFieldBar N) →
      fm.spDiv hred dataAll hsep D ∈
        Divisor.principal (K := k) (F := modularFunctionFieldC k N))

open Classical in

noncomputable def FibreModel.spPic0 (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable) :
    JZero N →+ Pic0 k (modularFunctionFieldC k N) :=
  if h : fm.SpDivPreservesPrincipal hred dataAll hsep then
    QuotientAddGroup.map _ _
      (AddMonoidHom.mk'
        (fun D => ⟨fm.spDiv hred dataAll hsep ↑D, h.1 ↑D D.2⟩)
        (fun D E => Subtype.ext (by
          show fm.spDiv hred dataAll hsep ↑(D + E)
              = fm.spDiv hred dataAll hsep ↑D + fm.spDiv hred dataAll hsep ↑E
          rw [AddSubgroup.coe_add]
          exact Finsupp.mapDomain_add)))
      (fun D hD => AddSubgroup.mem_comap.mpr ((AddSubgroup.mem_addSubgroupOf).mpr
        (h.2 ↑D D.2 ((AddSubgroup.mem_addSubgroupOf).mp hD))))
  else 0

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in

theorem FibreModel.piInf_mem_spPlace_nonunits_iff (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hpole : ∀ a : A,
      w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) (b : fm.BInf) :
    ((fm.piInf b : modularFunctionFieldC k N) ∈
        (fm.spPlace hred dataAll hsep w).toValuationSubring.nonunits ↔
      ∃ a : A, a ∈ IsLocalRing.maximalIdeal A ∧
        ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ))
          ∈ w.toValuationSubring.nonunits) := by
  have h := not_jBar_mem_compSubring_of_forall_ord_le w hpole
  constructor
  · intro hnu
    have hval := (fm.sp_piInf_nonunits_iff hred dataAll hsep w h b).mp hnu
    exact ⟨w.value A (Subring.inclusion (fm.binf_le_compSubring w
        ((fm.chart_dichotomy dataAll w).resolve_left h)) b), hval,
      w.hasValueAt_value A (Subring.inclusion (fm.binf_le_compSubring w
        ((fm.chart_dichotomy dataAll w).resolve_left h)) b)⟩
  · rintro ⟨a, ha, hval⟩
    have ht : ((fm.piInf b : modularFunctionFieldC k N) -
        algebraMap k (modularFunctionFieldC k N) (red a))
        ∈ (fm.spPlace hred dataAll hsep w).toValuationSubring.nonunits :=
      fm.sp_hasValueAt_inf hred dataAll hsep w h b a hval
    have hred0 : red a = 0 := (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _
      (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ) ℓ _ _ red a).mpr ha
    rwa [hred0, map_zero, sub_zero] at ht

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in

theorem FibreModel.piFin_mem_spPlace_nonunits_iff (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (a₀ : A)
    (ha₀ : 0 < w.ord (jBar N - algebraMap (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))
      (a₀ : AlgebraicClosure ℚ))) (b : fm.BFin) :
    ((fm.piFin b : modularFunctionFieldC k N) ∈
        (fm.spPlace hred dataAll hsep w).toValuationSubring.nonunits ↔
      ∃ a : A, a ∈ IsLocalRing.maximalIdeal A ∧
        ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) -
            algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ))
          ∈ w.toValuationSubring.nonunits) := by
  have hmem : (jBar N : laurentBaseChange (AlgebraicClosure ℚ)
      (modularFunctionFieldFull N)) ∈ w.compSubring A :=
    w.mem_compSubring_of_hasValueAt a₀.2 (w.hasValueAt_of_ord_pos ha₀)
  have hspec := fm.sp_spec_fin hred dataAll hsep w hmem b
  constructor
  · intro hnu
    have hcent := hspec.mp hnu
    rw [FibreModel.centreFin, Ideal.mem_comap] at hcent
    exact ⟨w.value A (Subring.inclusion (fm.bfin_le_compSubring w hmem) b),
      (w.mem_centre_iff _).mp hcent,
      w.hasValueAt_value A (Subring.inclusion (fm.bfin_le_compSubring w hmem) b)⟩
  · rintro ⟨a, ha, hval⟩
    refine hspec.mpr ?_
    rw [FibreModel.centreFin, Ideal.mem_comap]
    have hval' : w.HasValueAt
        (Subring.inclusion (fm.bfin_le_compSubring w hmem) b : laurentBaseChange
          (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ↑a := hval
    exact (w.mem_centre_iff_of_hasValueAt hval').mpr ha

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 400000 in

theorem FibreModel.jLineInv_mem_spPlace (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (w : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))
    (hpole : ∀ a : A,
      w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ)
        (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) :
    (((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N))⁻¹
      ∈ (fm.spPlace hred dataAll hsep w).toValuationSubring) :=
  fm.sp_jLineInv_mem hred dataAll hsep w
    (not_jBar_mem_compSubring_of_forall_ord_le w hpole)

set_option maxHeartbeats 1600000 in
set_option synthInstance.maxHeartbeats 400000 in

noncomputable def FibreModel.placeSpecializationOf (fm : FibreModel N A ℓ k red)
    (hred : Function.Surjective red)
    (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d)
    (hsep : (((dataAll N (dvd_refl N)).Φ.map
        (Polynomial.mapRingHom (Int.castRingHom k))).map
      (algebraMap (Polynomial k) (RatFunc k))).Separable)
    (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)
    (hα : HeckeAlphaBarIntegral (AlgebraicClosure ℚ) N ℓ)
    (hβ : HeckeBetaBarIntegral (AlgebraicClosure ℚ) N ℓ)
    (h_d0_j : ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N), ∀ a : A,
    0 < w.ord
        (⟨coeffEmb (AlgebraicClosure ℚ) jq,
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionField_le_full N (jq_mem N))⟩
          - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N)
              (a : AlgebraicClosure ℚ)) →
    0 < ((fm.spPlace hred dataAll hsep) w).ord
        (⟨jqModC k, jqModC_mem k N⟩ - algebraMap k (modularFunctionFieldC k N) (red a)))
    (h_d0_j_pole : ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N),
    (∀ a : A,
      w.ord
        (⟨coeffEmb (AlgebraicClosure ℚ) jq,
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionField_le_full N (jq_mem N))⟩
          - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N)
              (a : AlgebraicClosure ℚ)) ≤ 0) →
    ((fm.spPlace hred dataAll hsep) w).ord (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)
        < 0)
    (h_d0_jN : ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N), ∀ a : A,
    0 < w.ord
        (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq),
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (jqd_mem_full N (dvd_refl N))⟩
          - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N)
              (a : AlgebraicClosure ℚ)) →
    0 < ((fm.spPlace hred dataAll hsep) w).ord
        (⟨jqNModC k N, jqNModC_mem k N⟩
          - algebraMap k (modularFunctionFieldC k N) (red a)))
    (h_d0_jN_pole : ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N),
    (∀ a : A,
      w.ord
        (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq),
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (jqd_mem_full N (dvd_refl N))⟩
          - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N)
              (a : AlgebraicClosure ℚ)) ≤ 0) →
    ((fm.spPlace hred dataAll hsep) w).ord (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k
        N) < 0)
    (h_d1 : ∀ W : Place (AlgebraicClosure ℚ)
      (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull (N * ℓ))),
    (fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ) hα)
        = frobOnPlacesGeomLevel k N data hKr
            ((fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ)
                hβ))
      ∨ frobOnPlacesGeomLevel k N data hKr
            ((fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeAlphaBar (AlgebraicClosure ℚ) N
                ℓ) hα))
        = (fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ)
            hβ))
    (h_d2 : ∀ v : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N),
    frobOnPlacesGeomLevel k N data hKr
        (frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) v)) ≠ (fm.spPlace hred
            dataAll hsep) v →
    ∃ W₀ : Place (AlgebraicClosure ℚ)
        (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull (N * ℓ))),
      W₀.restrictAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ) hβ = v
        ∧ (fm.spPlace hred dataAll hsep) (W₀.restrictAlong (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ)
            hα)
            = frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) v)
        ∧ W₀.ramificationIndexAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ) = 1
        ∧ ∀ W : Place (AlgebraicClosure ℚ)
            (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull (N * ℓ))),
            W.restrictAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ) hβ = v →
            (fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ)
                hα)
                = frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) v) →
              W = W₀)
    (h_d4 : Function.Surjective (fm.spPlace hred dataAll hsep))
    (h_d5 : ∀ f : modularFunctionFieldBar N, f ≠ 0 →
    ∀ D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N),
      (∀ v, D v = v.ord f) →
      ∃ g : modularFunctionFieldC k N, g ≠ 0 ∧
        ∀ v' : Place k (modularFunctionFieldC k N),
          Finsupp.mapDomain (fm.spPlace hred dataAll hsep) D v' = v'.ord g)
    (h_d6_inertia : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ,
    σ ∈ A.inertiaSubgroupIn ℚ →
    ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N),
      (fm.spPlace hred dataAll hsep) (arithmeticGalois (modularFunctionFieldFull N) σ • w) =
          (fm.spPlace hred dataAll hsep) w)
    (h_d6_frobenius : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ,
    A.IsFrobeniusAt σ ℓ →
    ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N),
      (fm.spPlace hred dataAll hsep) (arithmeticGalois (modularFunctionFieldFull N) σ • w)
        = frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) w))
    (h_d7_dictInfty : ∀ (w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) (τ : A)
      (ht : (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq),
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (jqd_mem_full N (dvd_refl N))⟩ : modularFunctionFieldBar N)
          / (⟨coeffEmb (AlgebraicClosure ℚ) jq,
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionField_le_full N (jq_mem N))⟩ : modularFunctionFieldBar N) ^ N ∈
                  w.toValuationSubring),
    (∀ a : A,
      w.ord
        (⟨coeffEmb (AlgebraicClosure ℚ) jq,
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionField_le_full N (jq_mem N))⟩
          - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N)
              (a : AlgebraicClosure ℚ)) ≤ 0) →
    IsLocalRing.residue w.toValuationSubring ⟨_, ht⟩
        = algebraMap (AlgebraicClosure ℚ) w.ResidueField (τ : AlgebraicClosure ℚ) →
      ⟨jqNModC k N, jqNModC_mem k N⟩ / (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) ^ N
          - algebraMap k (modularFunctionFieldC k N) (red τ) = 0 ∨
      0 < ((fm.spPlace hred dataAll hsep) w).ord
        (⟨jqNModC k N, jqNModC_mem k N⟩ / (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) ^
            N
          - algebraMap k (modularFunctionFieldC k N) (red τ)))
    (h_d7_dictZero : ∀ (w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) (τ : A)
      (ht : (⟨coeffEmb (AlgebraicClosure ℚ) jq,
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (modularFunctionField_le_full N (jq_mem N))⟩ : modularFunctionFieldBar N)
          / (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq),
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (jqd_mem_full N (dvd_refl N))⟩ : modularFunctionFieldBar N) ^ N ∈
                  w.toValuationSubring),
    (∀ a : A,
      w.ord
        (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq),
            coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ)
              (jqd_mem_full N (dvd_refl N))⟩
          - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N)
              (a : AlgebraicClosure ℚ)) ≤ 0) →
    IsLocalRing.residue w.toValuationSubring ⟨_, ht⟩
        = algebraMap (AlgebraicClosure ℚ) w.ResidueField (τ : AlgebraicClosure ℚ) →
      ⟨jqModC k, jqModC_mem k N⟩ / (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) ^ N
          - algebraMap k (modularFunctionFieldC k N) (red τ) = 0 ∨
      0 < ((fm.spPlace hred dataAll hsep) w).ord
        (⟨jqModC k, jqModC_mem k N⟩ / (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) ^
            N
          - algebraMap k (modularFunctionFieldC k N) (red τ)))
    (h_spPic0_compat :
    ∀ D : Divisor.degZero (K := AlgebraicClosure ℚ) (F := ↥(modularFunctionFieldBar N)),
      ∃ D' : Divisor.degZero (K := k) (F := ↥(modularFunctionFieldC k N)),
        (D' : Divisor k (modularFunctionFieldC k N))
            = Finsupp.mapDomain (fm.spPlace hred dataAll hsep)
                (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N))
          ∧ (fm.spPic0 hred dataAll hsep) (Pic0.mk D) = Pic0.mk D')
    : PlaceSpecialization A ℓ N data hKr k red hα hβ :=
  ⟨fm.spPlace hred dataAll hsep, fm.spPic0 hred dataAll hsep, h_d0_j, h_d0_j_pole, h_d0_jN,
      h_d0_jN_pole, h_d1, h_d2, h_d4, h_d5, h_d6_inertia, h_d6_frobenius, h_d7_dictInfty,
      h_d7_dictZero, h_spPic0_compat⟩

end SpecializationConstruction

end CharPModel
end ModularCurve