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 : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
⊢ ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b
have right : p = (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) b
Tactic: use Finsupp.single i 1, le_rfl, hb
-- 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
i : σ
⊢ p ∣ X i ↔
    ∃ (r : R), IsUnit r ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = HSMul.hSMul (β := MvPolynomial σ R) r (X i))
have a : Nontrivial R
Tactic: nontriviality R
-- 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
i : σ
h : Nontrivial R
⊢ p ∣ X i ↔
    ∃ (r : R), IsUnit r ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = HSMul.hSMul (β := MvPolynomial σ R) r (X i))
have rw : (∃ (s : R), s ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) s ∨ p = HSMul.hSMul (β := MvPolynomial σ R) s (X i))) ↔
  ∃ (r : R),
    IsUnit r ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = r • HSMul.hSMul (α := R) (β := MvPolynomial σ R) 1 (X i))
Tactic: rw [← one_smul R (X i), dvd_smul_X_iff_exists (one_ne_zero' R)]
-- 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
i : σ
h : Nontrivial R
⊢ (∃ (s : R), s ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) s ∨ p = HSMul.hSMul (β := MvPolynomial σ R) s (X i))) ↔
    ∃ (r : R),
      IsUnit r ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = r • HSMul.hSMul (α := R) (β := MvPolynomial σ R) 1 (X i))
have h : ∀ (a : R),
  a ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) a ∨ p = HSMul.hSMul (β := MvPolynomial σ R) a (X i)) ↔
    IsUnit a ∧ (p = (C : (a : R) → MvPolynomial σ R) a ∨ p = a • HSMul.hSMul (α := R) (β := MvPolynomial σ R) 1 (X i))
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
i : σ
h : Nontrivial R
r : R
⊢ r ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = HSMul.hSMul (β := MvPolynomial σ R) r (X i)) ↔
    IsUnit r ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = r • HSMul.hSMul (α := R) (β := MvPolynomial σ R) 1 (X i))
have h : r ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = HSMul.hSMul (β := MvPolynomial σ R) r (X i)) ↔
  r ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = r • HSMul.hSMul (α := R) (β := MvPolynomial σ R) 1 (X i))
Tactic: rw [isUnit_iff_dvd_one, one_smul]
-- 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
i : σ
h_1 : Nontrivial R
r : R
h :
  r ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = HSMul.hSMul (β := MvPolynomial σ R) r (X i)) ↔
    r ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = r • HSMul.hSMul (α := R) (β := MvPolynomial σ R) 1 (X i))
⊢ r ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = HSMul.hSMul (β := MvPolynomial σ R) r (X i)) ↔
    IsUnit r ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = r • HSMul.hSMul (α := R) (β := MvPolynomial σ R) 1 (X i))
have h₁ : r ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = HSMul.hSMul (β := MvPolynomial σ R) r (X i)) ↔
  r ∣ 1 ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = HSMul.hSMul (β := MvPolynomial σ R) r (X i))
Tactic: rw [isUnit_iff_dvd_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
have simp : Eq (α := MvPolynomial σ R)
  (s.sum fun (a_1 : σ) (b : ℕ) ↦
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
        (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R) :
    MvPolynomial σ R)
  ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
Tactic: simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
    ← (monomial _).map_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R)
    (s.sum fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
have refine_1 : ∀ j ∈ s.support,
  ∀ (hne : j ≠ i),
    Eq (α := MvPolynomial σ R)
      ((fun (a_1 : σ) (b : ℕ) ↦
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
            (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
        j ((s : (a : σ) → ℕ) j))
      0
Tactic: refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
refine_1 :
  ∀ j ∈ s.support,
    ∀ (hne : j ≠ i),
      Eq (α := MvPolynomial σ R)
        ((fun (a_1 : σ) (b : ℕ) ↦
            HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
              ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
              (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
          j ((s : (a : σ) → ℕ) j))
        0
⊢ Eq (α := MvPolynomial σ R)
    (s.sum fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
have refine_2 : ∀ (hi : i ∉ s.support),
  Eq (α := MvPolynomial σ R)
    ((fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
      i ((s : (a : σ) → ℕ) i))
    0
Tactic: refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
refine_1 :
  ∀ j ∈ s.support,
    ∀ (hne : j ≠ i),
      Eq (α := MvPolynomial σ R)
        ((fun (a_1 : σ) (b : ℕ) ↦
            HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
              ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
              (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
          j ((s : (a : σ) → ℕ) j))
        0
refine_2 :
  ∀ (hi : i ∉ s.support),
    Eq (α := MvPolynomial σ R)
      ((fun (a_1 : σ) (b : ℕ) ↦
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
            (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
        i ((s : (a : σ) → ℕ) i))
      0
⊢ Eq (α := MvPolynomial σ R)
    (s.sum fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
have refine_3 : Eq (α := MvPolynomial σ R)
  ((fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
      i ((s : (a : σ) → ℕ) i) :
    MvPolynomial σ R)
  ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
Tactic: refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (hypothesis)
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
hi : i ∉ s.support
⊢ Eq (α := MvPolynomial σ R)
    ((fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
      i ((s : (a : σ) → ℕ) i))
    0
have hi₁ : Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: rw [Finsupp.notMem_support_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
have simp : Eq (α := MvPolynomial σ R)
  (s.sum fun (a_1 : σ) (b : ℕ) ↦
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
        (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R) :
    MvPolynomial σ R)
  ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
Tactic: classical
  simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
    ← (monomial _).map_smul]
  refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
  · simp [Pi.single_eq_of_ne hne]
  · rw [Finsupp.notMem_support_iff] at hi; simp [hi]
  · simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
simp :
  Eq (α := MvPolynomial σ R)
    (s.sum fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
have refine_1 : ∀ j ∈ s.support,
  ∀ (hne : j ≠ i),
    Eq (α := MvPolynomial σ R)
      ((fun (a_1 : σ) (b : ℕ) ↦
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
            (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
        j ((s : (a : σ) → ℕ) j))
      0
Tactic: classical
  simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
    ← (monomial _).map_smul]
  refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
  · simp [Pi.single_eq_of_ne hne]
  · rw [Finsupp.notMem_support_iff] at hi; simp [hi]
  · simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
simp :
  Eq (α := MvPolynomial σ R)
    (s.sum fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
refine_1 :
  ∀ j ∈ s.support,
    ∀ (hne : j ≠ i),
      Eq (α := MvPolynomial σ R)
        ((fun (a_1 : σ) (b : ℕ) ↦
            HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
              ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
              (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
          j ((s : (a : σ) → ℕ) j))
        0
⊢ Eq (α := MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
have refine_2 : ∀ (hi : i ∉ s.support),
  Eq (α := MvPolynomial σ R)
    ((fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
      i ((s : (a : σ) → ℕ) i))
    0
Tactic: classical
  simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
    ← (monomial _).map_smul]
  refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
  · simp [Pi.single_eq_of_ne hne]
  · rw [Finsupp.notMem_support_iff] at hi; simp [hi]
  · simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
simp :
  Eq (α := MvPolynomial σ R)
    (s.sum fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
refine_1 :
  ∀ j ∈ s.support,
    ∀ (hne : j ≠ i),
      Eq (α := MvPolynomial σ R)
        ((fun (a_1 : σ) (b : ℕ) ↦
            HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
              ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
              (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
          j ((s : (a : σ) → ℕ) j))
        0
refine_2 :
  ∀ (hi : i ∉ s.support),
    Eq (α := MvPolynomial σ R)
      ((fun (a_1 : σ) (b : ℕ) ↦
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
            (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
        i ((s : (a : σ) → ℕ) i))
      0
⊢ Eq (α := MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
have refine_3 : Eq (α := MvPolynomial σ R)
  ((fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
      i ((s : (a : σ) → ℕ) i) :
    MvPolynomial σ R)
  ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
Tactic: classical
  simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
    ← (monomial _).map_smul]
  refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
  · simp [Pi.single_eq_of_ne hne]
  · rw [Finsupp.notMem_support_iff] at hi; simp [hi]
  · simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) r) :
        MvPolynomial σ R) =
    HSMul.hSMul (α := ℕ) (β := MvPolynomial σ R) ((m : (a : σ) → ℕ) i : ℕ)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
have rw : Eq (α := MvPolynomial σ R)
  ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑((m : (a : σ) → ℕ) i) : R))) :
    MvPolynomial σ R)
  ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
Tactic: rw [pderiv_monomial, X, monomial_mul, smul_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑((m : (a : σ) → ℕ) i) : R))) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
have pos : ∀ (h : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
  Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑((m : (a : σ) → ℕ) i) : R))) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
Tactic: by_cases h : m i = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
pos :
  ∀ (h : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
    Eq (α := MvPolynomial σ R)
      ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R)
          (1 * (r * (↑((m : (a : σ) → ℕ) i) : R))) :
        MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑((m : (a : σ) → ℕ) i) : R))) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
have neg : ∀ (h : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
  Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑((m : (a : σ) → ℕ) i) : R))) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
Tactic: by_cases h : m i = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑((m : (a : σ) → ℕ) i) : R))) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
have pos : Eq (α := MvPolynomial σ R)
  ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑0 : R))) : MvPolynomial σ R)
  ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) 0 r) : MvPolynomial σ R)
Tactic: simp_rw [h, Nat.cast_zero, mul_zero, zero_smul, monomial_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
pos :
  Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑0 : R))) : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) 0 r) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑((m : (a : σ) → ℕ) i) : R))) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
have pos₁ : Eq (α := MvPolynomial σ R)
  ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * 0)) : MvPolynomial σ R)
  ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) 0 r) : MvPolynomial σ R)
Tactic: simp_rw [h, Nat.cast_zero, mul_zero, zero_smul, monomial_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
pos :
  Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑0 : R))) : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) 0 r) : MvPolynomial σ R)
pos₁ :
  Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * 0)) : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) 0 r) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (1 * (r * (↑((m : (a : σ) → ℕ) i) : R))) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
have pos₂ : Eq (α := MvPolynomial σ R)
  ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) 0 : MvPolynomial σ R)
  ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) 0 r) : MvPolynomial σ R)
Tactic: simp_rw [h, Nat.cast_zero, mul_zero, zero_smul, monomial_zero]