awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
H_1 : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
e : Polynomial (MvPolynomial.{u_1, u_2} { b : σ // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R { b : σ // b ≠ i })) (renameEquiv R (Equiv.optionSubtypeNe i))
H :
  ∀ (i_1 : { b : σ // ¬b = i } →₀ ℕ),
    IsNilpotent.{u_2} (R := R)
      (coeff i_1
        (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // ¬b = i } R)) P)
          ((n : (a : σ) → ℕ) i)))
h :
  coeff (Finsupp.equivMapDomain (Equiv.optionSubtypeNe i).symm n)
      ((Equiv.symm
            (MulEquiv.toEquiv (RingEquiv.toMulEquiv (AlgEquiv.toRingEquiv (renameEquiv R (Equiv.optionSubtypeNe i))))) :
          (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ i }) R)
        P) =
    coeff n P
⊢ coeff (Finsupp.equivMapDomain (Equiv.optionSubtypeNe i).symm n).some
      (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // ¬b = i } R)) P)
        ((n : (a : σ) → ℕ) i)) =
    coeff n P

Tactic:
refine (optionEquivLeft_coeff_some_coeff_none _ _ _ _).trans ?_

Premises used: MvPolynomial.optionEquivLeft_coeff_some_coeff_none, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
H_1 : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
e : Polynomial (MvPolynomial.{u_1, u_2} { b : σ // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R { b : σ // b ≠ i })) (renameEquiv R (Equiv.optionSubtypeNe i))
H :
  ∀ (i_1 : { b : σ // ¬b = i } →₀ ℕ),
    IsNilpotent.{u_2} (R := R)
      (coeff i_1
        (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // ¬b = i } R)) P)
          ((n : (a : σ) → ℕ) i)))
⊢ coeff (Finsupp.equivMapDomain (Equiv.optionSubtypeNe i).symm n)
      ((Equiv.symm
            (MulEquiv.toEquiv (RingEquiv.toMulEquiv (AlgEquiv.toRingEquiv (renameEquiv R (Equiv.optionSubtypeNe i))))) :
          (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ i }) R)
        P) =
    coeff n P

Tactic:
simp [Finsupp.equivMapDomain_eq_mapDomain,
      coeff_rename_mapDomain _ (Equiv.optionSubtypeNe i).symm.injective]

Premises used: MvPolynomial.coeff_rename_mapDomain, Finsupp.equivMapDomain_eq_mapDomain, Equiv.optionSubtypeNe, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
h : IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
h₁ : IsUnit (coeff 0 P)
h₂ : ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
⊢ IsNilpotent (HSub.hSub (β := MvPolynomial σ R) P ((C : (a : R) → MvPolynomial σ R) (coeff 0 P) : MvPolynomial σ R))

Tactic:
simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂]

Premises used: apply_ite, MvPolynomial.isNilpotent_iff, eq_comm
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
h : IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
h₁ : IsUnit (coeff 0 P)
h₂ : ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
⊢ IsNilpotent (HSub.hSub (β := MvPolynomial σ R) P ((C : (a : R) → MvPolynomial σ R) (coeff 0 P) : MvPolynomial σ R))

Tactic:
have : IsNilpotent (P - C (P.coeff 0)) := by
      simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂]
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
h : IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
h₁ : IsUnit (coeff 0 P)
h₂ : ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
this :
  IsNilpotent (HSub.hSub (β := MvPolynomial σ R) P ((C : (a : R) → MvPolynomial σ R) (coeff 0 P) : MvPolynomial σ R))
⊢ IsUnit P

Tactic:
simpa using this.isUnit_add_right_of_commute (h₁.map C) (.all _ _)

Premises used: IsUnit.map, IsNilpotent.isUnit_add_right_of_commute, Commute.all, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
refine_1 : ∀ (H : IsUnit P) (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
refine_2 refine_2₁ :
  (IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)) →
    ∀ (h₁ : IsUnit (coeff 0 P)) (h₂ : ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)), IsUnit P
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)

Tactic:
classical
  refine ⟨fun H ↦ ⟨H.map constantCoeff, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  · intro n hn
    obtain ⟨i, hi⟩ : ∃ i, n i ≠ 0 := by simpa [Finsupp.ext_iff] using hn
    let e := (optionEquivLeft _ _).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
    have H := (Polynomial.coeff_isUnit_isNilpotent_of_isUnit (H.map e.symm)).2 (n i) hi
    simp only [ne_eq, isNilpotent_iff] at H
    convert! ← H (n.equivMapDomain (Equiv.optionSubtypeNe i).symm).some
    refine (optionEquivLeft_coeff_some_coeff_none _ _ _ _).trans ?_
    simp [Finsupp.equivMapDomain_eq_mapDomain,
      coeff_rename_mapDomain _ (Equiv.optionSubtypeNe i).symm.injective]
  · have : IsNilpotent (P - C (P.coeff 0)) := by
      simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂]
    simpa using this.isUnit_add_right_of_commute (h₁.map C) (.all _ _)

Premises used: MvPolynomial.isNilpotent_iff, ne_eq, Finsupp.equivMapDomain_eq_mapDomain, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
⊢ ∀ (a : R), IsUnit (M := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) → IsUnit a

Tactic:
simp +contextual [isUnit_iff, coeff_C]

Premises used: MvPolynomial.coeff_C, MvPolynomial.isUnit_iff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
⊢ ∀ (a : R), IsUnit (M := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) → IsUnit a

Tactic:
classical simp +contextual [isUnit_iff, coeff_C]

Premises used: MvPolynomial.coeff_C, MvPolynomial.isUnit_iff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
⊢ IsLocalHom (R := R) (S := MvPolynomial σ R) (F := R →+* MvPolynomial σ R) (algebraMap R (MvPolynomial σ R))

Tactic:
inferInstanceAs (IsLocalHom C)

Premises used: _private.0.MvPolynomial.instIsLocalHomRingHomAlgebraMap._proof_1
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)

Tactic:
isUnit_iff (P := P)

Premises used: MvPolynomial.isUnit_iff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
h : P.totalDegree = 0 ↔ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ P.totalDegree = 0

Tactic:
convert! isUnit_iff (P := P)

Premises used: MvPolynomial.isUnit_iff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
h :
  (∀ m ∈ P.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)) ↔
    ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
⊢ P.totalDegree = 0 ↔ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)

Tactic:
rw [totalDegree_eq_zero_iff]

Premises used: MvPolynomial.totalDegree_eq_zero_iff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
⊢ (∀ m ∈ P.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)) ↔
    ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)

Tactic:
simp [not_imp_comm (a := _ = (0 : R)), Finsupp.ext_iff]

Premises used: not_imp_comm, Finsupp.ext_iff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
rw :
  IsUnit (coeff 0 P) ∧ P = (C : (a : R) → MvPolynomial σ R) (coeff 0 P) ↔
    ∃ (r : R), IsUnit r ∧ P = (C : (a : R) → MvPolynomial σ R) r
⊢ IsUnit P ↔ ∃ (r : R), IsUnit r ∧ P = (C : (a : R) → MvPolynomial σ R) r

Tactic:
rw [isUnit_iff_totalDegree_of_isReduced, totalDegree_eq_zero_iff_eq_C]

Premises used: MvPolynomial.isUnit_iff_totalDegree_of_isReduced, MvPolynomial.totalDegree_eq_zero_iff_eq_C
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
⊢ IsUnit (coeff 0 P) ∧ P = (C : (a : R) → MvPolynomial σ R) (coeff 0 P) ↔
    ∃ (r : R), IsUnit r ∧ P = (C : (a : R) → MvPolynomial σ R) r

Tactic:
⟨fun H ↦ ⟨_, H⟩, ?_⟩

Premises used: MvPolynomial.coeff, Iff.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
refine :
  (∃ (r : R), IsUnit r ∧ P = (C : (a : R) → MvPolynomial σ R) r) →
    IsUnit (coeff 0 P) ∧ P = (C : (a : R) → MvPolynomial σ R) (coeff 0 P)
⊢ IsUnit (coeff 0 P) ∧ P = (C : (a : R) → MvPolynomial σ R) (coeff 0 P) ↔
    ∃ (r : R), IsUnit r ∧ P = (C : (a : R) → MvPolynomial σ R) r

Tactic:
refine ⟨fun H ↦ ⟨_, H⟩, ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsReduced R
r : R
hr : IsUnit r
⊢ IsUnit.{u_2} (M := R) (coeff.{u_2, u_1} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) r)) ∧
    Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (coeff.{u_2, u_1} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) r)) :
        MvPolynomial σ R)

Tactic:
simpa
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
simp_rw :
  (HMul.hMul (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)) (β :=
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
        ((optionEquivLeft R { b : σ // b ≠ n } :
              (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
            ((renameEquiv R (optionSubtypeNe n).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
              p) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
        ((optionEquivLeft R { b : σ // b ≠ n } :
              (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
            ((renameEquiv R (optionSubtypeNe n).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
              q) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))).natDegree =
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
        ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((renameEquiv R (optionSubtypeNe n).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            p)) +
      Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
        ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((renameEquiv R (optionSubtypeNe n).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            q))
⊢ degreeOf n (p * q) = degreeOf n p + degreeOf n q

Tactic:
simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]

Premises used: MvPolynomial.renameEquiv_apply, map_mul, MvPolynomial.degreeOf_eq_natDegree
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
hp₁ :
  Ne (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
    ((optionEquivLeft R { b : σ // b ≠ n } :
          (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
        ((renameEquiv R (optionSubtypeNe n).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
          p) :
      Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
    (0 : Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
hq₁ :
  Ne (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
    ((optionEquivLeft R { b : σ // b ≠ n } :
          (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
        ((renameEquiv R (optionSubtypeNe n).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
          q) :
      Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
    (0 : Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
⊢ (HMul.hMul (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)) (β :=
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
        ((optionEquivLeft R { b : σ // b ≠ n } :
              (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
            ((renameEquiv R (optionSubtypeNe n).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
              p) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
        ((optionEquivLeft R { b : σ // b ≠ n } :
              (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
            ((renameEquiv R (optionSubtypeNe n).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
              q) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))).natDegree =
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
        ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((renameEquiv R (optionSubtypeNe n).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            p)) +
      Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R)
        ((optionEquivLeft R { b : σ // b ≠ n } :
            (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
          ((renameEquiv R (optionSubtypeNe n).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
            q))

Tactic:
rw [Polynomial.natDegree_mul]

Premises used: Polynomial.natDegree_mul
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ Ne (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
    ((optionEquivLeft R { b : σ // b ≠ n } :
          (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
        ((renameEquiv R (optionSubtypeNe n).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
          p) :
      Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
    (0 : Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))

Tactic:
simpa [-renameEquiv_apply, EmbeddingLike.map_eq_zero_iff]

Premises used: MvPolynomial.renameEquiv_apply, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ Ne (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
    ((optionEquivLeft R { b : σ // b ≠ n } :
          (a : MvPolynomial (Option { b : σ // b ≠ n }) R) → Polynomial (MvPolynomial { b : σ // b ≠ n } R))
        ((renameEquiv R (optionSubtypeNe n).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
          q) :
      Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))
    (0 : Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ n } R))

Tactic:
simpa [-renameEquiv_apply, EmbeddingLike.map_eq_zero_iff]

Premises used: MvPolynomial.renameEquiv_apply, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
inl :
  ∀ (nontrivial : Subsingleton (MvPolynomial σ R)),
    degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
inr :
  ∀ (nontrivial : Nontrivial (MvPolynomial σ R)),
    degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

Tactic:
rcases subsingleton_or_nontrivial (MvPolynomial σ R) with nontrivial | nontrivial

Premises used: subsingleton_or_nontrivial, MvPolynomial
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
nontrivial : Subsingleton (MvPolynomial σ R)
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

Tactic:
simp [Subsingleton.eq_zero]

Premises used: Subsingleton.eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ 0
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, degreeOf n (f i)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : ∀ (h : ∀ i ∈ s, f i ≠ 0), degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
h : ∀ i ∈ insert a s, f i ≠ 0
⊢ ¬f a = 0 ∧ ∀ a ∈ s, ¬f a = 0

Tactic:
simp only [mem_insert, ne_eq, forall_eq_or_imp] at h

Premises used: Finset.mem_insert, forall_eq_or_imp, ne_eq
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : ∀ (h : ∀ i ∈ s, f i ≠ 0), degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
h : ¬f a = 0 ∧ ∀ a ∈ s, ¬f a = 0
⊢ ¬f a = 0

Tactic:
obtain ⟨ha, hs⟩ := h
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : ∀ (h : ∀ i ∈ s, f i ≠ 0), degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
h : ¬f a = 0 ∧ ∀ a ∈ s, ¬f a = 0
ha : ¬f a = 0
⊢ ∀ a ∈ s, ¬f a = 0

Tactic:
obtain ⟨ha, hs⟩ := h
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : ∀ (h : ∀ i ∈ s, f i ≠ 0), degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
rw : ∀ a ∈ s, f a ≠ 0
rw₁ : Type u_3
rw₂ : ι → MvPolynomial σ R
rw₃ : Finset ι
⊢ Ne (α := MvPolynomial σ R) (∏ x ∈ s, f x) 0

Tactic:
rw [prod_ne_zero_iff]

Premises used: Finset.prod_ne_zero_iff
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : ∀ (h : ∀ i ∈ s, f i ≠ 0), degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ ∀ a ∈ s, f a ≠ 0

Tactic:
hs
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : ∀ (h : ∀ i ∈ s, f i ≠ 0), degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, degreeOf n (f i)

Tactic:
simp [a_not_mem, not_false_eq_true, prod_insert, sum_insert, degreeOf_mul_eq ha
        (by rw [prod_ne_zero_iff]; exact hs), ih hs]

Premises used: Finset.prod_insert, MvPolynomial.degreeOf_mul_eq, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
nontrivial : Nontrivial (MvPolynomial σ R)
inr :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ 0),
    degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, degreeOf n (f i)
inr₁ :
  ∀ (a : ι) (s : Finset ι) (a_not_mem : a ∉ s)
    (ih : ∀ (h : ∀ i ∈ s, f i ≠ 0), degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i))
    (h : ∀ i ∈ insert a s, f i ≠ 0),
    degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, degreeOf n (f i)
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

Tactic:
induction s using Finset.induction_on with
    | empty => simp
    | insert a s a_not_mem ih =>
      simp only [mem_insert, ne_eq, forall_eq_or_imp] at h
      obtain ⟨ha, hs⟩ := h
      simp [a_not_mem, not_false_eq_true, prod_insert, sum_insert, degreeOf_mul_eq ha
        (by rw [prod_ne_zero_iff]; exact hs), ih hs]

Premises used: Finset.prod_insert, Insert.insert, Finset.mem_insert, forall_eq_or_imp, ne_eq, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
n : σ
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
nontrivial : Nontrivial (MvPolynomial σ R)
inr :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ 0),
    degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, degreeOf n (f i)
inr₁ :
  ∀ (a : ι) (s : Finset ι) (a_not_mem : a ∉ s)
    (ih : ∀ (h : ∀ i ∈ s, f i ≠ 0), degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i))
    (h : ∀ i ∈ insert a s, f i ≠ 0),
    degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, degreeOf n (f i)
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

Tactic:
classical
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s a_not_mem ih =>
      simp only [mem_insert, ne_eq, forall_eq_or_imp] at h
      obtain ⟨ha, hs⟩ := h
      simp [a_not_mem, not_false_eq_true, prod_insert, sum_insert, degreeOf_mul_eq ha
        (by rw [prod_ne_zero_iff]; exact hs), ih hs]

Premises used: Finset.prod_insert, Insert.insert, Finset.mem_insert, forall_eq_or_imp, ne_eq, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
rw : ∑ i_1 ∈ range n, degreeOf i p = n * degreeOf i p
⊢ degreeOf i (p ^ n) = n * degreeOf i p

Tactic:
rw [pow_eq_prod_const, degreeOf_prod_eq (range n) (fun _ ↦ p) (fun _ _ ↦ hp)]

Premises used: Finset.range, MvPolynomial.degreeOf_prod_eq, Finset.pow_eq_prod_const