awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
hj : ¬j = i
⊢ LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)

Tactic:
(hmn j).trans (Finsupp.single_eq_of_ne hj).le

Premises used: Finsupp.single_eq_of_ne, Eq.le, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
hj : ¬j = i
⊢ LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)

Tactic:
exact (hmn j).trans (Finsupp.single_eq_of_ne hj).le

Premises used: Finsupp.single_eq_of_ne, Eq.le, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
neg : m = Finsupp.single i 1
⊢ m = 0 ∨ m = Finsupp.single i 1

Tactic:
right
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
neg : ∀ (j : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ)
⊢ m = Finsupp.single i 1

Tactic:
ext j
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
neg : LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)
⊢ Eq (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ)

Tactic:
apply le_antisymm (hmn j)

Premises used: le_antisymm
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
pos : ∀ (hj : j = i), LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)
neg : ∀ (hj : ¬j = i), LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)
⊢ LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)

Tactic:
by_cases hj : j = i
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
hj : j = i
⊢ LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)

Tactic:
simpa [hj, Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
hj : ¬j = i
⊢ LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)

Tactic:
simp [Finsupp.single_eq_of_ne hj]

Premises used: Finsupp.single_eq_of_ne
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
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 = (C : (a : R) → MvPolynomial σ R) b
h : LE.le (α := σ →₀ ℕ) 0 (Finsupp.single i 1) ∧ b ∣ r ∧ p = (monomial 0 : (a : R) → MvPolynomial σ R) b
⊢ ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b

Tactic:
use 0
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
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 = (C : (a : R) → MvPolynomial σ R) b
⊢ LE.le (α := σ →₀ ℕ) 0 (Finsupp.single i 1) ∧ b ∣ r ∧ p = (monomial 0 : (a : R) → MvPolynomial σ R) b

Tactic:
simp [hb, hp]
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
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)
right : p = (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) b
⊢ ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b

Tactic:
use Finsupp.single i 1, le_rfl, hb

Premises used: le_rfl, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
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)
⊢ p = (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) b

Tactic:
simp [hp, smul_monomial]

Premises used: MvPolynomial.smul_monomial
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
h : Nontrivial R
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))
⊢ p ∣ X i ↔
    ∃ (r : R), IsUnit r ∧ (p = (C : (a : R) → MvPolynomial σ R) r ∨ p = HSMul.hSMul (β := MvPolynomial σ R) r (X i))

Tactic:
rw [← one_smul R (X i), dvd_smul_X_iff_exists (one_ne_zero' R)]

Premises used: one_ne_zero', MvPolynomial.X, MvPolynomial.dvd_smul_X_iff_exists, one_smul
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
h_1 : Nontrivial R
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))
⊢ (∃ (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:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
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))
h₁ 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))
⊢ 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))

Tactic:
rw [isUnit_iff_dvd_one, one_smul]

Premises used: one_smul, isUnit_iff_dvd_one
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
⊢ Eq (α := Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (mkDerivation R (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i 1))
    (mkDerivation R (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i 1))

Tactic:
congr!
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
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)

Tactic:
simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
    ← (monomial _).map_smul]

Premises used: MvPolynomial.monomial, smul_mul_assoc, MvPolynomial.pderiv_def, MvPolynomial.mkDerivation_monomial, LinearMap.map_smul, Finsupp.smul_sum, smul_eq_mul
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
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)

Tactic:
(Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_

Premises used: Finsupp.sum, Finset.sum_eq_single, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
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
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)
⊢ 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:
refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_

Premises used: Finset.sum_eq_single, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i j : σ
h : 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:
simp [Pi.single_eq_of_ne hne]

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
hi : i ∉ s.support
⊢ Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
rw [Finsupp.notMem_support_iff] at hi

Premises used: Finsupp.notMem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
hi : Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ 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:
simp [hi]
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
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))
        i ((s : (a : σ) → ℕ) i) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
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)
⊢ 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)

Tactic:
rw [pderiv_monomial, X, monomial_mul, smul_monomial]

Premises used: MvPolynomial.smul_monomial, MvPolynomial.X, MvPolynomial.monomial_mul, MvPolynomial.pderiv_monomial
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
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)
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)
⊢ 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

Premises used: DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
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)
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)
pos₃ :
  Eq (α := MvPolynomial σ R) ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) 0)
    ((monomial m : (a : R) → MvPolynomial σ R) 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:
simp_rw [h, Nat.cast_zero, mul_zero, zero_smul, monomial_zero]

Premises used: MvPolynomial.monomial_zero, MulZeroClass.mul_zero, zero_smul, Nat.cast_zero
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
neg :
  Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) (r * (↑((m : (a : σ) → ℕ) i) : R)) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
neg₁ :
  Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) ((↑((m : (a : σ) → ℕ) i) : R) * r) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) (HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) r) : MvPolynomial σ R)
neg₂ :
  Eq (α := MvPolynomial σ R)
    ((monomial (single i 1 + (m - single i 1)) : (a : R) → MvPolynomial σ R) ((↑((m : (a : σ) → ℕ) i) : R) * r) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) ((↑((m : (a : σ) → ℕ) i) : R) * r) : MvPolynomial σ R)
neg₃ :
  Eq (α := MvPolynomial σ R)
    ((monomial (m - single i 1 + single i 1) : (a : R) → MvPolynomial σ R) ((↑((m : (a : σ) → ℕ) i) : R) * r) :
      MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) ((↑((m : (a : σ) → ℕ) i) : R) * r) : MvPolynomial σ R)
neg₄ neg₅ :
  Eq (α := MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) ((↑((m : (a : σ) → ℕ) i) : R) * r) : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) ((↑((m : (a : σ) → ℕ) i) : R) * 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)

Tactic:
rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]

Premises used: Finsupp.sub_add_single_one_cancel, add_comm, mul_comm, nsmul_eq_mul, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
a : R
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a) : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
derivation_C _ _

Premises used: MvPolynomial.derivation_C
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) 1) 0

Tactic:
pderiv_C

Premises used: MvPolynomial.pderiv_C, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
rw :
  Eq (α := MvPolynomial σ R)
    ((mkDerivation R (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i 1) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (X j) :
      MvPolynomial σ R)
    (Pi.single (M := fun (x : σ) ↦ MvPolynomial σ R) i (1 : (fun (x : σ) ↦ MvPolynomial σ R) i) j : MvPolynomial σ R)
rw₁ rw₂ :
  Eq (α := MvPolynomial σ R)
    (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) j : MvPolynomial σ R)
    (Pi.single (M := fun (x : σ) ↦ MvPolynomial σ R) i (1 : (fun (x : σ) ↦ MvPolynomial σ R) i) j : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (X j) : MvPolynomial σ R)
    (Pi.single (M := fun (x : σ) ↦ MvPolynomial σ R) i (1 : (fun (x : σ) ↦ MvPolynomial σ R) i) j : MvPolynomial σ R)

Tactic:
rw [pderiv_def, mkDerivation_X]

Premises used: MvPolynomial.mkDerivation_X, MvPolynomial.pderiv_def
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    (1 : MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    (1 : MvPolynomial σ R)

Tactic:
classical simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i j : σ
h : j ≠ i
⊢ Eq (α := MvPolynomial σ R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (X j) : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i j : σ
h : j ≠ i
⊢ Eq (α := MvPolynomial σ R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (X j) : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
classical simp [h]
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
f : MvPolynomial σ R
h : i ∉ f.vars
⊢ Eq (α := MvPolynomial σ R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
derivation_eq_zero_of_forall_mem_vars fun _ hj => pderiv_X_of_ne <| ne_of_mem_of_not_mem hj h

Premises used: MvPolynomial.derivation_eq_zero_of_forall_mem_vars, ne_of_mem_of_not_mem, MvPolynomial.pderiv_X_of_ne
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
a : R
inst : CommSemiring R
i : σ
n : ℕ
⊢ Eq (α := MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial (single i n) : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial σ R)
    ((monomial (single i (n - 1)) : (a : R) → MvPolynomial σ R) (a * (↑n : R)) : MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (f * g) =
    HMul.hMul (α := MvPolynomial σ R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) g +
      HMul.hMul (β := MvPolynomial σ R) f ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) g : MvPolynomial σ R)

Tactic:
simp only [(pderiv i).leibniz f g, smul_eq_mul, mul_comm, add_comm]

Premises used: MvPolynomial.pderiv, add_comm, Derivation.leibniz, mul_comm, smul_eq_mul