-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
refine_2 refine_2₁ refine_2₂ : n ∈ P
refine_2₃ :
  let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
  ∀ (hp : p ∈ P) (hp0 : p ≠ 0), n ∈ P
refine_2₄ :
  let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
  ∀ (hp : p ∈ P) (hp0 : p ≠ 0) (this : p ≠ 1), n ∈ P
refine_2₅ :
  let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
  ∀ (hp : p ∈ P) (hp0 : p ≠ 0) (this : p ≠ 1) (prime : Nat.Prime p), n ∈ P
refine_2₆ :
  let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
  ∀ (hp : p ∈ P) (hp0 : p ≠ 0) (this : p ≠ 1) (prime : Nat.Prime p) (hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p}),
    n ∈ P
refine_2₇ :
  let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
  ∀ (hp : p ∈ P) (hp0 : p ≠ 0) (this : p ≠ 1) (prime : Nat.Prime p) (hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p})
    (q : ℕ) (hq : q ∈ P) (hqp : q ∉ span {p}), n ∈ P
refine_2₈ :
  let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
  ∀ (hp : p ∈ P) (hp0 : p ≠ 0) (this : p ≠ 1) (prime : Nat.Prime p) (hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p})
    (q : ℕ) (hq : q ∈ P) (hqp : q ∉ span {p}) (hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) 0), 0 ∈ P
refine_2₉ refine_2₁₀ :
  let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
  ∀ (hp : p ∈ P) (hp0 : p ≠ 0) (this : p ≠ 1) (prime : Nat.Prime p) (hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p})
    (q : ℕ) (hq : q ∈ P) (hqp : q ∉ span {p}) (hn1 : n ≠ 0), n ∈ P
refine_2₁₁ :
  let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
  ∀ (hp : p ∈ P) (hp0 : p ≠ 0) (this : p ≠ 1) (prime : Nat.Prime p) (hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p})
    (q : ℕ) (hq : q ∈ P) (hqp : q ∉ span {p}) (hn1 : n ≠ 0) (this : n ≠ 1), n ∈ P
refine_2₁₂ :
  let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
  ∀ (hp : p ∈ P) (hp0 : p ≠ 0) (this : p ≠ 1) (prime : Nat.Prime p) (hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p})
    (q : ℕ) (hq : q ∈ P) (hqp : q ∉ span {p}) (hn1 : n ≠ 0) (this : n ≠ 1) (a b : ℕ)
    (eq : a * p + b * q = n ^ (p.pred * q.pred)), n ∈ P
⊢ n ∈ P

Tactic:
classical
  let p := Nat.find h0
  have ⟨(hp : p ∈ P), (hp0 : p ≠ 0)⟩ := Nat.find_spec h0
  have : p ≠ 1 := ne_of_mem_of_not_mem hp P.one_notMem
  have prime : p.Prime := Nat.prime_iff_not_exists_mul_eq.mpr <| .intro (by lia)
    fun ⟨m, n, hm, hn, eq⟩ ↦ have := mul_ne_zero_iff.mp (eq ▸ hp0)
    (h.mem_or_mem (eq ▸ hp)).elim (Nat.find_min h0 hm ⟨·, this.1⟩) (Nat.find_min h0 hn ⟨·, this.2⟩)
  push Not at hsp
  have ⟨q, hq, hqp⟩ := SetLike.exists_of_lt
    ((P.span_singleton_le_iff_mem.mpr hp).lt_of_ne (hsp p prime).symm)
  obtain rfl | hn1 := eq_or_ne n 0
  · exact Ideal.zero_mem _
  have : n ≠ 1 := Nat.mem_maximalIdeal_iff.mp hn
  have ⟨a, b, eq⟩ := Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le p q _
    (by simp [prime.coprime_iff_not_dvd.mpr (Ideal.mem_span_singleton.not.mp hqp)])
    (Nat.lt_pow_self (show 1 < n by lia)).le
  exact h.mem_of_pow_mem _ (eq ▸ add_mem (P.mul_mem_left _ hp) (P.mul_mem_left _ hq))

Premises used: Ideal.IsPrime.mem_of_pow_mem, Ideal.zero_mem, eq_or_ne, OfNat.ofNat, Not, rfl