Close-up: avoidance step

The prime-avoidance step in the general close-up construction. Given generators {a} union s' with c in their T-span, if no common prime factor of the elements of s' divides both a and c, one obtains the required A-extension by applying prime avoidance (Heitmann, Lemma 4).

theorem close_up_avoidance_step {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) 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) {m : ℕ} (ih : ∀ (R : NSubring T), Cardinal.mk ↥R.carrier < Cardinal.mk T → ∀ (s : Finset ↥R.carrier), s.card ≤ m → ∀ (c : ↥R.carrier), ↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s) → ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)) (R : NSubring T) (hR_card : Cardinal.mk ↥R.carrier < Cardinal.mk T) (hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) (hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T) (a : ↥R.carrier) (s' : Finset ↥R.carrier) (hs'_card : s'.card ≤ m) (c : ↥R.carrier) (hc : ↑c ∈ Ideal.map R.carrier.subtype (Ideal.span (insert a ↑s'))) (h_no_common : ∀ (q : ↥R.carrier), Prime q → ¬∀ x ∈ s', q ∣ x) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span (insert a ↑s'))