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
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
⊢ p = b * a
have rw₁ : b * a = b * a
Tactic: rw [hab, mul_comm]
-- 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
hle : a.totalDegree ≤ b.totalDegree
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a, hab, hle
-- 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
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
⊢ IsUnit a ∨ IsUnit b
have inr : ∀ (ha₀ : a ≠ 0), IsUnit a ∨ IsUnit b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- 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
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: obtain rfl | hb₀ := eq_or_ne b 0
Cleared hypotheses: b, hab, hle
-- 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
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
⊢ IsUnit a ∨ IsUnit b
have inr₁ : ∀ (hb₀ : b ≠ 0), IsUnit a ∨ IsUnit b
Tactic: obtain rfl | hb₀ := eq_or_ne b 0
-- 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
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
⊢ IsUnit a ∨ IsUnit b
have this : 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
-- 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
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
hb₀ : b ≠ 0
this : a.totalDegree + b.totalDegree = 1
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: obtain ⟨r, rfl⟩ : ∃ r, a = C r := ⟨_, (totalDegree_eq_zero_iff_eq_C (p := a)).mp (by lia)⟩
Cleared hypotheses: a, hab, hle, ha₀, this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i : n
⊢ 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)
have 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)
Tactic: rw [sumSMulX, Finsupp.linearCombination_apply, Finsupp.sum, coeff_sum]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i : n
⊢ 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)
have 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
Tactic: rw [Finset.sum_eq_single i _ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ 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)
have 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
Tactic: rw [Finset.sum_eq_single i _ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) j : R) (X j)) = 0
have rw : HSMul.hSMul (α := R) (β := R) ((c : (a : n) → R) j : R) 0 = 0
Tactic: rw [coeff_smul, coeff_X', if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ coeff (Finsupp.single i 1) (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) j : R) (X j)) = 0
have hnc : ¬Eq (α := n →₀ ℕ) (Finsupp.single j 1) (Finsupp.single i 1)
Tactic: rw [coeff_smul, coeff_X', if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ ¬Eq (α := n →₀ ℕ) (Finsupp.single j 1) (Finsupp.single i 1)
have hnc : ¬j = i
Tactic: rwa [Finsupp.single_left_inj Nat.one_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
i : n
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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)
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ 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)
have rw₁₀ : ∀ (j : n) (hj : j ∈ c.support) (hji : j ≠ i), HSMul.hSMul (α := R) (β := R) ((c : (a : n) → R) j : R) 0 = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ 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)
have hnc : ∀ (j : n) (hj : j ∈ c.support) (hji : j ≠ i), ¬Eq (α := n →₀ ℕ) (Finsupp.single j 1) (Finsupp.single i 1)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ Irreducible (M := MvPolynomial n R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c : MvPolynomial n R)
have hp : totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) = 1
Tactic: apply irreducible_of_totalDegree_eq_one
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ Irreducible (M := MvPolynomial n R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c : MvPolynomial n R)
have hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)) → IsUnit x
Tactic: apply irreducible_of_totalDegree_eq_one
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) = 1
have hp : totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) = 1
have hp₁ : 1 ≤ totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c) ≤ 1
have 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
Tactic: simp only [sumSMulX, Finsupp.linearCombination_apply, Finsupp.sum]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ 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
have hp : ∀ i ∈ c.support, (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) i : R) (X i)).totalDegree ≤ 1
Tactic: apply totalDegree_finsetSum_le
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ (HSMul.hSMul (α := R) (β := MvPolynomial n R) ((c : (a : n) → R) i : R) (X i)).totalDegree ≤ 1
have hp : totalDegree.{u_2, u_1} (R := R) (X i) ≤ 1
Tactic: apply le_trans (totalDegree_smul_le ..)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ 1 ≤ totalDegree.{u_2, u_1} (R := R) (σ := n) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)
have 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 : ℕ)
Tactic: rw [← not_lt, Nat.lt_one_iff, totalDegree_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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 : ℕ)
⊢ False
have hp : ∀ (i : n) (hi : i ∈ c.support), False
Tactic: obtain ⟨i, hi⟩ := hc_nonempty
Cleared hypotheses: hc_nonempty
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (hypothesis)
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
⊢ False
have hi₁ : Ne.{u_2 + 1} (α := R) ((c : (a : n) → R) i : R) (0 : R)
Tactic: simp only [Finsupp.mem_support_iff] at hi
Cleared hypotheses: hi