awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := 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
hf0 : φ ≠ 0
hif : i ∉ φ.vars
⊢ Irreducible (φ * X i + ψ)
have hig : i ∉ ψ.vars
Tactic: apply irreducible_mul_X_add
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := 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
hf0 : φ ≠ 0
hif : i ∉ φ.vars
hig : i ∉ ψ.vars
⊢ Irreducible (φ * X i + ψ)
have h : IsRelPrime φ ψ
Tactic: apply irreducible_mul_X_add
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := 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
have hig : ∀ (x : n →₀ ℕ), d ≠ x → x ∈ f.support → i ∉ x.support
Tactic: suffices ∀ x, d ≠ x → x ∈ f.support → i ∉ x.support by
      simpa [mem_vars_iff_mem_support, hdψ] using this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := 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
p : MvPolynomial n R
hpφ : p ∣ φ
q : MvPolynomial n R
hq : ψ = p * q
⊢ IsUnit p
have h : ∀ (m : n →₀ ℕ) (b : R) (hm : m ≤ d₀) (hb : b ∣ coeff d f) (hpφ : (monomial m : (a : R) → MvPolynomial n R) b ∣ φ)
  (hq : ψ = HMul.hMul (α := MvPolynomial n R) ((monomial m : (a : R) → MvPolynomial n R) b : MvPolynomial n R) q),
  IsUnit (M := MvPolynomial n R) ((monomial m : (a : R) → MvPolynomial n R) b : MvPolynomial n R)
Tactic: obtain ⟨m, b, hm, hb, rfl⟩ := (dvd_monomial_iff_exists hfd).mp hpφ
Cleared hypotheses: p, hpφ, hq
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := 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
q : MvPolynomial n R
m : n →₀ ℕ
b : R
hm : m ≤ d₀
hb : b ∣ coeff d f
hpφ : (monomial m : (a : R) → MvPolynomial n R) b ∣ φ
hq : ψ = HMul.hMul (α := MvPolynomial n R) ((monomial m : (a : R) → MvPolynomial n R) b : MvPolynomial n R) q
⊢ IsUnit (M := MvPolynomial n R) ((monomial m : (a : R) → MvPolynomial n R) b : MvPolynomial n R)
have h : ∀ (d₂ : n →₀ ℕ) (hd₂ : d₂ ∈ f.support) (H : d₂ ≠ d),
  IsUnit (M := MvPolynomial n R) ((monomial m : (a : R) → MvPolynomial n R) b : MvPolynomial n R)
Tactic: obtain ⟨d₂, hd₂, H⟩ := nontrivial.exists_ne d
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (hypothesis)
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
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := 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
q : MvPolynomial n R
m : n →₀ ℕ
b : R
hm : m ≤ d₀
hb : b ∣ coeff d f
hpφ : (monomial m : (a : R) → MvPolynomial n R) b ∣ φ
hq : ψ = HMul.hMul (α := MvPolynomial n R) ((monomial m : (a : R) → MvPolynomial n R) b : MvPolynomial n R) q
d₂ : n →₀ ℕ
hd₂ : d₂ ∈ f.support
H : d₂ ≠ d
⊢ m = 0
have aux : coeff d₂ ψ ≠ 0
Tactic: have aux : coeff d₂ ψ ≠ 0 := by simpa [hdψ, H.symm] using hd₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (hypothesis)
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
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := 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
q : MvPolynomial n R
m : n →₀ ℕ
b : R
hm : m ≤ d₀
hb : b ∣ coeff d f
hpφ : (monomial m : (a : R) → MvPolynomial n R) b ∣ φ
hq : ψ = HMul.hMul (α := MvPolynomial n R) ((monomial m : (a : R) → MvPolynomial n R) b : MvPolynomial n R) q
d₂ : n →₀ ℕ
hd₂ : d₂ ∈ f.support
H : d₂ ≠ d
aux : coeff d₂ ψ ≠ 0
⊢ m = 0
have aux₁ : m ≤ d₂ ∧ ¬b * coeff (d₂ - m) q = 0
Tactic: simp only [hq, coeff_monomial_mul', ne_eq, ite_eq_right_iff, Classical.not_imp] at aux
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := 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
q : MvPolynomial n R
m : n →₀ ℕ
b : R
hm : m ≤ d₀
hb : b ∣ coeff d f
hpφ : (monomial m : (a : R) → MvPolynomial n R) b ∣ φ
hq : ψ = HMul.hMul (α := MvPolynomial n R) ((monomial m : (a : R) → MvPolynomial n R) b : MvPolynomial n R) q
d₂ : n →₀ ℕ
hd₂ : d₂ ∈ f.support
H : d₂ ≠ d
⊢ IsUnit (M := MvPolynomial n R) ((monomial m : (a : R) → MvPolynomial n R) b : MvPolynomial n R)
have h : ∀ (hm : 0 ≤ d₀) (hpφ : (monomial 0 : (a : R) → MvPolynomial n R) b ∣ φ)
  (hq : ψ = HMul.hMul (α := MvPolynomial n R) ((monomial 0 : (a : R) → MvPolynomial n R) b : MvPolynomial n R) q),
  IsUnit (M := MvPolynomial n R) ((monomial 0 : (a : R) → MvPolynomial n R) b : MvPolynomial n R)
Tactic: 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))
Cleared hypotheses: m, hm, hpφ, hq
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (hypothesis)
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
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := 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
q : MvPolynomial n R
b : R
hb : b ∣ coeff d f
d₂ : n →₀ ℕ
hd₂ : d₂ ∈ f.support
H : d₂ ≠ d
hm : 0 ≤ d₀
hpφ : (monomial 0 : (a : R) → MvPolynomial n R) b ∣ φ
hq : ψ = HMul.hMul (α := MvPolynomial n R) ((monomial 0 : (a : R) → MvPolynomial n R) b : MvPolynomial n R) q
⊢ IsUnit (M := MvPolynomial n R) ((monomial 0 : (a : R) → MvPolynomial n R) b : MvPolynomial n R)
have hb' : IsUnit b
Tactic: have hb' : IsUnit b := isPrimitive _ fun k ↦
      if hk : k = d then hk ▸ hb else hf ▸ by simp [hq, hφ, Ne.symm hk]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ Irreducible f
have have : coeff d f ≠ 0
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ Irreducible f
have have₁ : ∀ (hfd : coeff d f ≠ 0), 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ Irreducible f
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ Irreducible f
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ Irreducible f
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
⊢ IsUnit a ∨ IsUnit b
have inr : ∀ (this : ∀ (a b : MvPolynomial n R) (hab : p = a * b) (hle : a.totalDegree ≤ b.totalDegree), IsUnit a ∨ IsUnit b)
  (hle : ¬a.totalDegree ≤ b.totalDegree), IsUnit a ∨ IsUnit b
Tactic: wlog hle : a.totalDegree ≤ b.totalDegree generalizing a b
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
inr :
  ∀ (this : ∀ (a b : MvPolynomial n R) (hab : p = a * b) (hle : a.totalDegree ≤ b.totalDegree), IsUnit a ∨ IsUnit b)
    (hle : ¬a.totalDegree ≤ b.totalDegree), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b
have wlog : ∀ (a b : MvPolynomial n R) (hab : p = a * b) (hle : a.totalDegree ≤ b.totalDegree), IsUnit a ∨ IsUnit b
Tactic: wlog hle : a.totalDegree ≤ b.totalDegree generalizing a b
Cleared hypotheses: a, b, hab
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
this : ∀ (a b : MvPolynomial n R) (hab : p = a * b) (hle : a.totalDegree ≤ b.totalDegree), IsUnit a ∨ IsUnit b
hle : ¬a.totalDegree ≤ b.totalDegree
⊢ p = b * a
have rw : a * b = b * a
Tactic: rw [hab, mul_comm]