Prove prime_avoidance

Stream: mathlib4

[Young]

import Mathlib.Tactic
import Mathlib.RingTheory.Ideal.Prime

import Mathlib.Data.Finset.Insert
import Mathlib.Algebra.BigOperators.Group.Finset
import Mathlib.RingTheory.Ideal.Defs
import Mathlib.RingTheory.Ideal.BigOperators
import Mathlib.Data.Finset.Attach
import Mathlib.Data.Finset.Image
import Mathlib.Data.Finset.Erase

theorem mem_insert_self {α : Type*} [DecidableEq α] (a : α) (s : Finset α) :
    a ∈ insert a s := by
  rw [Finset.mem_insert]
  exact Or.inl rfl

theorem mem_insert_of_mem {α : Type*} [DecidableEq α] (a b : α) (s : Finset α) :
    b ∈ s → b ∈ insert a s := by
  intro h
  rw [Finset.mem_insert]
  exact Or.inr h

theorem Ideal.not_mem_of_not_mem_sum {R : Type*} [Semiring R] [AddCommMonoid R] {I : Ideal R} {ι : Type*} [DecidableEq ι] {s : Finset ι} {f : ι → R} :
    (∑ i ∈ s, f i ∉ I) → (∃ i ∈ s, f i ∉ I) := by
  induction s using Finset.induction
  case empty =>
    simp
    intro h
    exfalso
    apply h
    exact I.zero_mem
  case insert i s hi ih =>
    rw [Finset.sum_insert hi]
    intro h
    by_contra h'
    push_neg at h'
    apply h
    exact I.add_mem (h' i (mem_insert_self i s)) (ih fun j hj => h' j (mem_insert_of_mem i j s hj))


private lemma prime_avoidance_ {R : Type*} [Ring R] [DecidableEq (Ideal R)] (S : Finset (Ideal R)) (I: Ideal R) ( n : ℕ ) (hne : S.card = n + 1) (hpi : ∀ P ∈ S, P.IsPrime) (hnc : ∀ P ∈ S, ¬ ((I: Set R) ⊆ P)) : (∃ x ∈ I, ∀ P ∈  S, x ∉ P) := by
    induction n
    case zero =>
      simp at *
      rw [Finset.card_eq_one] at hne
      rcases hne with ⟨Q, hQ⟩
      have hQ' : Q ∈ S := by
        rw [hQ]
        exact Finset.mem_singleton_self Q
      rcases Set.not_subset.1 (hnc Q hQ') with ⟨x, hx, hnx⟩
      use x
      constructor
      · exact hx
      · intro P hP
        rw [hQ] at hP
        rw [Finset.mem_singleton.1 hP]
        exact hnx
    case succ _ k resₖx =>
      have c : ∀ P ∈ S, ∃ xₚ ∈ I, ∀ Q ∈ S.erase P, xₚ ∉ Q := by
        intro P hP
        have hneₖ : (S.erase P).card = k + 1 := by
          rw [Finset.card_erase_of_mem hP,hne]
          simp
        have hpiₖ : ∀ Q ∈ S.erase P, Q.IsPrime := by
          intro Q hQ
          exact hpi Q (Finset.mem_erase.1 hQ).2
        have hncₖ : ∀ Q ∈ S.erase P, ¬ ((I: Set R) ⊆ Q) := by
          intro Q hQ
          exact hnc Q (Finset.mem_erase.1 hQ).2
        rcases prime_avoidance_ (S.erase P) I k hneₖ hpiₖ hncₖ with ⟨xₚ, hxₚ, hₚ⟩
        use xₚ
      let x_Ps := S.attach.map (λ P => (c P P.2).choose)
      let x := x_Ps.sum
      use x
      constructor
      ·
        apply Ideal.sum_mem
        intro P _
        exact (c P P.prop).choose_spec.1
      ·
        intro P hP
        have hx_P : x_Ps.sum ∉ P := by
          apply Ideal.not_mem_of_not_mem_sum
          intro Q hQ hxQ
          rw [Finset.mem_map] at hQ
          rcases hQ with ⟨Q', hQ', hQ''⟩
          rw [← hQ'']
          exact (c Q' Q'.2).choose_spec.2 P (Finset.mem_erase_of_ne_of_mem (ne_of_mem_of_not_mem hQ' (fun h => hP (h.symm))) hQ')
        exact hx_P


theorem prime_avoidance {R : Type*} [Ring R] [DecidableEq (Ideal R)] (S : Finset (Ideal R)) (I: Ideal R) (hne : S.Nonempty) (hpi : ∀ P ∈ S, P.IsPrime) (hnc : ∀ P ∈ S, ¬ (I <= P)) : (∃ x ∈ I, ∀ P ∈  S, x ∉ P) := by
    apply Finset.card_ne_zero.2 at hne
    generalize hS : S.card = n
    induction n
    case zero => contradiction
    case succ _ k _ =>
      exact prime_avoidance_ S I k hS hpi hnc

[Young]

let x_Ps := S.attach.map (λ P => (c P P.2).choose)

This is somewhere terrible.

[Notification Bot]

This topic was moved here from #lean4 > Prove prime_avoidance by Kevin Buzzard.