Krull Domain Intersection for Two-Generator Close-Up

Given coprime y₁, y₂ in an N-subring R and c ∈ (y₁,y₂)T ∩ R, construct an A-extension S with c ∈ (y₁,y₂)S via the intersection Rbar = R[x₁, y₂⁻¹] ∩ R[x₂, y₁⁻¹] where c = x₁y₁ + x₂y₂.

theorem intersection_close_up_ker_pf₁ {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (y₂ : ↥R.carrier) (t₁ u : T) (C_ext : Set (Ideal T)) (D_ext : Set T) (hC_ext_mem : ∀ (p : ↥R.carrier), ↑p ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {↑p}), P ∈ C_ext) (hD_ext_invFun : ∀ (f : Polynomial ↥R.carrier), f ≠ 0 → ∀ P ∈ C_ext, P ≠ ⊥ → Polynomial.map ((Ideal.Quotient.mk P).comp R.carrier.subtype) f ≠ 0 → (Ideal.Quotient.mk P) ↑y₂ ≠ 0 → ∀ v₀ ∈ {v : T ⧸ P | Polynomial.eval ((Ideal.Quotient.mk P) t₁ + v * (Ideal.Quotient.mk P) ↑y₂) (Polynomial.map ((Ideal.Quotient.mk P).comp R.carrier.subtype) f) = 0}, Function.invFun (⇑(Ideal.Quotient.mk P)) v₀ ∈ D_ext) (hu_avoid : ∀ P ∈ C_ext, ∀ r ∈ D_ext, u ∉ ↑P + {r}) (P : Ideal T) (hP_prime : P.IsPrime) (_hP_ne_top : P ≠ ⊤) (hP_ht : P.height ≤ 1) (hy₂_nP : ↑y₂ ∉ P) (p : ↥R.carrier) (hp : Prime p) (hp_P : ↑p ∈ P) (f : Polynomial ↥R.carrier) (hf_mem : (Polynomial.aeval (t₁ + u * ↑y₂)) f ∈ P) : Polynomial.C p ∣ f

theorem intersection_close_up_ker_pf₂ {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (y₁ : ↥R.carrier) (t₂ u : T) (C_ext : Set (Ideal T)) (D_ext : Set T) (hC_ext_mem : ∀ (p : ↥R.carrier), ↑p ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {↑p}), P ∈ C_ext) (hD_ext_invFun : ∀ (f : Polynomial ↥R.carrier), f ≠ 0 → ∀ P ∈ C_ext, P ≠ ⊥ → Polynomial.map ((Ideal.Quotient.mk P).comp R.carrier.subtype) f ≠ 0 → (Ideal.Quotient.mk P) ↑y₁ ≠ 0 → ∀ v₀ ∈ {v : T ⧸ P | Polynomial.eval ((Ideal.Quotient.mk P) t₂ - v * (Ideal.Quotient.mk P) ↑y₁) (Polynomial.map ((Ideal.Quotient.mk P).comp R.carrier.subtype) f) = 0}, Function.invFun (⇑(Ideal.Quotient.mk P)) v₀ ∈ D_ext) (hu_avoid : ∀ P ∈ C_ext, ∀ r ∈ D_ext, u ∉ ↑P + {r}) (P : Ideal T) (hP_prime : P.IsPrime) (_hP_ne_top : P ≠ ⊤) (hP_ht : P.height ≤ 1) (hy₁_nP : ↑y₁ ∉ P) (p : ↥R.carrier) (hp : Prime p) (hp_P : ↑p ∈ P) (f : Polynomial ↥R.carrier) (hf_mem : (Polynomial.aeval (t₂ - u * ↑y₁)) f ∈ P) : Polynomial.C p ∣ f

theorem intersection_close_up {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : NSubring T) (y₁ y₂ c : ↥R.carrier) (hc : ↑c ∈ Ideal.span {↑y₁, ↑y₂}) (hcoprime : ∀ (p : ↥R.carrier), Prime p → ¬(p ∣ y₁ ∧ p ∣ y₂)) (hy₁ : ↑y₁ ≠ 0) (hy₂ : ↑y₂ ≠ 0) (hM_ne_bot : IsLocalRing.maximalIdeal T ≠ ⊥) (hM_not_assoc : ∀ (r : T), r ≠ 0 → IsLocalRing.maximalIdeal T ∉ associatedPrimes T (T ⧸ Ideal.span {r})) (hAss_ht : ∀ (r : T), r ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {r}), P.height ≤ 1) (hR_card : Cardinal.mk ↥R.carrier < Cardinal.mk T) (hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier) (x₁ : ↥S.carrier), ⟨↑c, ⋯⟩ - x₁ * ⟨↑y₁, ⋯⟩ ∈ Ideal.span {⟨↑y₂, ⋯⟩}