Close-up: factor theorem

Combines the divisibility, intersection, and no-common-factor sub-cases into the main factor theorem for the close-up induction (Heitmann, Lemma 4, case n >= 3).

theorem close_up_aux_factor {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)) (m : ℕ) (ih_m : ∀ m_1 < m, ∀ (R : NSubring T), Cardinal.mk ↥R.carrier < Cardinal.mk T → ∀ (a : ↥R.carrier) (s : Finset ↥R.carrier), gcdComplexity s ≤ m_1 → s.card = n'' + 1 + 1 + 1 → a ∈ s → ∀ (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} (ih_a : ∀ (y : ↥R.carrier), DvdNotUnit y a → ∀ (s : Finset ↥R.carrier), gcdComplexity s ≤ m → s.card = n'' + 1 + 1 + 1 → y ∈ s → ∀ (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)) {s : Finset ↥R.carrier} (hs_gcd : gcdComplexity s ≤ m) (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) {p : ↥R.carrier} (_hp : Prime p) (_hp_dvd : ∀ x ∈ s', p ∣ x) (hpa : ¬p ∣ a) (hgcd_factor : ∃ (q : ↥R.carrier), Prime q ∧ (∀ x ∈ s', q ∣ x) ∧ (q ∣ a ∨ q ∣ c)) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)