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
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
pos :
  ∀ (hp : p = 0),
    degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
      degreeOf j p
⊢ degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    degreeOf j p
have neg : ∀ (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
-- 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
hp : ¬p = 0
⊢ degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    degreeOf j p
have neg : (HMul.hMul (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)) (β :=
      Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))
      ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            ((C : (a : R) → MvPolynomial σ R) c)) :
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))
      ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p) :
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))).natDegree =
  Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    ((optionEquivLeft R { b : σ // b ≠ j } :
        (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
      ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
        p))
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
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
⊢ (HMul.hMul (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)) (β :=
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))
        ((optionEquivLeft R { b : σ // b ≠ j } :
              (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
            ((renameEquiv R (optionSubtypeNe j).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
              ((C : (a : R) → MvPolynomial σ R) c)) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))
        ((optionEquivLeft R { b : σ // b ≠ j } :
              (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
            ((renameEquiv R (optionSubtypeNe j).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
              p) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))).natDegree =
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p))
have neg : Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          ((C : (a : R) → MvPolynomial σ R) c))) +
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)) =
  Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    ((optionEquivLeft R { b : σ // b ≠ j } :
        (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
      ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
        p))
Tactic: rw [Polynomial.natDegree_mul']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
⊢ HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            ((C : (a : R) → MvPolynomial σ R) c))))
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p))) ≠
    0
have hp' : Ne (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
  (Polynomial.leadingCoeff
    ((optionEquivLeft R { b : σ // b ≠ j } :
        (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
      ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
          (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
        p)))
  0
Tactic: have hp' : (optionEquivLeft R _ ((rename (optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0 := by
      intro h
      exact hp (rename_injective _ (Equiv.injective _) (by simpa using h))
-- 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
hp : ¬p = 0
hp' :
  Ne (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0
⊢ HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            ((C : (a : R) → MvPolynomial σ R) c))))
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p))) ≠
    0
have neg : ¬HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) (β := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
      ((C : (a : R) → MvPolynomial { b : σ // ¬b = j } R) c : MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
      (Polynomial.leadingCoeff
          ((optionEquivLeft R { b : σ // ¬b = j } :
              (a : MvPolynomial (Option { b : σ // ¬b = j }) R) → Polynomial (MvPolynomial { b : σ // ¬b = j } R))
            ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
              p)) :
        MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) =
    0
Tactic: simp_rw [ne_eq, renameEquiv_apply, algHom_C, algebraMap_eq, optionEquivLeft_C,
      Polynomial.leadingCoeff_C]
-- 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
hp : ¬p = 0
hp' :
  Ne (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0
⊢ ¬HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) (β := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
        ((C : (a : R) → MvPolynomial { b : σ // ¬b = j } R) c : MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
        (Polynomial.leadingCoeff
            ((optionEquivLeft R { b : σ // ¬b = j } :
                (a : MvPolynomial (Option { b : σ // ¬b = j }) R) → Polynomial (MvPolynomial { b : σ // ¬b = j } R))
              ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
                  (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
                p)) :
          MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) =
      0
have neg : ∀
  (hp' :
    HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) (β := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
        ((C : (a : R) → MvPolynomial { b : σ // ¬b = j } R) c : MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
        (Polynomial.leadingCoeff
            ((optionEquivLeft R { b : σ // ¬b = j } :
                (a : MvPolynomial (Option { b : σ // ¬b = j }) R) → Polynomial (MvPolynomial { b : σ // ¬b = j } R))
              ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
                  (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
                p)) :
          MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) =
      0),
  Eq (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0
Tactic: contrapose hp'
Cleared hypotheses: hp'
-- 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
hp : ¬p = 0
hp' :
  HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) (β := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
      ((C : (a : R) → MvPolynomial { b : σ // ¬b = j } R) c : MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
      (Polynomial.leadingCoeff
          ((optionEquivLeft R { b : σ // ¬b = j } :
              (a : MvPolynomial (Option { b : σ // ¬b = j }) R) → Polynomial (MvPolynomial { b : σ // ¬b = j } R))
            ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
              p)) :
        MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) =
    0
⊢ Eq (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0
have neg : ∀ (m : { b : σ // b ≠ j } →₀ ℕ),
  Eq.{u_1 + 1} (α := R)
    (coeff m
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p))))
    (coeff m 0)
Tactic: ext m
-- 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
hp : ¬p = 0
hp' :
  HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) (β := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
      ((C : (a : R) → MvPolynomial { b : σ // ¬b = j } R) c : MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
      (Polynomial.leadingCoeff
          ((optionEquivLeft R { b : σ // ¬b = j } :
              (a : MvPolynomial (Option { b : σ // ¬b = j }) R) → Polynomial (MvPolynomial { b : σ // ¬b = j } R))
            ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
              p)) :
        MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) =
    0
m : { b : σ // b ≠ j } →₀ ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (coeff m
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p))))
    (coeff m 0)
have neg : c *
    coeff m
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p))) =
  0
Tactic: apply hc.1
-- 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
hp : ¬p = 0
⊢ degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    degreeOf j p
have neg : Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    ((optionEquivLeft R { b : σ // b ≠ j } :
        (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
      ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
          (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
        (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p))) =
  Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    ((optionEquivLeft R { b : σ // b ≠ j } :
        (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
      ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
          (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
        p))
Tactic: classical
  simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]
  rw [Polynomial.natDegree_mul']
  · simp
  · have hp' : (optionEquivLeft R _ ((rename (optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0 := by
      intro h
      exact hp (rename_injective _ (Equiv.injective _) (by simpa using h))
    simp_rw [ne_eq, renameEquiv_apply, algHom_C, algebraMap_eq, optionEquivLeft_C,
      Polynomial.leadingCoeff_C]
    contrapose hp'
    ext m
    apply hc.1
    simpa using congr_arg (coeff m) hp'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ (monomial n : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial n : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
have rw : (monomial n : (a : R) → MvPolynomial σ R) a =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial n : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
Tactic: rw [mul_comm, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
rw :
  (monomial n : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial n : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
⊢ (monomial n : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial n : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
have rw₁ : Eq (α := MvPolynomial σ R) ((monomial n : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((monomial n : (a : R) → MvPolynomial σ R) (a * 1) : MvPolynomial σ R)
Tactic: rw [mul_comm, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
rw :
  (monomial n : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial n : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R) ((monomial n : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial n : (a : R) → MvPolynomial σ R) (a * 1) : MvPolynomial σ R)
⊢ (monomial n : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial n : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
have rw₂ : Eq (α := MvPolynomial σ R) ((monomial n : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((monomial n : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
Tactic: rw [mul_comm, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) a ↔
    ∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
have rw : (∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R),
    m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) ↔
  ∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
Tactic: rw [show monomial n a = monomial n 1 * C a by rw [mul_comm, C_mul_monomial, mul_one],
    dvd_monomial_mul_iff_exists]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ (∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R),
      m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) ↔
    ∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
have h : ∀ (a_1 : σ →₀ ℕ),
  (∃ (r : MvPolynomial σ R),
      a_1 ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial a_1 : (a : R) → MvPolynomial σ R) 1 * r) ↔
    ∃ (b : R), a_1 ≤ n ∧ b ∣ a ∧ p = (monomial a_1 : (a : R) → MvPolynomial σ R) b
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
⊢ (∃ (r : MvPolynomial σ R),
      m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) ↔
    ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
have h : (∃ (r : MvPolynomial σ R),
    m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) →
  ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (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 : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
h :
  (∃ (r : MvPolynomial σ R),
      m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) →
    ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
⊢ (∃ (r : MvPolynomial σ R),
      m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) ↔
    ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
have h₁ : (∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b) →
  ∃ (r : MvPolynomial σ R),
    m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hr : r ∣ (C : (a : R) → MvPolynomial σ R) a
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
have hr₁ : ∃ (b : R), b ∣ a ∧ r = (C : (a : R) → MvPolynomial σ R) b
Tactic: rw [dvd_C_iff_exists ha] at hr
Cleared hypotheses: hr, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hr : ∃ (b : R), b ∣ a ∧ r = (C : (a : R) → MvPolynomial σ R) b
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
have h₁ : ∀ (b : R) (hb : b ∣ a) (hr : r = (C : (a : R) → MvPolynomial σ R) b),
  ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
Tactic: obtain ⟨b, hb, hr⟩ := hr
Cleared hypotheses: hr