awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
rw : Irreducible (φ * X i + ψ)
⊢ Irreducible f

Tactic:
rw [hf]
-- 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
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
h : IsRelPrime φ ψ
⊢ Irreducible (φ * X i + ψ)

Tactic:
apply irreducible_mul_X_add

Premises used: MvPolynomial.irreducible_mul_X_add
-- 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
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
⊢ φ ≠ 0

Tactic:
grind only [monomial_eq_zero]

Premises used: MvPolynomial.monomial_eq_zero
-- 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
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

Tactic:
simp [φ, hfd, d₀, hdi]
-- 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
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
this : ∀ (x : n →₀ ℕ), d ≠ x → x ∈ f.support → i ∉ x.support
⊢ i ∉ ψ.vars

Tactic:
simpa [mem_vars_iff_mem_support, hdψ] using this

Premises used: MvPolynomial.mem_vars_iff_mem_support
-- 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
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
hig : ∀ (x : n →₀ ℕ), d ≠ x → x ∈ f.support → i ∉ x.support
⊢ i ∉ ψ.vars

Tactic:
suffices ∀ x, d ≠ x → x ∈ f.support → i ∉ x.support by
      simpa [mem_vars_iff_mem_support, hdψ] using this
-- 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
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
x : n →₀ ℕ
hxd : d ≠ x
hx : x ∈ f.support
hix : i ∈ x.support
⊢ i ∈ d.support

Tactic:
simp [hdi]
-- 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
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
⊢ ∀ (x : n →₀ ℕ), d ≠ x → x ∈ f.support → i ∉ x.support

Tactic:
exact fun x hxd hx hix ↦
      Finset.disjoint_iff_ne.mp (disjoint hd hx hxd) i (by simp [hdi]) _ hix rfl

Premises used: Finset.disjoint_iff_ne, Iff.mp, rfl
-- 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
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
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)
⊢ IsUnit p

Tactic:
obtain ⟨m, b, hm, hb, rfl⟩ := (dvd_monomial_iff_exists hfd).mp hpφ

Premises used: MvPolynomial.dvd_monomial_iff_exists, Iff.mp, rfl
-- 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
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
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)
⊢ 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

Premises used: Finset.Nontrivial.exists_ne
-- 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
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
⊢ coeff d₂ ψ ≠ 0

Tactic:
simpa [hdψ, H.symm] using hd₂

Premises used: Ne.symm
-- 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
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
⊢ coeff d₂ ψ ≠ 0

Tactic:
have aux : coeff d₂ ψ ≠ 0 := by simpa [hdψ, H.symm] using hd₂
-- 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
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 ≤ 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

Premises used: MvPolynomial.coeff_monomial_mul', ne_eq, ite_eq_right_iff, Classical.not_imp
-- 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
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 : m ≤ d₂ ∧ ¬b * coeff (d₂ - m) q = 0
⊢ m = 0

Tactic:
simpa using disjoint hd₂ hd H (Finsupp.support_mono aux.1)
        ((Finsupp.support_mono hm).trans (d.support.erase_subset i))

Premises used: Finsupp.support, HasSubset.Subset.trans, Finsupp.support_mono, And.left, Finset.erase_subset
-- 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
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
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)
⊢ IsUnit (M := MvPolynomial n R) ((monomial m : (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))

Premises used: rfl
-- 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
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
k : n →₀ ℕ
hk : ¬k = d
⊢ b ∣ coeff k (φ * X i + ψ)

Tactic:
simp [hq, hφ, Ne.symm hk]

Premises used: Ne.symm
-- 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
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 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]
-- 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
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
hb' : IsUnit b
⊢ IsUnit (M := MvPolynomial n R) ((monomial 0 : (a : R) → MvPolynomial n R) b : MvPolynomial n R)

Tactic:
simpa
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
H : IsUnit p
⊢ False

Tactic:
simp [(MvPolynomial.isUnit_iff_totalDegree_of_isReduced.mp H).2] at hp

Premises used: MvPolynomial.isUnit_iff_totalDegree_of_isReduced, And.right, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
wlog : ∀ (a b : MvPolynomial n R) (hab : p = a * b) (hle : a.totalDegree ≤ b.totalDegree), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
wlog hle : a.totalDegree ≤ b.totalDegree generalizing a b

Premises used: MvPolynomial.totalDegree
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
rw : a * b = b * a
rw₁ rw₂ : b * a = b * a
⊢ p = b * a

Tactic:
rw [hab, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
⊢ b.totalDegree ≤ a.totalDegree

Tactic:
lia
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
⊢ IsUnit a ∨ IsUnit b

Tactic:
exact (this b a (by rw [hab, mul_comm]) (by lia)).symm

Premises used: Or.symm
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
hle : a.totalDegree ≤ b.totalDegree
inl :
  ∀ (hab : p = 0 * b) (hle : totalDegree.{u_2, u_1} (R := R) (σ := n) 0 ≤ b.totalDegree),
    IsUnit (M := MvPolynomial n R) 0 ∨ IsUnit b
inr : ∀ (ha₀ : a ≠ 0), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
b : MvPolynomial n R
hab : p = 0 * b
hle : totalDegree.{u_2, u_1} (R := R) (σ := n) 0 ≤ b.totalDegree
⊢ IsUnit (M := MvPolynomial n R) 0 ∨ IsUnit b

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
inr :
  ∀ (hab : p = a * 0) (hle : a.totalDegree ≤ totalDegree.{u_2, u_1} (R := R) (σ := n) 0),
    IsUnit a ∨ IsUnit (M := MvPolynomial n R) 0
inr₁ : ∀ (hb₀ : b ≠ 0), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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 : MvPolynomial n R
ha₀ : a ≠ 0
hab : p = a * 0
hle : a.totalDegree ≤ totalDegree.{u_2, u_1} (R := R) (σ := n) 0
⊢ IsUnit a ∨ IsUnit (M := MvPolynomial n R) 0

Tactic:
simp_all