-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
mpr₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  (f * g).coeff (m + n) ∉ P
mpr₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
let let₁ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∑ x ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff x.1 * g.coeff x.2 ∈ P
let₂ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ c ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
let₃ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ (i j : ℕ) (hij : (i, j) ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n)),
    f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
let₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ (i j : ℕ) (hij : (i, j) ≠ (m, n) ∧ (i, j).1 + (i, j).2 = (m, n).1 + (m, n).2),
    f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
let₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ (i j : ℕ) (hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
inl :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ (i j : ℕ) (hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n) (hi : i < m), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
inr inr₁ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ (i j : ℕ) (hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n) (hj : j < n), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P

Tactic:
classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        rw [coeff_mul, ← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m, n))).mpr rfl),
          Finset.sum_insert (Finset.notMem_erase _ _), (P.add_mem_iff_left _).not]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)

Premises used: Submodule.sum_mem, Prod.mk_inj, mt, Polynomial.coeff_mul, Iff.not, Ne, not_or, Finset.mem_erase, Finset.HasAntidiagonal.mem_antidiagonal, not_and_or, mul_comm, Ideal.add_mem_iff_left, Ideal.IsPrime.mem_or_mem', Finset.notMem_erase, Finset.sum_insert, Ideal.mul_mem_left