-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hI : I ∈ (N.colon {x}).minimalPrimes
hx : x ∉ N
neg : ∃ (x' : M), I = N.colon {x'}
neg₁ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes), ∃ (x' : M), I = N.colon {x'}
neg₂ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I),
    ∃ (x' : M), I = N.colon {x'}
neg₃ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I)
    (hn0 : Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key ≠ 0) (J : Ideal R)
    (hJ : I ^ Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key * J ≤ ann)
    (hJI : ¬J ≤ I), ∃ (x' : M), I = N.colon {x'}
neg₄ neg₅ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hn0 : n ≠ 0) (hJ : I ^ n * J ≤ ann), ∃ (x' : M), I = N.colon {x'}
neg₆ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hn0 : n ≠ 0) (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}), ∃ (x' : M), I = N.colon {x'}
neg₇ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}), ∃ (x' : M), I = N.colon {x'}
neg₈ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}), ∃ (y : ↥K), N.colon {y • x} ≤ I
neg₉ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (h' : ∀ (y : ↥K), ¬N.colon {y • x} ≤ I), False
neg₁₀ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (h' : ∀ (y : ↥K), ∃ x_1 ∈ N.colon {y • x}, x_1 ∉ I), False
neg₁₁ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x})
        (h : ∀ (y : ↥K), f y ∉ I), False
neg₁₂ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x})
        (h : ∀ (y : ↥K), f y ∉ I) (s : Finset ↥K) (hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤), False
neg₁₃ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x})
        (h : ∀ (y : ↥K), f y ∉ I) (s : Finset ↥K) (hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤), False
neg₁₄ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x})
        (h : ∀ (y : ↥K), f y ∉ I) (s : Finset ↥K) (hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤),
        let z : R := ∏ y ∈ s, f y;
        ∀ (hz : z ∉ I), False
neg₁₅ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x})
        (h : ∀ (y : ↥K), f y ∉ I) (s : Finset ↥K) (hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤),
        let z : R := ∏ y ∈ s, f y;
        ∀ (hz : z ∉ I) (hz' : K ≤ N.colon {z • x}), False
neg₁₆ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x})
        (h : ∀ (y : ↥K), f y ∉ I) (s : Finset ↥K) (hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤),
        let z : R := ∏ y ∈ s, f y;
        ∀ (hz : z ∉ I) (hz' : K * Ideal.span {z} ≤ ann), False
neg₁₇ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x})
        (h : ∀ (y : ↥K), f y ∉ I) (s : Finset ↥K) (hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤),
        let z : R := ∏ y ∈ s, f y;
        ∀ (hz : z ∉ I) (hz' : K * Ideal.span {z} ≤ ann)
          (hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I), False
pos :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x})
        (h : ∀ (y : ↥K), f y ∉ I) (s : Finset ↥K) (hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤),
        let z : R := ∏ y ∈ s, f y;
        ∀ (hz : z ∉ I) (hz' : K * Ideal.span {z} ≤ ann)
          (hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I) (hn' : n - 1 = 0), False
neg₁₈ neg₁₉ :
  let ann := N.colon {x};
  ∀ (hI : I ∈ ann.minimalPrimes) (key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) (J : Ideal R)
    (hJI : ¬J ≤ I),
    let n := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key;
    ∀ (hJ : I ^ n * J ≤ ann),
      let K := I ^ (n - 1) * J;
      ∀ (step1 : ∀ y ∈ K, I ≤ N.colon {y • x}) (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x})
        (h : ∀ (y : ↥K), f y ∉ I) (s : Finset ↥K) (hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤),
        let z : R := ∏ y ∈ s, f y;
        ∀ (hz : z ∉ I) (hz' : K * Ideal.span {z} ≤ ann)
          (hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I) (hn' : ¬n - 1 = 0), False
⊢ ∃ (x' : M), I = N.colon {x'}

Tactic:
classical
  -- `I` is a minimal prime over `ann = colon N {x}`
  set ann := colon N {x}
  -- there exists an integer `n ≠ 0` and an ideal `J` satisfying `I ^ n * J ≤ ann` and `¬ J ≠ I`
  have key : ∃ n ≠ 0, ∃ J : Ideal R, I ^ n * J ≤ ann ∧ ¬ J ≤ I := by
    -- let `n` be large enough so that `ann.radical ^ n ≤ ann` (uses Noetherian)
    obtain ⟨n, hn⟩ := ann.exists_radical_pow_le_of_fg ann.radical.fg_of_isNoetherianRing
    have hn0 : n ≠ 0 := by contrapose hn; simpa [hn, ann]
    -- then take `J` to be the product of the other minimal primes raised to the `n`th power
    have h := ann.finite_minimalPrimes_of_isNoetherianRing R
    rw [← ann.sInf_minimalPrimes, ← h.coe_toFinset, ← h.toFinset.inf_id_eq_sInf,
      ← Finset.insert_erase (h.mem_toFinset.mpr hI), Finset.inf_insert, id_eq] at hn
    grw [← Ideal.mul_le_inf, mul_pow] at hn
    refine ⟨n, hn0, ((h.toFinset.erase I).inf id) ^ n, hn, ?_⟩
    have (K : Ideal R) (hKI : K ≤ I) (hK : K ∈ ann.minimalPrimes) : K = I :=
      le_antisymm hKI (hI.2 hK.1 hKI)
    simpa [hI.isPrime.pow_le_iff hn0, hI.isPrime.inf_le', imp_not_comm, not_imp_not]
  obtain ⟨hn0, J, hJ, hJI⟩ := Nat.find_spec key
  -- let `n` be minimal such that there exists an ideal `J` with `I ^ n * J ≤ ann` and `¬ J ≠ I`
  set n := Nat.find key
  -- the minimality of `n` will allow us to pick `x'` from the ideal `K = I ^ (n - 1) * J`
  let K := I ^ (n - 1) * J
  -- we want `I = colon N {x'}`, and we have `I ≤ colon N {y • x}` for every `y ∈ K` (uses `n ≠ 0`)
  have step1 : ∀ y ∈ K, I ≤ colon N {y • x} := by
    intro y hy p hp
    rw [mem_colon_singleton, smul_smul, ← mem_colon_singleton]
    apply hJ
    simpa [K, ← mul_assoc, mul_pow_sub_one hn0] using mul_mem_mul hp hy
  clear hn0
  -- so it suffices to find a single `y ∈ K` with `colon N {y • x} ≤ I`
  suffices step2 : ∃ y : K, colon N {y • x} ≤ I by
    obtain ⟨y, hyI⟩ := step2
    exact ⟨y • x, le_antisymm (step1 y y.2) hyI⟩
  -- if not, then for every `y ∈ K`, there exists an `f y ∈ colon N {y • x}` with `f y ∉ I`
  by_contra! h'
  simp only [SetLike.not_le_iff_exists] at h'
  choose f g h using h'
  -- let `s` be a finite generating set for `K`
  obtain ⟨s, hs⟩ : (⊤ : Submodule R K).FG := Module.Finite.fg_top
  -- let `z` be the product of these finitely many `f y`'s
  let z := ∏ y ∈ s, f y
  -- then `z ∉ I`
  have hz : z ∉ I := by simp [z, hI.isPrime.prod_mem_iff, h]
  -- and `K ≤ colon N {z • x}`
  have hz' : K ≤ colon N {z • x} := by
    rw [← (map_injective_of_injective K.subtype_injective).eq_iff, map_subtype_top] at hs
    rw [← hs, map_span, span_le, Set.image_subset_iff]
    intro i hi
    rw [Set.mem_preimage, SetLike.mem_coe, mem_colon_singleton, smul_comm, ← mem_colon_singleton]
    obtain ⟨y, hy : z = f i * y⟩ := Finset.dvd_prod_of_mem f hi
    exact hy ▸ Ideal.mul_mem_right y _ (g i)
  -- or equivalently `K * Ideal.span {z} ≤ ann`
  replace hz' : K * Ideal.span {z} ≤ ann := by
    rw [mul_comm, Ideal.span_singleton_mul_le_iff]
    intro i hi
    simpa only [ann, mem_colon_singleton, mul_comm, mul_smul] using hz' hi
  -- but now `K = I ^ (n - 1) * J` contradicts the minimality of `n`
  have hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬ J * Ideal.span {z} ≤ I := by
    rw [← mul_assoc, hI.isPrime.mul_le, not_or, Ideal.span_singleton_le_iff_mem]
    exact ⟨hz', hJI, hz⟩
  by_cases hn' : n - 1 = 0
  · simp [K, show n = 1 by grind] at hz'
    exact (hK.2 (hz'.trans hI.le)).elim
  · grind [Nat.find_min' key ⟨hn', J * Ideal.span {z}, hK⟩]

Premises used: Module.Finite.fg_top, Submodule.colon, SetLike.not_le_iff_exists, Singleton.singleton