awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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)
  ((monomial m : (a : R) → MvPolynomial σ R) 0)
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 : ℕ)
⊢ 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 : 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)
Tactic: rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]
-- 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 : ℕ)
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)
⊢ 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₁ : 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)
Tactic: rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]
-- 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 : ℕ)
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)
⊢ 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₂ : 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)
Tactic: rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]
-- 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 : ℕ)
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)
⊢ 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₃ : 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)
Tactic: rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]
-- 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 : ℕ)
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)
⊢ 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₄ : 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)
Tactic: rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
⊢ 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)
have 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)
Tactic: rw [pderiv_def, mkDerivation_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pderiv_def, mkDerivation_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
f : MvPolynomial σ R
n : ℕ
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (f ^ n) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
have rw : n •
    HSMul.hSMul (β := MvPolynomial σ R) (f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
  HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: rw [(pderiv i).leibniz_pow f n, nsmul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
f : MvPolynomial σ R
n : ℕ
rw :
  n •
      HSMul.hSMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (f ^ n) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
have rw₁ : (↑n : MvPolynomial σ R) *
    HSMul.hSMul (β := MvPolynomial σ R) (f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
  HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: rw [(pderiv i).leibniz_pow f n, nsmul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
f : MvPolynomial σ R
n : ℕ
rw :
  n •
      HSMul.hSMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
rw₁ :
  (↑n : MvPolynomial σ R) *
      HSMul.hSMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (f ^ n) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
have rw₂ : (↑n : MvPolynomial σ R) *
    HMul.hMul (β := MvPolynomial σ R) (f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
  HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: rw [(pderiv i).leibniz_pow f n, nsmul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
i : σ
f : MvPolynomial σ R
n : ℕ
rw :
  n •
      HSMul.hSMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
rw₁ :
  (↑n : MvPolynomial σ R) *
      HSMul.hSMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
rw₂ :
  (↑n : MvPolynomial σ R) *
      HMul.hMul (β := MvPolynomial σ R) (f ^ (n - 1))
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (f ^ n) =
    HMul.hMul (β := MvPolynomial σ R) ((↑n : MvPolynomial σ R) * f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
have rw₃ : (↑n : MvPolynomial σ R) *
    HMul.hMul (β := MvPolynomial σ R) (f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
  (↑n : MvPolynomial σ R) *
    HMul.hMul (β := MvPolynomial σ R) (f ^ (n - 1))
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: rw [(pderiv i).leibniz_pow f n, nsmul_eq_mul, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
inst : CommSemiring R
f : MvPolynomial σ R
i : σ
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
have rw : (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (a • f) =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: rw [C_mul', Derivation.map_smul, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
inst : CommSemiring R
f : MvPolynomial σ R
i : σ
rw :
  (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (a • f) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
have rw₁ : HSMul.hSMul (β := MvPolynomial σ R) a ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: rw [C_mul', Derivation.map_smul, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
a : R
inst : CommSemiring R
f : MvPolynomial σ R
i : σ
rw :
  (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (a • f) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
rw₁ :
  HSMul.hSMul (β := MvPolynomial σ R) a ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ (pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
have rw₂ : HSMul.hSMul (β := MvPolynomial σ R) a ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R) =
  HSMul.hSMul (β := MvPolynomial σ R) a ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: rw [C_mul', Derivation.map_smul, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
inst_1 : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
⊢ Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) f) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ S)
have apply : ∀ (p : MvPolynomial σ R) (j : σ)
  (eq :
    Eq (α := MvPolynomial σ S)
      ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
        MvPolynomial σ S)
      ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
        MvPolynomial σ S)),
  Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
      MvPolynomial σ S)
Tactic: apply induction_on f (fun r ↦ by simp) (fun p q hp hq ↦ by simp [hp, hq]) fun p j eq ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
inst_1 : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq :
  Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
      MvPolynomial σ S)
have inl : ∀
  (eq :
    Eq (α := MvPolynomial σ S)
      ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
        MvPolynomial σ S)
      ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv j : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
        MvPolynomial σ S)),
  Eq (α := MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv j : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
      MvPolynomial σ S)
Tactic: obtain rfl | h := eq_or_ne j i
Cleared hypotheses: i, eq
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
inst_1 : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq :
  Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)
inl :
  ∀
    (eq :
      Eq (α := MvPolynomial σ S)
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
          MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
            ((pderiv j : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial σ S)),
    Eq (α := MvPolynomial σ S)
      ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
          ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
        MvPolynomial σ S)
      ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
          ((pderiv j : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
        MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
      MvPolynomial σ S)
have inr : ∀ (h : j ≠ i),
  Eq (α := MvPolynomial σ S)
    ((pderiv i : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X j)) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X j)) :
      MvPolynomial σ S)
Tactic: obtain rfl | h := eq_or_ne j i