IsDiscreteValuationRing_primesOver_integralClosure_eq_range_of_finrank_le_sum_inertiaDeg.lean

theorem mem_of_isIntegral (V : ValuationSubring F) (hOV : ∀ x : O, algebraMap O F x ∈ V)
    {y : F} (hy : IsIntegral O y) : y ∈ V

def toV : ↥(integralClosure O F) →+* ↥V

theorem coe_toV (b : ↥(integralClosure O F)) : ((toV V hOV b : ↥V) : F) = (b : F)

def centre : Ideal ↥(integralClosure O F)

instance isPrime_centre : (centre V hOV).IsPrime

theorem mem_centre_iff (b : ↥(integralClosure O F)) : b ∈ centre V hOV ↔ (b : F) ∈ V.nonunits

theorem instances_B (E : Type*) [Field E] [Algebra O E] [IsFractionRing O E] [Algebra E F]
    [IsScalarTower O E F] [FiniteDimensional E F] [Algebra.IsSeparable E F] :
    IsDedekindDomain ↥(integralClosure O F) ∧ Module.Finite O ↥(integralClosure O F) ∧
      IsFractionRing ↥(integralClosure O F) F

instance faithfulSMul_B : FaithfulSMul O ↥(integralClosure O F)

theorem comap_centre : (centre V hOV).comap (algebraMap O ↥(integralClosure O F)) = maximalIdeal O

theorem liesOver_centre : (centre V hOV).LiesOver (maximalIdeal O)

theorem centre_ne_bot : centre V hOV ≠ ⊥

theorem card_le_inertiaDeg [IsDedekindDomain ↥(integralClosure O F)] [Module.Finite O
  ↥(integralClosure O F)]
    {ι : Type*} [Fintype ι] (b : ι → F) (hb : ∀ i, IsIntegral O (b i))
    (hres : ∀ c : ι → O, (∑ i, algebraMap O F (c i) * b i) ∈ V.nonunits → ∀ i, c i ∈ maximalIdeal
      O) :
    Fintype.card ι ≤ (centre V hOV).inertiaDeg O

theorem primesOverFinset_eq_and_ramificationIdx_eq
    (E : Type*) [Field E] [Algebra O E] [IsFractionRing O E] [Algebra E F]
    [IsScalarTower O E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
    [IsDedekindDomain ↥(integralClosure O F)] [Module.Finite O ↥(integralClosure O F)]
    [IsFractionRing ↥(integralClosure O F) F]
    (hd : Module.finrank E F ≤ (centre V hOV).inertiaDeg O) :
    IsDedekindDomain.primesOverFinset (maximalIdeal O) ↥(integralClosure O F) = {centre V hOV} ∧
      Ideal.ramificationIdx' (maximalIdeal O) (centre V hOV) = 1 ∧
      (centre V hOV).inertiaDeg O = Module.finrank E F

def centreHOS [IsDedekindDomain ↥(integralClosure O F)] (h0 : centre V hOV ≠ ⊥) :
    HeightOneSpectrum ↥(integralClosure O F)

theorem valuationSubringAtPrime_le [IsDedekindDomain ↥(integralClosure O F)] [IsFractionRing
  ↥(integralClosure O F) F]
    (h0 : centre V hOV ≠ ⊥) :
    HeightOneSpectrum.valuationSubringAtPrime F (centreHOS V hOV h0) ≤ V

theorem eq_valuationSubringAtPrime [IsDedekindDomain ↥(integralClosure O F)] [IsFractionRing
  ↥(integralClosure O F) F]
    (hV : V ≠ ⊤) (h0 : centre V hOV ≠ ⊥) :
    HeightOneSpectrum.valuationSubringAtPrime F (centreHOS V hOV h0) = V

theorem centre_eq_map [IsDedekindDomain ↥(integralClosure O F)] [Module.Finite O ↥(integralClosure
  O F)]
    (hprimes :
      IsDedekindDomain.primesOverFinset (maximalIdeal O) ↥(integralClosure O F) = {centre V hOV})
    (he : Ideal.ramificationIdx' (maximalIdeal O) (centre V hOV) = 1) :
    centre V hOV = (maximalIdeal O).map (algebraMap O ↥(integralClosure O F))

theorem valuationSubring_unique_of_residues_linearIndependent
    (E : Type*) [Field E] [Algebra O E] [IsFractionRing O E] [Algebra E F]
    [IsScalarTower O E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
    (V : ValuationSubring F) (hV : V ≠ ⊤) (hOV : ∀ x : O, algebraMap O F x ∈ V)
    (hdom : ∀ x ∈ maximalIdeal O, algebraMap O F x ∈ V.nonunits)
    (b : Fin (Module.finrank E F) → F) (hb : ∀ i, IsIntegral O (b i))
    (hres : ∀ c : Fin (Module.finrank E F) → O,
      (∑ i, algebraMap O F (c i) * b i) ∈ V.nonunits → ∀ i, c i ∈ maximalIdeal O) :
    (∀ V' : ValuationSubring F, V' ≠ ⊤ → (∀ x : O, algebraMap O F x ∈ V') →
        (∀ x ∈ maximalIdeal O, algebraMap O F x ∈ V'.nonunits) → V' = V) ∧
    (∀ ϖ : O, Irreducible ϖ → ∀ x ∈ V, x ∈ V.nonunits → ∃ y ∈ V, x = algebraMap O F ϖ * y)

theorem exists_valuationSubring_mem_iff_presentation
    {R : Type*} [CommRing R] [IsDomain R] [Algebra R F] [IsFractionRing R F]
    (𝔭 : Ideal R) [𝔭.IsPrime] [ValuationRing (Localization.AtPrime 𝔭)] :
    ∃ W : ValuationSubring F, ∀ x : F, x ∈ W ↔ ∃ r s : R, s ∉ 𝔭 ∧ x * algebraMap R F s = algebraMap
      R F r

theorem centre_injective [IsDedekindDomain ↥(integralClosure O F)] [IsFractionRing
  ↥(integralClosure O F) F]
    {ι : Type*} (V : ι → ValuationSubring F) (hV : ∀ i, V i ≠ ⊤) (hOV : ∀ i, ∀ x : O, algebraMap O
      F x ∈ V i)
    (hdom : ∀ i, ∀ x ∈ maximalIdeal O, algebraMap O F x ∈ (V i).nonunits)
    (hinj : Function.Injective V) :
    Function.Injective (fun i => centre (V i) (hOV i)) := by
  intro i j h
  apply hinj
  have hi := eq_valuationSubringAtPrime (V i) (hOV i) (hV i) (centre_ne_bot (V i) (hOV i) (hdom i))
  have hj := eq_valuationSubringAtPrime (V j) (hOV j) (hV j) (centre_ne_bot (V j) (hOV j) (hdom j))
  rw [← hi, ← hj]
  congr 1
  exact HeightOneSpectrum.ext h

theorem primesOverFinset_eq_image
    (E : Type*) [Field E] [Algebra O E] [IsFractionRing O E] [Algebra E F]
    [IsScalarTower O E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
    [IsDedekindDomain ↥(integralClosure O F)] [Module.Finite O ↥(integralClosure O F)]
    [IsFractionRing ↥(integralClosure O F) F]
    {ι : Type*} [Fintype ι] (V : ι → ValuationSubring F) (hV : ∀ i, V i ≠ ⊤)
    (hOV : ∀ i, ∀ x : O, algebraMap O F x ∈ V i)
    (hdom : ∀ i, ∀ x ∈ maximalIdeal O, algebraMap O F x ∈ (V i).nonunits)
    (hinj : Function.Injective V)
    (d : ι → ℕ) (hd : ∀ i, d i ≤ (centre (V i) (hOV i)).inertiaDeg O)
    (hsum : Module.finrank E F ≤ ∑ i, d i) :
    IsDedekindDomain.primesOverFinset (maximalIdeal O) ↥(integralClosure O F) = Finset.univ.image
      (fun i => centre (V i) (hOV i)) ∧
    (∀ i, Ideal.ramificationIdx' (maximalIdeal O) (centre (V i) (hOV i)) = 1) ∧
    (∀ i, (centre (V i) (hOV i)).inertiaDeg O = d i) ∧
    ∑ i, d i = Module.finrank E F := by
  classical
  have hp0 : maximalIdeal O ≠ ⊥ := IsDiscreteValuationRing.not_a_field O
  have hsumEF :
      ∑ P ∈ IsDedekindDomain.primesOverFinset (maximalIdeal O) ↥(integralClosure O F),
        (maximalIdeal O).ramificationIdx' P * P.inertiaDeg O =
          Module.finrank E F := by
    calc
      _ = ∑ P : (maximalIdeal O).primesOver ↥(integralClosure O F),
            P.1.ramificationIdx O * P.1.inertiaDeg O := by
          refine Finset.sum_bij
            (fun P hP => (⟨P, (IsDedekindDomain.mem_primesOverFinset_iff hp0
              ↥(integralClosure O F)).mp hP⟩ :
                (maximalIdeal O).primesOver ↥(integralClosure O F))) ?_ ?_ ?_ ?_
          · intro _ _
            exact Finset.mem_univ _
          · intro _ _ _ _ hEq
            exact congrArg Subtype.val hEq
          · intro ⟨P, hP⟩ _
            exact ⟨P, (IsDedekindDomain.mem_primesOverFinset_iff hp0
              ↥(integralClosure O F)).mpr hP, rfl⟩
          · intro P hP
            obtain ⟨hPprime, hPover⟩ :=
              (IsDedekindDomain.mem_primesOverFinset_iff hp0 ↥(integralClosure O F)).mp hP
            let : P.IsPrime := hPprime
            let : P.LiesOver (maximalIdeal O) := hPover
            rw [Ideal.ramificationIdx'_eq_ramificationIdx _ _ hp0]
      _ = Module.finrank O ↥(integralClosure O F) :=
        Ideal.sum_ramification_inertia_eq_finrank (maximalIdeal O) ↥(integralClosure O F)
      _ = Module.finrank E F :=
        (IsFractionRing.finrank_eq O E ↥(integralClosure O F) F).symm
  set s := IsDedekindDomain.primesOverFinset (maximalIdeal O) ↥(integralClosure O F) with hs
  set 𝔓 : ι → Ideal ↥(integralClosure O F) := fun i => centre (V i) (hOV i) with h𝔓
  set I := Finset.univ.image 𝔓 with hI
  have h𝔓inj : Function.Injective 𝔓 := centre_injective V hV hOV hdom hinj
  have hmem : ∀ i, 𝔓 i ∈ s := fun i => by
    have := liesOver_centre (V i) (hOV i) (hdom i)
    exact (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨inferInstance, inferInstance⟩
  have hIs : I ⊆ s := by
    intro P hP
    obtain ⟨i, -, rfl⟩ := Finset.mem_image.mp hP
    exact hmem i
  set t : Ideal ↥(integralClosure O F) → ℕ :=
    fun P => Ideal.ramificationIdx' (maximalIdeal O) P * P.inertiaDeg O with ht
  have hpos : ∀ P ∈ s, 1 ≤ t P := by
    intro P hP
    have hP' := (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mp hP
    have : P.IsPrime := hP'.1
    have : P.LiesOver (maximalIdeal O) := hP'.2
    have he : Ideal.ramificationIdx' (maximalIdeal O) P ≠ 0 :=
      Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver P hp0
    have hf : P.inertiaDeg O ≠ 0 := (Ideal.inertiaDeg_pos P O).ne'
    exact Nat.one_le_iff_ne_zero.mpr (mul_ne_zero he hf)
  have he1 : ∀ i, 1 ≤ Ideal.ramificationIdx' (maximalIdeal O) (𝔓 i) := by
    intro i
    have := liesOver_centre (V i) (hOV i) (hdom i)
    exact Nat.one_le_iff_ne_zero.mpr (Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver
      (𝔓 i) hp0)
  have h1 : ∑ P ∈ I, t P ≤ ∑ P ∈ s, t P := Finset.sum_le_sum_of_subset_of_nonneg hIs (fun P _ _ =>
    Nat.zero_le _)
  have h2 : ∑ P ∈ I, t P = ∑ i, t (𝔓 i) := by
    rw [hI, Finset.sum_image (fun i _ j _ h => h𝔓inj h)]
  have h3 : ∀ i, (𝔓 i).inertiaDeg O ≤ t (𝔓 i) := fun i =>
    Nat.le_mul_of_pos_left _ (he1 i)
  have h4 : ∑ i, d i ≤ ∑ i, (𝔓 i).inertiaDeg O := Finset.sum_le_sum (fun i _ => hd i)
  have h5 : ∑ i, (𝔓 i).inertiaDeg O ≤ ∑ i, t (𝔓 i) := Finset.sum_le_sum (fun i _ => h3 i)
  have hsumEF' : ∑ P ∈ s, t P = Module.finrank E F := hsumEF
  have hchain : ∑ P ∈ s, t P ≤ ∑ i, d i := hsumEF' ▸ hsum
  have hEq1 : ∑ P ∈ I, t P = ∑ P ∈ s, t P := by omega
  have hEq2 : ∑ i, (𝔓 i).inertiaDeg O = ∑ i, t (𝔓 i) := by omega
  have hEq3 : ∑ i, d i = ∑ i, (𝔓 i).inertiaDeg O := by omega
  have hsI : s = I := by
    refine (Finset.Subset.antisymm ?_ hIs)
    intro P hP
    by_contra hPI
    have hlt : ∑ Q ∈ I, t Q < ∑ Q ∈ s, t Q :=
      Finset.sum_lt_sum_of_subset hIs hP hPI (hpos P hP) (fun Q _ _ => Nat.zero_le _)
    omega
  have hterm : ∀ i ∈ Finset.univ, (𝔓 i).inertiaDeg O = t (𝔓 i) :=
    (Finset.sum_eq_sum_iff_of_le (fun i _ => h3 i)).mp hEq2
  have hterm' : ∀ i ∈ Finset.univ, d i = (𝔓 i).inertiaDeg O :=
    (Finset.sum_eq_sum_iff_of_le (fun i _ => hd i)).mp hEq3
  refine ⟨hsI, fun i => ?_, fun i => (hterm' i (Finset.mem_univ i)).symm, by omega⟩
  have hfpos : 0 < (𝔓 i).inertiaDeg O := by
    have := liesOver_centre (V i) (hOV i) (hdom i)
    exact Ideal.inertiaDeg_pos _ _
  have := hterm i (Finset.mem_univ i)
  rw [ht] at this
  exact (Nat.eq_of_mul_eq_mul_right hfpos (by rw [one_mul]; exact this.symm))

theorem map_eq_prod_centre [IsDedekindDomain ↥(integralClosure O F)] [Module.Finite O
  ↥(integralClosure O F)]
    {ι : Type*} [Fintype ι] (V : ι → ValuationSubring F)
    (hOV : ∀ i, ∀ x : O, algebraMap O F x ∈ V i)
    (hdom : ∀ i, ∀ x ∈ maximalIdeal O, algebraMap O F x ∈ (V i).nonunits)
    (h𝔓inj : Function.Injective (fun i => centre (V i) (hOV i)))
    (hprimes : IsDedekindDomain.primesOverFinset (maximalIdeal O) ↥(integralClosure O F) =
      Finset.univ.image (fun i => centre (V i) (hOV i)))
    (he : ∀ i, Ideal.ramificationIdx' (maximalIdeal O) (centre (V i) (hOV i)) = 1) :
    (maximalIdeal O).map (algebraMap O ↥(integralClosure O F)) = ∏ i, centre (V i) (hOV i) := by
  classical
  have hp0 : maximalIdeal O ≠ ⊥ := IsDiscreteValuationRing.not_a_field O
  have hmap0 : Ideal.map (algebraMap O ↥(integralClosure O F)) (maximalIdeal O) ≠ ⊥ :=
    (Ideal.map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective O _)).not.mpr hp0
  set m := UniqueFactorizationMonoid.factors (Ideal.map (algebraMap O ↥(integralClosure O F))
    (maximalIdeal O)) with hm
  have hcount : ∀ P, m.count P ≤ 1 := by
    intro P
    by_cases hP : P ∈ m
    · have hP' : P ∈ IsDedekindDomain.primesOverFinset (maximalIdeal O) ↥(integralClosure O F) :=
        Multiset.mem_toFinset.mpr hP
      rw [hprimes] at hP'
      obtain ⟨i, -, rfl⟩ := Finset.mem_image.mp hP'
      rw [hm, ← Ideal.IsDedekindDomain.ramificationIdx'_eq_factors_count hmap0 inferInstance
        (centre_ne_bot (V i) (hOV i) (hdom i)), he i]
    · rw [Multiset.count_eq_zero_of_notMem hP]; exact Nat.zero_le _
  have hnodup : m.Nodup := Multiset.nodup_iff_count_le_one.mpr hcount
  have hprod := UniqueFactorizationMonoid.factors_prod hmap0
  rw [← hm] at hprod
  rw [← associated_iff_eq.mp hprod]
  have hmf : m.toFinset = Finset.univ.image (fun i => centre (V i) (hOV i)) := by rw [← hprimes]
  calc m.prod = (m.toFinset.val).prod := by rw [Multiset.toFinset_val, hnodup.dedup]
    _ = ∏ P ∈ m.toFinset, P := by rw [Finset.prod_eq_multiset_prod, Multiset.map_id']
    _ = ∏ i, centre (V i) (hOV i) := by rw [hmf, Finset.prod_image (fun i _ j _ h => h𝔓inj h)]

theorem valuationSubring_mem_of_inertiaDeg_le
    (E : Type*) [Field E] [Algebra O E] [IsFractionRing O E] [Algebra E F]
    [IsScalarTower O E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
    {ι : Type*} [Fintype ι] (V : ι → ValuationSubring F) (hV : ∀ i, V i ≠ ⊤)
    (hOV : ∀ i, ∀ x : O, algebraMap O F x ∈ V i)
    (hdom : ∀ i, ∀ x ∈ maximalIdeal O, algebraMap O F x ∈ (V i).nonunits)
    (hinj : Function.Injective V)
    (d : ι → ℕ)
    (hd : ∀ (_hB : IsDedekindDomain ↥(integralClosure O F)) (_hBf : Module.Finite O
      ↥(integralClosure O F)),
      ∀ i, d i ≤ (centre (V i) (hOV i)).inertiaDeg O)
    (hsum : Module.finrank E F ≤ ∑ i, d i) :
    (∀ V' : ValuationSubring F, V' ≠ ⊤ → (∀ x : O, algebraMap O F x ∈ V') →
        (∀ x ∈ maximalIdeal O, algebraMap O F x ∈ V'.nonunits) → ∃ i, V' = V i) ∧
    (∀ i, ∀ ϖ : O, Irreducible ϖ → ∀ x ∈ V i, x ∈ (V i).nonunits → ∃ y ∈ V i, x = algebraMap O F ϖ
      * y) ∧
    (∑ i, d i = Module.finrank E F) ∧
    (∀ i, (centre (V i) (hOV i)).inertiaDeg O = d i) ∧
    (∀ i, Ideal.ramificationIdx' (maximalIdeal O) (centre (V i) (hOV i)) = 1)

theorem valuationSubring_mem_of_residues_linearIndependent_family
    (E : Type*) [Field E] [Algebra O E] [IsFractionRing O E] [Algebra E F]
    [IsScalarTower O E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
    {ι : Type*} [Fintype ι] (V : ι → ValuationSubring F) (hV : ∀ i, V i ≠ ⊤)
    (hOV : ∀ i, ∀ x : O, algebraMap O F x ∈ V i)
    (hdom : ∀ i, ∀ x ∈ maximalIdeal O, algebraMap O F x ∈ (V i).nonunits)
    (hinj : Function.Injective V)
    (d : ι → ℕ) (b : ∀ i, Fin (d i) → F) (hb : ∀ i j, IsIntegral O (b i j))
    (hres : ∀ i, ∀ c : Fin (d i) → O,
      (∑ j, algebraMap O F (c j) * b i j) ∈ (V i).nonunits → ∀ j, c j ∈ maximalIdeal O)
    (hsum : Module.finrank E F ≤ ∑ i, d i) :
    (∀ V' : ValuationSubring F, V' ≠ ⊤ → (∀ x : O, algebraMap O F x ∈ V') →
        (∀ x ∈ maximalIdeal O, algebraMap O F x ∈ V'.nonunits) → ∃ i, V' = V i) ∧
    (∀ i, ∀ ϖ : O, Irreducible ϖ → ∀ x ∈ V i, x ∈ (V i).nonunits → ∃ y ∈ V i, x = algebraMap O F ϖ
      * y) ∧
    (∑ i, d i = Module.finrank E F) ∧
    (∀ i, (centre (V i) (hOV i)).inertiaDeg O = d i) ∧
    (∀ i, Ideal.ramificationIdx' (maximalIdeal O) (centre (V i) (hOV i)) = 1)

theorem mem_valuationSubringAtPrime_iff {B : Type*} [CommRing B] [IsDedekindDomain B] [Algebra B F]
  [IsFractionRing B F]
    (v : HeightOneSpectrum B) (x : F) :
    x ∈ HeightOneSpectrum.valuationSubringAtPrime F v ↔ ∃ a s : B, s ∉ v.asIdeal ∧ x * algebraMap B
      F s = algebraMap B F a

theorem valuationSubringAtPrime_data [IsDedekindDomain ↥(integralClosure O F)] [IsFractionRing
  ↥(integralClosure O F) F]
    (𝔓 : Ideal ↥(integralClosure O F)) [𝔓.IsPrime] (h0 : 𝔓 ≠ ⊥) [𝔓.LiesOver (maximalIdeal O)] :
    let W := HeightOneSpectrum.valuationSubringAtPrime F ⟨𝔓, inferInstance, h0⟩
    ∃ (hOV : ∀ x : O, algebraMap O F x ∈ W),
      (∀ x ∈ maximalIdeal O, algebraMap O F x ∈ W.nonunits) ∧ W ≠ ⊤ ∧ centre W hOV = 𝔓 := by
  intro W
  have hB : ∀ b : ↥(integralClosure O F), (b : F) ∈ W := fun b =>
    (mem_valuationSubringAtPrime_iff _ _).mpr ⟨b, 1, fun h => (Ideal.ne_top_iff_one _).mp
      (Ideal.IsPrime.ne_top inferInstance) h,
      by rw [map_one, mul_one]; rfl⟩
  have hOV : ∀ x : O, algebraMap O F x ∈ W := fun x => hB (algebraMap O ↥(integralClosure O F) x)
  have hnon : ∀ b : ↥(integralClosure O F), b ∈ 𝔓 → (b : F) ∈ W.nonunits := by
    intro b hb
    rw [ValuationSubring.mem_nonunits_iff_or]
    by_cases hb0 : (b : F) = 0
    · exact Or.inl hb0
    · refine Or.inr (fun hinv => ?_)
      obtain ⟨a, s, hs, has⟩ := (mem_valuationSubringAtPrime_iff _ _).mp hinv
      apply hs
      have : s = a * b := by
        apply FaithfulSMul.algebraMap_injective ↥(integralClosure O F) F
        rw [map_mul, ← has]
        change _ = (b : F)⁻¹ * algebraMap _ F s * (b : F)
        field_simp
      rw [this]; exact 𝔓.mul_mem_left a hb
  have hcen : ∀ b : ↥(integralClosure O F), (b : F) ∈ W.nonunits → b ∈ 𝔓 := by
    intro b hb
    by_contra hbn
    rw [ValuationSubring.mem_nonunits_iff_or] at hb
    rcases hb with hb0 | hinv
    · exact hbn (by rw [show b = 0 from Subtype.ext hb0]; exact 𝔓.zero_mem)
    · apply hinv
      refine (mem_valuationSubringAtPrime_iff _ _).mpr ⟨1, b, hbn, ?_⟩
      have hb0 : (b : F) ≠ 0 := fun h => hbn
        (by rw [show b = 0 from Subtype.ext h]; exact 𝔓.zero_mem)
      rw [map_one]
      exact inv_mul_cancel₀ hb0
  refine ⟨hOV, ?_, ?_, ?_⟩
  · intro x hx
    have : algebraMap O ↥(integralClosure O F) x ∈ 𝔓 := by
      rw [← Ideal.mem_comap, ← Ideal.under_def, ← Ideal.over_def 𝔓 (maximalIdeal O)]; exact hx
    exact hnon _ this
  · intro htop
    obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible O
    have hϖm : ϖ ∈ maximalIdeal O := (IsDiscreteValuationRing.irreducible_iff_uniformizer ϖ).mp hϖ
      ▸ Ideal.mem_span_singleton_self ϖ
    have hmem : algebraMap O ↥(integralClosure O F) ϖ ∈ 𝔓 := by
      rw [← Ideal.mem_comap, ← Ideal.under_def, ← Ideal.over_def 𝔓 (maximalIdeal O)]; exact hϖm
    have hn := hnon _ hmem
    rw [ValuationSubring.mem_nonunits_iff_or] at hn
    rcases hn with h0 | hinv
    · exact hϖ.ne_zero (FaithfulSMul.algebraMap_injective O F (by rw [map_zero]; exact h0))
    · exact hinv (htop ▸ ValuationSubring.mem_top _)
  · ext b
    rw [mem_centre_iff]
    exact ⟨hcen b, hnon b⟩

theorem of_primes
    (E : Type*) [Field E] [Algebra O E] [IsFractionRing O E] [Algebra E F]
    [IsScalarTower O E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
    [IsDedekindDomain ↥(integralClosure O F)] [Module.Finite O ↥(integralClosure O F)]
    [IsFractionRing ↥(integralClosure O F) F]
    {ι : Type*} [Fintype ι] (𝔓 : ι → Ideal ↥(integralClosure O F))
    [hprime : ∀ i, (𝔓 i).IsPrime] (h0 : ∀ i, 𝔓 i ≠ ⊥) [hover : ∀ i, (𝔓 i).LiesOver (maximalIdeal O)]
    (hinj : Function.Injective 𝔓)
    (d : ι → ℕ) (hd : ∀ i, d i ≤ (𝔓 i).inertiaDeg O) (hsum : Module.finrank E F ≤ ∑ i, d i) :
    (maximalIdeal O).primesOver ↥(integralClosure O F) = Set.range 𝔓 ∧
    (∀ i, Ideal.ramificationIdx' (maximalIdeal O) (𝔓 i) = 1) ∧
    (∀ i, (𝔓 i).inertiaDeg O = d i) ∧
    (∑ i, d i = Module.finrank E F) ∧
    (∀ V' : ValuationSubring F, V' ≠ ⊤ → (∀ x : O, algebraMap O F x ∈ V') →
        (∀ x ∈ maximalIdeal O, algebraMap O F x ∈ V'.nonunits) →
        ∃ i, V' = HeightOneSpectrum.valuationSubringAtPrime F ⟨𝔓 i, hprime i, h0 i⟩) ∧
    (∀ i, ∀ ϖ : O, Irreducible ϖ → ∀ x ∈ HeightOneSpectrum.valuationSubringAtPrime F ⟨𝔓 i, hprime
      i, h0 i⟩,
        x ∈ (HeightOneSpectrum.valuationSubringAtPrime F ⟨𝔓 i, hprime i, h0 i⟩).nonunits →
        ∃ y ∈ HeightOneSpectrum.valuationSubringAtPrime F ⟨𝔓 i, hprime i, h0 i⟩, x = algebraMap O F
          ϖ * y)

theorem
  _root_.IsDiscreteValuationRing.primesOver_integralClosure_eq_range_of_finrank_le_sum_inertiaDeg
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {F : Type*} [Field F] [Algebra O F] [FaithfulSMul O F]
    (E : Type*) [Field E] [Algebra O E] [IsFractionRing O E] [Algebra E F]
    [IsScalarTower O E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
    [IsDedekindDomain ↥(integralClosure O F)] [Module.Finite O ↥(integralClosure O F)]
    [IsFractionRing ↥(integralClosure O F) F]
    {ι : Type*} [Fintype ι] (𝔓 : ι → Ideal ↥(integralClosure O F))
    [hprime : ∀ i, (𝔓 i).IsPrime] (h0 : ∀ i, 𝔓 i ≠ ⊥) [hover : ∀ i, (𝔓 i).LiesOver
      (IsLocalRing.maximalIdeal O)]
    (hinj : Function.Injective 𝔓)
    (d : ι → ℕ) (hd : ∀ i, d i ≤ (𝔓 i).inertiaDeg O) (hsum : Module.finrank E F ≤ ∑ i, d i) :
    (IsLocalRing.maximalIdeal O).primesOver ↥(integralClosure O F) = Set.range 𝔓 ∧
    (∀ i, Ideal.ramificationIdx' (IsLocalRing.maximalIdeal O) (𝔓 i) = 1) ∧
    (∀ i, (𝔓 i).inertiaDeg O = d i) ∧
    (∑ i, d i = Module.finrank E F) ∧
    (∀ V' : ValuationSubring F, V' ≠ ⊤ → (∀ x : O, algebraMap O F x ∈ V') →
        (∀ x ∈ IsLocalRing.maximalIdeal O, algebraMap O F x ∈ V'.nonunits) →
        ∃ i, V' = IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime F ⟨𝔓 i, hprime i, h0
          i⟩) ∧
    (∀ i, ∀ ϖ : O, Irreducible ϖ → ∀ x ∈ IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime
      F ⟨𝔓 i, hprime i, h0 i⟩,
        x ∈ (IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime F ⟨𝔓 i, hprime i, h0
          i⟩).nonunits →
        ∃ y ∈ IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime F ⟨𝔓 i, hprime i, h0 i⟩, x
          = algebraMap O F ϖ * y)