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
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)
⊢ Membership.mem (γ := Finset (n →₀ ℕ)) (support.{u_2, u_1} (R := R) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c))
    (Finsupp.single i 1)
have rwa : Ne.{u_2 + 1} (α := R) (coeff (Finsupp.single i 1) ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)) 0
Tactic: rwa [mem_support_iff, coeff_sumSMulX]
-- 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 : Ne.{u_2 + 1} (α := R) ((c : (a : n) → R) i : R) (0 : R)
⊢ False
have h₁ : Eq (α := ℕ) ((Finsupp.single i 1 : (a : n) → ℕ) i : ℕ) (0 : ℕ)
Tactic: specialize h (Finsupp.single i 1) (by
        rwa [mem_support_iff, coeff_sumSMulX]) i
Cleared hypotheses: h
-- 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
r : R
hr : ∀ (i : n →₀ ℕ), r ∣ coeff i ((sumSMulX : (a : n →₀ R) → MvPolynomial n R) c)
⊢ IsUnit r
have hp' : ∀ (i : n), r ∣ (c : (a : n) → R) i
Tactic: apply hc_gcd
-- 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 : 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
have 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)
Tactic: rw [← Finsupp.sum_single (Finsupp.embDomain _ _)]
-- 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 : 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)
    ((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)
have 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)
Tactic: simp [Finsupp.sum_embDomain, sumSMulXSMulY, X, monomial_mul,
      Finsupp.linearCombination_apply, smul_monomial, ι]
-- 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 : 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' := ⋯ }
⊢ Irreducible (M := 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)
have aux : (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
-- 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 : 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
⊢ Irreducible (M := 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)
have hcoeff : ∀ (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]
-- 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 : 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
hcoeff :
  ∀ (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)
⊢ support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
have rw : support (Finsupp.embDomain ι c) = Finset.map ι c.support
Tactic: rw [aux, support, Finsupp.support_embDomain]
-- 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 : 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
hcoeff :
  ∀ (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)
rw : support (Finsupp.embDomain ι c) = Finset.map ι c.support
⊢ support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
have rw₁ : (Finsupp.embDomain ι c).support = Finset.map ι c.support
Tactic: rw [aux, support, Finsupp.support_embDomain]
-- 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 : 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
hcoeff :
  ∀ (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)
rw : support (Finsupp.embDomain ι c) = Finset.map ι c.support
rw₁ : (Finsupp.embDomain ι c).support = Finset.map ι c.support
⊢ support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
have rw₂ : Finset.map ι c.support = Finset.map ι c.support
Tactic: rw [aux, support, Finsupp.support_embDomain]
-- 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 : 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
hcoeff :
  ∀ (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)
⊢ Irreducible (M := 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)
have hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
Tactic: have hsupp : (sumSMulXSMulY c).support = c.support.map ι := by
    rw [aux, support, Finsupp.support_embDomain]
-- 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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
⊢ Irreducible (M := 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)
have obtain : ∀ (a : n) (ha : a ∈ c.support),
  Irreducible (M := 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)
Tactic: obtain ⟨a, ha⟩ := hc.nonempty
-- 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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ Irreducible (M := 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)
have nontrivial : Finset.Nontrivial.{u_1} (α := n ⊕ n →₀ ℕ)
  (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
Tactic: apply irreducible_of_disjoint_support (d := ι a) (i := .inl a)
-- 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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
nontrivial :
  Finset.Nontrivial.{u_1} (α := n ⊕ n →₀ ℕ)
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
⊢ Irreducible (M := 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)
have hd : Membership.mem (α := n ⊕ n →₀ ℕ) (γ := Finset (n ⊕ n →₀ ℕ))
  (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
  ((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ)
Tactic: apply irreducible_of_disjoint_support (d := ι a) (i := .inl a)
-- 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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
nontrivial :
  Finset.Nontrivial.{u_1} (α := n ⊕ n →₀ ℕ)
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
hd :
  Membership.mem (α := n ⊕ n →₀ ℕ) (γ := Finset (n ⊕ n →₀ ℕ))
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
    ((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ)
⊢ Irreducible (M := 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)
have hdi : Eq (α := ℕ) ((((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ) : (a : n ⊕ n) → ℕ) (Sum.inl a) : ℕ) (1 : ℕ)
Tactic: apply irreducible_of_disjoint_support (d := ι a) (i := .inl a)
-- 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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
nontrivial :
  Finset.Nontrivial.{u_1} (α := n ⊕ n →₀ ℕ)
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
hd :
  Membership.mem (α := n ⊕ n →₀ ℕ) (γ := Finset (n ⊕ n →₀ ℕ))
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
    ((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ)
hdi : Eq (α := ℕ) ((((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ) : (a : n ⊕ n) → ℕ) (Sum.inl a) : ℕ) (1 : ℕ)
⊢ Irreducible (M := 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)
have disjoint : (↑(support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c)) :
      Set (n ⊕ n →₀ ℕ)).PairwiseDisjoint
  Finsupp.support
Tactic: apply irreducible_of_disjoint_support (d := ι a) (i := .inl a)
-- 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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
nontrivial :
  Finset.Nontrivial.{u_1} (α := n ⊕ n →₀ ℕ)
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
hd :
  Membership.mem (α := n ⊕ n →₀ ℕ) (γ := Finset (n ⊕ n →₀ ℕ))
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
    ((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ)
hdi : Eq (α := ℕ) ((((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ) : (a : n ⊕ n) → ℕ) (Sum.inl a) : ℕ) (1 : ℕ)
disjoint :
  (↑(support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c)) :
        Set (n ⊕ n →₀ ℕ)).PairwiseDisjoint
    Finsupp.support
⊢ Irreducible (M := 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)
have isPrimitive : ∀ (r : R), (∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c)) → IsUnit r
Tactic: apply irreducible_of_disjoint_support (d := ι a) (i := .inl a)
-- 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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ Finset.Nontrivial.{u_1} (α := n ⊕ n →₀ ℕ)
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
have nontrivial : (Finset.map ι c.support).Nontrivial
Tactic: rwa [hsupp, Finset.map_nontrivial]
-- 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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ Membership.mem (α := n ⊕ n →₀ ℕ) (γ := Finset (n ⊕ n →₀ ℕ))
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
    ((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ)
have hd : Ne.{u_2 + 1} (α := R)
  (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) a)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
  0
Tactic: rwa [MvPolynomial.mem_support_iff, hcoeff, ← Finsupp.mem_support_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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
hd :
  Ne.{u_2 + 1} (α := R)
    (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) a)
      ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
    0
⊢ Membership.mem (α := n ⊕ n →₀ ℕ) (γ := Finset (n ⊕ n →₀ ℕ))
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
    ((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ)
have hd₁ : Ne.{u_2 + 1} (α := R) ((c : (a : n) → R) a : R) (0 : R)
Tactic: rwa [MvPolynomial.mem_support_iff, hcoeff, ← Finsupp.mem_support_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 : 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
hcoeff :
  ∀ (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)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (↑(support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c)) :
        Set (n ⊕ n →₀ ℕ)).PairwiseDisjoint
    Finsupp.support
have disjoint : (↑c.support : Set n).PairwiseDisjoint (α := Finset (n ⊕ n))
  (Function.comp (β := n ⊕ n →₀ ℕ) Finsupp.support (⇑ι : (a : n) → n ⊕ n →₀ ℕ))
Tactic: rw [hsupp, Finset.coe_map, ι.injective.injOn.pairwiseDisjoint_image]