Close-up: no common factor

Sub-case of the well-founded close-up induction where no prime of R divides all generators simultaneously. The key observation is that the ideal of the generators s' cannot be contained in any associated prime of height at most one, so the avoidance step applies directly.

theorem prime_height_le_one_mem_assoc {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {R : NSubring T} (P : Ideal T) (hP_prime : P.IsPrime) (hP_ht : P.height ≤ 1) (hPR_ne : Ideal.comap R.carrier.subtype P ≠ ⊥) : ∃ (r₀ : ↥R.carrier), ↑r₀ ≠ 0 ∧ P ∈ associatedPrimes T (T ⧸ Ideal.span {↑r₀})

theorem no_common_I_not_le_assoc {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {n'' : ℕ} {R : NSubring T} [DecidableEq ↥R.carrier] {a : ↥R.carrier} {s : Finset ↥R.carrier} (hs_eq : s.card = n'' + 1 + 1 + 1) (ha_mem : a ∈ s) (s' : Finset ↥R.carrier) (hs'_def : s' = s.erase a) (hno_common_prime : ∀ (p : ↥R.carrier), Prime p → ¬∀ x ∈ s', p ∣ x) (_hI_s'_bot : Ideal.map R.carrier.subtype (Ideal.span ↑s') ≠ ⊥) (r : ↥R.carrier) (hr_ne : ↑r ≠ 0) (P : Ideal T) (hP_mem : P ∈ associatedPrimes T (T ⧸ Ideal.span {↑r})) (hle : Ideal.map R.carrier.subtype (Ideal.span ↑s') ≤ P) : False

theorem close_up_aux_no_common_nonzero {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) (hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) (hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T) (n'' : ℕ) (ih : ∀ (R : NSubring T), Cardinal.mk ↥R.carrier < Cardinal.mk T → ∀ (s : Finset ↥R.carrier), s.card ≤ n'' + 1 + 1 → ∀ (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) [DecidableEq ↥R.carrier] {a : ↥R.carrier} {s : Finset ↥R.carrier} (hs_eq : s.card = n'' + 1 + 1 + 1) (ha_mem : a ∈ s) {c : ↥R.carrier} (s' : Finset ↥R.carrier) (hs'_def : s' = s.erase a) (hs_insert : s = insert a s') (hs'_card : s'.card ≤ n'' + 1 + 1) (_hgcd : ¬∃ (p : ↥R.carrier), Prime p ∧ ∀ x ∈ s', p ∣ x) (hno_common_prime : ∀ (p : ↥R.carrier), Prime p → ¬∀ x ∈ s', p ∣ x) (t u v : T) (hv : v ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s')) (ht_eq : u = R.carrier.subtype a * t) (huv : u + v = ↑c) (ha_zero : ↑a ≠ 0) (hI_s'_bot : 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)

theorem close_up_aux_no_common {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) (hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) (hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T) (n'' : ℕ) (ih : ∀ (R : NSubring T), Cardinal.mk ↥R.carrier < Cardinal.mk T → ∀ (s : Finset ↥R.carrier), s.card ≤ n'' + 1 + 1 → ∀ (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) [DecidableEq ↥R.carrier] {a : ↥R.carrier} {s : Finset ↥R.carrier} (hs_eq : s.card = n'' + 1 + 1 + 1) (ha_mem : a ∈ s) {c : ↥R.carrier} (hc : ↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s)) (s' : Finset ↥R.carrier) (hs'_def : s' = s.erase a) (hs_insert : s = insert a s') (hs'_card : s'.card ≤ n'' + 1 + 1) (hgcd : ¬∃ (p : ↥R.carrier), Prime p ∧ ∀ x ∈ s', p ∣ x) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)