awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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
⊢ degreeOf n (p * q) = degreeOf n p + degreeOf n q
have 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))
Tactic: simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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
⊢ (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))
have 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))
Tactic: rw [Polynomial.natDegree_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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))
⊢ (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))
have 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))
Tactic: rw [Polynomial.natDegree_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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
⊢ degreeOf n (p * q) = degreeOf n p + degreeOf n q
have simp_rw : 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))
      ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
          (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
        (p * q))) =
  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))
        ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
            (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))
        ((rename (⇑(optionSubtypeNe n).symm : (a : σ) → Option { b : σ // b ≠ n }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ n }) R)
          q))
Tactic: classical
  simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]
  rw [Polynomial.natDegree_mul] <;> simpa [-renameEquiv_apply, EmbeddingLike.map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
have inl : ∀ (nontrivial : Subsingleton (MvPolynomial σ R)),
  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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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)
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
have inr : ∀ (nontrivial : Nontrivial (MvPolynomial σ R)),
  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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (hypothesis)
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
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, degreeOf n (f i)
have h₁ : ¬f a = 0 ∧ ∀ a ∈ s, ¬f a = 0
Tactic: simp only [mem_insert, ne_eq, forall_eq_or_imp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (hypothesis)
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
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, degreeOf n (f i)
have ha : ¬f a = 0
Tactic: obtain ⟨ha, hs⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (hypothesis)
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
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, degreeOf n (f i)
have hs : ∀ a ∈ s, ¬f a = 0
Tactic: obtain ⟨ha, hs⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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
⊢ Ne (α := MvPolynomial σ R) (∏ x ∈ s, f x) 0
have rw : ∀ a ∈ s, f a ≠ 0
Tactic: rw [prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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)
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
have 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)
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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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)
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
have 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)
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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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)
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
have 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)
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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
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)
⊢ degreeOf.{u_1, u_2} (R := R) n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
have 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)
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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
⊢ degreeOf i (p ^ n) = n * degreeOf i p
have rw : ∑ i_1 ∈ range n, degreeOf i p = n * degreeOf i p
Tactic: rw [pow_eq_prod_const, degreeOf_prod_eq (range n) (fun _ ↦ p) (fun _ _ ↦ hp)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).degrees = p.degrees + q.degrees
have a : ∀ (s : σ), Multiset.count s (p * q).degrees = Multiset.count s (p.degrees + q.degrees)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
s : σ
⊢ Multiset.count s (p * q).degrees = Multiset.count s (p.degrees + q.degrees)
have a : Multiset.count s (p * q).degrees = Multiset.count s p.degrees + Multiset.count s q.degrees
Tactic: simp_rw [Multiset.count_add, ← degreeOf_def, degreeOf_mul_eq hp hq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
s : σ
a : Multiset.count s (p * q).degrees = Multiset.count s p.degrees + Multiset.count s q.degrees
⊢ Multiset.count s (p * q).degrees = Multiset.count s (p.degrees + q.degrees)
have a₁ : degreeOf s (p * q) = degreeOf s p + degreeOf s q
Tactic: simp_rw [Multiset.count_add, ← degreeOf_def, degreeOf_mul_eq hp hq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).degrees = p.degrees + q.degrees
have a : ∀ (s : σ), Multiset.count s (p * q).degrees = Multiset.count s (p.degrees + q.degrees)
Tactic: classical
  ext s
  simp_rw [Multiset.count_add, ← degreeOf_def, degreeOf_mul_eq hp hq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ (f * g).totalDegree = f.totalDegree + g.totalDegree
have intro : ∀ (w : LinearOrder σ), WellFoundedGT σ → (f * g).totalDegree = f.totalDegree + g.totalDegree
Tactic: cases exists_wellFoundedGT σ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
h : f ∣ g
hg : g ≠ 0
⊢ f.totalDegree ≤ g.totalDegree
have obtain : ∀ (r : MvPolynomial σ R) (hg : f * r ≠ 0), f.totalDegree ≤ (f * r).totalDegree
Tactic: obtain ⟨r, rfl⟩ := h
Cleared hypotheses: g, h, hg
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ f.totalDegree ≤ (f * r).totalDegree
have rw : f.totalDegree ≤ f.totalDegree + r.totalDegree
Tactic: rw [totalDegree_mul_of_isDomain (by aesop) (by aesop)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
⊢ f ∣ (C : (a : R) → MvPolynomial σ R) a ↔ ∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b
have mp : f ∣ (C : (a : R) → MvPolynomial σ R) a → ∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
mp : f ∣ (C : (a : R) → MvPolynomial σ R) a → ∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b
⊢ f ∣ (C : (a : R) → MvPolynomial σ R) a ↔ ∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b
have mpr : (∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b) → f ∣ (C : (a : R) → MvPolynomial σ R) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
⊢ ∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b
have h : coeff 0 f ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
Tactic: use coeff 0 f
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
this : f.totalDegree = 0
⊢ coeff 0 f ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
have this₁ : f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
Tactic: rw [totalDegree_eq_zero_iff_eq_C] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
this : f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
⊢ coeff 0 f ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
have refine : coeff 0 f ∣ a
Tactic: refine ⟨?_, this⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
this : f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
⊢ coeff 0 f ∣ a
have hf₁ : ∀ (i : σ →₀ ℕ), coeff 0 f ∣ coeff i ((C : (a : R) → MvPolynomial σ R) a)
Tactic: rw [this, C_dvd_iff_dvd_coeff] at hf
Cleared hypotheses: hf, this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
⊢ coeff 0 f ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
have h : f.totalDegree = 0
Tactic: suffices f.totalDegree = 0 by
      rw [totalDegree_eq_zero_iff_eq_C] at this
      refine ⟨?_, this⟩
      rw [this, C_dvd_iff_dvd_coeff] at hf
      simpa using hf 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
⊢ f.totalDegree = 0
have h : f.totalDegree ≤ 0
Tactic: apply Nat.eq_zero_of_le_zero
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
⊢ degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    degreeOf j p
have pos : ∀ (hp : p = 0),
  degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    degreeOf j p
Tactic: by_cases hp : p = 0