IsFractionRing_exists_pow_mul_mem_colon_and_surjective_restrict_of_branchData.lean

def cond {B : Type u} [CommRing B] {F : Type v} [CommRing F] [Algebra B F] (y : F) : Ideal B where
  carrier := {b | ∃ c : B, algebraMap B F b * y = algebraMap B F c}
  add_mem' := by
    rintro a b ⟨c, hc⟩ ⟨d, hd⟩
    exact ⟨c + d, by rw [map_add, add_mul, hc, hd, map_add]⟩
  zero_mem' := ⟨0, by simp⟩
  smul_mem' := by
    rintro r a ⟨c, hc⟩
    exact ⟨r * c, by rw [smul_eq_mul, map_mul, mul_assoc, hc, map_mul]⟩

theorem exists_eq_algebraMap_of_forall_maximal {B : Type u} [CommRing B] {F : Type v} [CommRing F]
  [Algebra B F]
    (y : F) (h : ∀ 𝔪 : Ideal B, 𝔪.IsMaximal → ∃ b : B, b ∉ 𝔪 ∧ ∃ c : B, algebraMap B F b * y =
      algebraMap B F c) :
    ∃ c : B, y = algebraMap B F c

theorem _root_.IsFractionRing.exists_pow_mul_mem_colon_and_surjective_restrict_of_branchData
    {B : Type u} [CommRing B] [IsDomain B] [IsNoetherianRing B]
    {F : Type v} [Field F] [Algebra B F] [IsFractionRing B F]
    {ι : Type u} [Fintype ι]
    (𝔪 : ι → Ideal B) (h𝔪 : ∀ i, (𝔪 i).IsMaximal) (hinj : Function.Injective 𝔪)
    (t : ι → B) (_ht : ∀ i, t i ∈ 𝔪 i) (ht0 : ∀ i, t i ≠ 0)
    (I : ι → Ideal B)
    (hI : ∀ i (a : B), a ∈ I i ↔ ∃ s : B, s ∉ 𝔪 i ∧ s * a ∈ Ideal.span {t i})
    (hle : ∀ i (P : Ideal B), P.IsPrime → I i ≤ P → P ≤ 𝔪 i)
    (n : ℕ) :
    (∀ (x : B) (g : F),
      (∀ 𝔭 : Ideal B, 𝔭.IsPrime → x ∉ 𝔭 → ∃ s : B, s ∉ 𝔭 ∧
        ∀ a ∈ (∏ i, I i) ^ n, ∃ b : B, g * algebraMap B F a * algebraMap B F s = algebraMap B F b) →
      ∃ k : ℕ, ∀ a ∈ (∏ i, I i) ^ n, ∃ b : B, algebraMap B F x ^ k * g * algebraMap B F a =
        algebraMap B F b) ∧
    (∀ e : ι → B, ∃ g : F, (∀ a ∈ (∏ i, I i) ^ (n + 1), ∃ b : B, g * algebraMap B F a = algebraMap
      B F b) ∧
      ∀ i, ∃ (s c : B), s ∉ 𝔪 i ∧ c ∈ I i ∧
        (g * algebraMap B F (t i) ^ (n + 1) - algebraMap B F (e i)) * algebraMap B F s = algebraMap
          B F c) ∧
    (∀ g : F, (∀ a ∈ (∏ i, I i) ^ (n + 1), ∃ b : B, g * algebraMap B F a = algebraMap B F b) →
      ((∀ i, ∃ (s c : B), s ∉ 𝔪 i ∧ c ∈ I i ∧ g * algebraMap B F (t i) ^ (n + 1) * algebraMap B F s
        = algebraMap B F c) ↔
        ∀ a ∈ (∏ i, I i) ^ n, ∃ b : B, g * algebraMap B F a = algebraMap B F b))