-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
have : coeff d f ≠ 0
have₁ : ∀ (hfd : coeff d f ≠ 0), Irreducible f
have₂ : coeff d f ≠ 0
have₃ have₄ have₅ have₆ have₇ : ∀ (hfd : coeff d f ≠ 0), Irreducible f
have₈ :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ), Irreducible f
have₉ :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f)), Irreducible f
have₁₀ :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), Irreducible f
have₁₁ :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), Irreducible (φ * X i + ψ)
hf0 :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), φ ≠ 0
hif :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), i ∉ φ.vars
hig :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), i ∉ ψ.vars
h :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), IsRelPrime φ ψ
hif₁ :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), i ∉ φ.vars
hig₁ :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), i ∉ ψ.vars
h₁ :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), IsRelPrime φ ψ
hig₂ :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), i ∉ ψ.vars
h₂ h₃ :
  ∀ (hfd : coeff d f ≠ 0),
    let d₀ := Finsupp.erase i d;
    let φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f);
    let ψ := f - φ * X i;
    ∀ (hf : f = φ * X i + ψ) (hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f))
      (hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f), IsRelPrime φ ψ
⊢ Irreducible f

Tactic:
classical
  have hfd : f.coeff d ≠ 0 := by simpa using hd
  let d₀ := d.erase i
  let φ : MvPolynomial n R := monomial d₀ (f.coeff d)
  let ψ : MvPolynomial n R := f - φ * X i
  have hf : f = φ * X i + ψ := by grind only
  have hφ : φ * X i = monomial d (f.coeff d) := by
    nth_rw 1 [← Finsupp.erase_add_single i d]; simp [φ, monomial_add_single, hdi, d₀]
  have hdψ (k) : ψ.coeff k = if d = k then 0 else f.coeff k := by
    simp +contextual [ψ, hφ, sub_eq_iff_eq_add, ite_add_ite]
  rw [hf]
  apply irreducible_mul_X_add
  · grind only [monomial_eq_zero]
  · simp [φ, hfd, d₀, hdi]
  · suffices ∀ x, d ≠ x → x ∈ f.support → i ∉ x.support by
      simpa [mem_vars_iff_mem_support, hdψ] using this
    exact fun x hxd hx hix ↦
      Finset.disjoint_iff_ne.mp (disjoint hd hx hxd) i (by simp [hdi]) _ hix rfl
  · rintro p hpφ ⟨q, hq⟩
    obtain ⟨m, b, hm, hb, rfl⟩ := (dvd_monomial_iff_exists hfd).mp hpφ
    obtain ⟨d₂, hd₂, H⟩ := nontrivial.exists_ne d
    obtain rfl : m = 0 := by
      have aux : coeff d₂ ψ ≠ 0 := by simpa [hdψ, H.symm] using hd₂
      simp only [hq, coeff_monomial_mul', ne_eq, ite_eq_right_iff, Classical.not_imp] at aux
      simpa using disjoint hd₂ hd H (Finsupp.support_mono aux.1)
        ((Finsupp.support_mono hm).trans (d.support.erase_subset i))
    have hb' : IsUnit b := isPrimitive _ fun k ↦
      if hk : k = d then hk ▸ hb else hf ▸ by simp [hq, hφ, Ne.symm hk]
    simpa

Premises used: MvPolynomial.irreducible_mul_X_add, Finset.disjoint_iff_ne, MvPolynomial.monomial_eq_zero, Iff.mp, Finset.Nontrivial.exists_ne, rfl