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
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
hb₀ : b ≠ 0
⊢ a.totalDegree + b.totalDegree = 1

Tactic:
simpa [totalDegree_mul_of_isDomain, ha₀, hb₀, hp] using congr(($hab).totalDegree).symm

Premises used: congrArg, MvPolynomial.totalDegree_mul_of_isDomain, id, MvPolynomial.totalDegree, Eq.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
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ a.totalDegree + b.totalDegree = 1

Tactic:
have : a.totalDegree + b.totalDegree = 1 := by
      simpa [totalDegree_mul_of_isDomain, ha₀, hb₀, hp] using congr(($hab).totalDegree).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
ha₀ : a ≠ 0
hb₀ : b ≠ 0
this : a.totalDegree + b.totalDegree = 1
⊢ a.totalDegree = 0

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
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
hb₀ : b ≠ 0
this : a.totalDegree + b.totalDegree = 1
inr :
  ∀ (r : R) (hab : p = HMul.hMul (α := MvPolynomial n R) ((C : (a : R) → MvPolynomial n R) r : MvPolynomial n R) b)
    (hle : totalDegree.{u_2, u_1} (R := R) (σ := n) ((C : (a : R) → MvPolynomial n R) r) ≤ b.totalDegree)
    (ha₀ : Ne (α := MvPolynomial n R) ((C : (a : R) → MvPolynomial n R) r : MvPolynomial n R) (0 : MvPolynomial n R))
    (this : totalDegree.{u_2, u_1} (R := R) (σ := n) ((C : (a : R) → MvPolynomial n R) r) + b.totalDegree = 1),
    IsUnit (M := MvPolynomial n R) ((C : (a : R) → MvPolynomial n R) r : MvPolynomial n R) ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain ⟨r, rfl⟩ : ∃ r, a = C r := ⟨_, (totalDegree_eq_zero_iff_eq_C (p := a)).mp (by lia)⟩

Premises used: 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
hb₀ : b ≠ 0
r : R
hab : p = HMul.hMul (α := MvPolynomial n R) ((C : (a : R) → MvPolynomial n R) r : MvPolynomial n R) b
hle : totalDegree.{u_2, u_1} (R := R) (σ := n) ((C : (a : R) → MvPolynomial n R) r) ≤ b.totalDegree
ha₀ : Ne (α := MvPolynomial n R) ((C : (a : R) → MvPolynomial n R) r : MvPolynomial n R) (0 : MvPolynomial n R)
this : totalDegree.{u_2, u_1} (R := R) (σ := n) ((C : (a : R) → MvPolynomial n R) r) + b.totalDegree = 1
i : n →₀ ℕ
⊢ r ∣ coeff i p

Tactic:
simp [hab]
-- 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
hb₀ : b ≠ 0
r : R
hab : p = HMul.hMul (α := MvPolynomial n R) ((C : (a : R) → MvPolynomial n R) r : MvPolynomial n R) b
hle : totalDegree.{u_2, u_1} (R := R) (σ := n) ((C : (a : R) → MvPolynomial n R) r) ≤ b.totalDegree
ha₀ : Ne (α := MvPolynomial n R) ((C : (a : R) → MvPolynomial n R) r : MvPolynomial n R) (0 : MvPolynomial n R)
this : totalDegree.{u_2, u_1} (R := R) (σ := n) ((C : (a : R) → MvPolynomial n R) r) + b.totalDegree = 1
⊢ IsUnit (M := MvPolynomial n R) ((C : (a : R) → MvPolynomial n R) r : MvPolynomial n R) ∨ IsUnit b

Tactic:
simp [hp' r fun i ↦ by simp [hab]]
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i : n
rw :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ c.support,
        coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) x : R) (X x)) :
      R)
    ((c : (a : n) → R) i : R)
⊢ Eq.{u_2 + 1} (α := R) (coeff (Finsupp.single i 1) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) : R)
    ((c : (a : n) → R) i : R)

Tactic:
rw [sumSMulX, Finsupp.linearCombination_apply, Finsupp.sum, coeff_sum]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, MvPolynomial.sumSMulX, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i : n
⊢ i ∉ c.support →
    coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) i : R) (X i)) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i : n
rw :
  coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) i : R) (X i)) =
    (c : (a : n) → R) i
rw₁ :
  ∀ b ∈ c.support,
    b ≠ i →
      coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) b : R) (X b)) = 0
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ c.support,
        coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) x : R) (X x)) :
      R)
    ((c : (a : n) → R) i : R)

Tactic:
rw [Finset.sum_eq_single i _ (by simp)]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i : n
⊢ coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) i : R) (X i)) =
    (c : (a : n) → R) i

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i j : n
hj : j ∈ c.support
hji : j ≠ i
rw : HSMul.hSMul (α := R) (β := R) ((c : (a : n) → R) j : R) 0 = 0
hnc : ¬Eq (α := n →₀ ℕ) (Finsupp.single j 1) (Finsupp.single i 1)
⊢ coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) j : R) (X j)) = 0

Tactic:
rw [coeff_smul, coeff_X', if_neg]

Premises used: MvPolynomial.coeff_smul, MvPolynomial.coeff_X', if_neg
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i j : n
hj : j ∈ c.support
hji : j ≠ i
⊢ HSMul.hSMul (α := R) (β := R) ((c : (a : n) → R) j : R) 0 = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i j : n
hj : j ∈ c.support
hji : j ≠ i
hnc hnc₁ hnc₂ hnc₃ : ¬j = i
⊢ ¬Eq (α := n →₀ ℕ) (Finsupp.single j 1) (Finsupp.single i 1)

Tactic:
rwa [Finsupp.single_left_inj Nat.one_ne_zero]

Premises used: Nat.one_ne_zero, Finsupp.single_left_inj
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i : n
rw :
  Eq.{u_2 + 1} (α := R)
    (coeff (Finsupp.single i 1) ((Finsupp.linearCombination R X : (a : n →₀ R) → MvPolynomial n R) c) : R)
    ((c : (a : n) → R) i : R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    (coeff (Finsupp.single i 1) (c.sum fun (i : n) (a : R) ↦ HSMul.hSMul (β := MvPolynomial n R) a (X i)) : R)
    ((c : (a : n) → R) i : R)
rw₂ :
  Eq.{u_2 + 1} (α := R)
    (coeff (Finsupp.single i 1)
        (∑ a ∈ c.support, HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) a : R) (X a)) :
      R)
    ((c : (a : n) → R) i : R)
rw₃ rw₄ rw₅ :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ c.support,
        coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) x : R) (X x)) :
      R)
    ((c : (a : n) → R) i : R)
rw₆ :
  coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) i : R) (X i)) =
    (c : (a : n) → R) i
rw₇ rw₈ rw₉ :
  ∀ (j : n) (hj : j ∈ c.support) (hji : j ≠ i),
    coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) j : R) (X j)) = 0
rw₁₀ : ∀ (j : n) (hj : j ∈ c.support) (hji : j ≠ i), HSMul.hSMul (α := R) (β := R) ((c : (a : n) → R) j : R) 0 = 0
hnc hnc₁ : ∀ (j : n) (hj : j ∈ c.support) (hji : j ≠ i), ¬Eq (α := n →₀ ℕ) (Finsupp.single j 1) (Finsupp.single i 1)
⊢ Eq.{u_2 + 1} (α := R) (coeff (Finsupp.single i 1) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) : R)
    ((c : (a : n) → R) i : R)

Tactic:
classical
  rw [sumSMulX, Finsupp.linearCombination_apply, Finsupp.sum, coeff_sum]
  rw [Finset.sum_eq_single i _ (by simp)]
  · simp
  intro j hj hji
  rw [coeff_smul, coeff_X', if_neg]
  · simp
  · rwa [Finsupp.single_left_inj Nat.one_ne_zero]

Premises used: Finsupp.sum, MvPolynomial.coeff_smul, Nat.one_ne_zero, Finsupp.linearCombination_apply, Finset.sum_eq_single, MvPolynomial.sumSMulX, MvPolynomial.coeff_X', Finsupp.single_left_inj, if_neg, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
hp : totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)) → IsUnit x
⊢ Irreducible (M := MvPolynomial n R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c : MvPolynomial n R)

Tactic:
apply irreducible_of_totalDegree_eq_one

Premises used: MvPolynomial.irreducible_of_totalDegree_eq_one
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
hp : totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) ≤ 1
hp₁ : 1 ≤ totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)
⊢ totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
hp :
  totalDegree.{u_2, u_1} (R := R) (σ := n)
      (∑ x ∈ c.support, HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) x : R) (X x)) ≤
    1
⊢ totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) ≤ 1

Tactic:
simp only [sumSMulX, Finsupp.linearCombination_apply, Finsupp.sum]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, MvPolynomial.sumSMulX
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
hp : ∀ i ∈ c.support, (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) i : R) (X i)).totalDegree ≤ 1
⊢ totalDegree.{u_2, u_1} (R := R) (σ := n)
      (∑ x ∈ c.support, HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) x : R) (X x)) ≤
    1

Tactic:
apply totalDegree_finsetSum_le

Premises used: MvPolynomial.totalDegree_finsetSum_le
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
i : n
h : i ∈ c.support
hp : totalDegree.{u_2, u_1} (R := R) (X i) ≤ 1
⊢ (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) i : R) (X i)).totalDegree ≤ 1

Tactic:
apply le_trans (totalDegree_smul_le ..)

Premises used: MvPolynomial.totalDegree_smul_le, le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
i : n
h : i ∈ c.support
⊢ totalDegree.{u_2, u_1} (R := R) (X i) ≤ 1

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
hp :
  ¬∀ (m : n →₀ ℕ),
      Membership.mem (γ := Finset (n →₀ ℕ))
          (support.{u_2, u_1} (R := R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)) m →
        ∀ (x : n), Eq (α := ℕ) ((m : (a : n) → ℕ) x : ℕ) (0 : ℕ)
⊢ 1 ≤ totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)

Tactic:
rw [← not_lt, Nat.lt_one_iff, totalDegree_eq_zero_iff]

Premises used: MvPolynomial.totalDegree_eq_zero_iff, not_lt, Nat.lt_one_iff
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
h :
  ∀ (m : n →₀ ℕ),
    Membership.mem (γ := Finset (n →₀ ℕ)) (support.{u_2, u_1} (R := R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c))
        m →
      ∀ (x : n), Eq (α := ℕ) ((m : (a : n) → ℕ) x : ℕ) (0 : ℕ)
hp : ∀ (i : n) (hi : i ∈ c.support), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := hc_nonempty
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
h :
  ∀ (m : n →₀ ℕ),
    Membership.mem (γ := Finset (n →₀ ℕ)) (support.{u_2, u_1} (R := R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c))
        m →
      ∀ (x : n), Eq (α := ℕ) ((m : (a : n) → ℕ) x : ℕ) (0 : ℕ)
i : n
hi : i ∈ c.support
⊢ Ne.{u_2 + 1} (α := R) ((c : (a : n) → R) i : R) (0 : R)

Tactic:
simp only [Finsupp.mem_support_iff] at hi

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
h :
  ∀ (m : n →₀ ℕ),
    Membership.mem (γ := Finset (n →₀ ℕ)) (support.{u_2, u_1} (R := R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c))
        m →
      ∀ (x : n), Eq (α := ℕ) ((m : (a : n) → ℕ) x : ℕ) (0 : ℕ)
i : n
hi : Ne.{u_2 + 1} (α := R) ((c : (a : n) → R) i : R) (0 : R)
rwa : Ne.{u_2 + 1} (α := R) (coeff (Finsupp.single i 1) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)) 0
rwa₁ rwa₂ rwa₃ rwa₄ : Ne.{u_2 + 1} (α := R) ((c : (a : n) → R) i : R) (0 : R)
⊢ Membership.mem (γ := Finset (n →₀ ℕ)) (support.{u_2, u_1} (R := R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c))
    (Finsupp.single i 1)

Tactic:
rwa [mem_support_iff, coeff_sumSMulX]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.coeff_sumSMulX
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
h :
  ∀ (m : n →₀ ℕ),
    Membership.mem (γ := Finset (n →₀ ℕ)) (support.{u_2, u_1} (R := R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c))
        m →
      ∀ (x : n), Eq (α := ℕ) ((m : (a : n) → ℕ) x : ℕ) (0 : ℕ)
i : n
hi : Ne.{u_2 + 1} (α := R) ((c : (a : n) → R) i : R) (0 : R)
⊢ Eq (α := ℕ) ((Finsupp.single i 1 : (a : n) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
specialize h (Finsupp.single i 1) (by
        rwa [mem_support_iff, coeff_sumSMulX]) i

Premises used: OfNat.ofNat, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
i : n
hi : Ne.{u_2 + 1} (α := R) ((c : (a : n) → R) i : R) (0 : R)
h : Eq (α := ℕ) ((Finsupp.single i 1 : (a : n) → ℕ) i : ℕ) (0 : ℕ)
⊢ False

Tactic:
simp only [Finsupp.single_eq_same, one_ne_zero] at h

Premises used: Finsupp.single_eq_same, one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
r : R
hr : ∀ (i : n →₀ ℕ), r ∣ coeff i ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)
hp' : ∀ (i : n), r ∣ (c : (a : n) → R) i
⊢ IsUnit r

Tactic:
apply hc_gcd
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
r : R
hr : ∀ (i : n →₀ ℕ), r ∣ coeff i ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)
i : n
⊢ r ∣ (c : (a : n) → R) i

Tactic:
simpa [coeff_sumSMulX] using hr (Finsupp.single i 1)

Premises used: MvPolynomial.coeff_sumSMulX, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
i j : n
⊢ Eq.{u_1 + 1} (α := n ⊕ n →₀ ℕ)
      ((fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1)) i)
      ((fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1)) j) →
    i = j

Tactic:
simp +contextual [Finsupp.ext_iff, Finsupp.single_apply, ite_eq_iff']

Premises used: ite_eq_iff', Finsupp.single_apply, Finsupp.ext_iff
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := ⋯ }
rw :
  Eq (α := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((Finsupp.embDomain ι c).sum Finsupp.single : Finsupp.{u_1, u_2} (n ⊕ n →₀ ℕ) R)
⊢ (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c

Tactic:
rw [← Finsupp.sum_single (Finsupp.embDomain _ _)]

Premises used: Finsupp.embDomain, Finsupp.sum_single
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := ⋯ }
simp :
  Eq (α := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    (c.sum fun (i : n) (a : R) ↦
      (monomial (HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1)) :
          (a : R) → MvPolynomial (n ⊕ n) R)
        a)
    (c.sum fun (a : n) (b : R) ↦
      Finsupp.single (HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl a) 1) (Finsupp.single (Sum.inr a) 1)) b)
⊢ Eq (α := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((Finsupp.embDomain ι c).sum Finsupp.single : Finsupp.{u_1, u_2} (n ⊕ n →₀ ℕ) R)

Tactic:
simp [Finsupp.sum_embDomain, sumSMulXSMulY, X, monomial_mul,
      Finsupp.linearCombination_apply, smul_monomial, ι]

Premises used: MvPolynomial.smul_monomial, MvPolynomial.X, Finsupp.sum_embDomain, Finsupp.linearCombination_apply, MvPolynomial.sumSMulXSMulY, MvPolynomial.monomial_mul
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := ⋯ }
⊢ Eq (α := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    (c.sum fun (i : n) (a : R) ↦
      (monomial (HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1)) :
          (a : R) → MvPolynomial (n ⊕ n) R)
        a)
    (c.sum fun (a : n) (b : R) ↦
      Finsupp.single (HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl a) 1) (Finsupp.single (Sum.inr a) 1)) b)

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := ⋯ }
⊢ (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c

Tactic:
have aux : sumSMulXSMulY c = c.embDomain ι := by
    rw [← Finsupp.sum_single (Finsupp.embDomain _ _)]
    simp [Finsupp.sum_embDomain, sumSMulXSMulY, X, monomial_mul,
      Finsupp.linearCombination_apply, smul_monomial, ι]
    rfl
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := ⋯ }
aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c
i : n
⊢ Eq.{u_2 + 1} (α := R)
    (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) i)
        ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) :
      R)
    ((c : (a : n) → R) i : R)

Tactic:
simp [aux, coeff, Finsupp.embDomain_apply]

Premises used: Finsupp.embDomain_apply, MvPolynomial.coeff
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := ⋯ }
aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c
⊢ ∀ (i : n),
    Eq.{u_2 + 1} (α := R)
      (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) i)
          ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) :
        R)
      ((c : (a : n) → R) i : R)

Tactic:
have hcoeff (i : n) : coeff (ι i) (sumSMulXSMulY c) = c i := by
    simp [aux, coeff, Finsupp.embDomain_apply]