Close-up: B2 sub-case

The B2 sub-case of the well-founded close-up induction: a common prime p divides every element of s' but divides neither a nor c. The argument splits on whether the ideal generated by s' is zero or not, and reduces to the factor and intersection cases.

theorem close_up_aux_b2_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)) (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} {s : Finset ↥R.carrier} (hs_gcd : gcdComplexity s ≤ m) (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) {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) (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_b2 {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} {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) {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)