awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF :
  eval (HMul.hMul (α := K) (β := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) (((algebraMap ℤ K : (a : ℤ) → K) b)⁻¹ : K))
      (Polynomial.map (algebraMap ℤ K) f) =
    0
⊢ eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0
have inr : eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
Tactic: rwa [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivation (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
have this : HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
  (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f)
Tactic: have : C a • D f = D (C a * f) := by simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivation (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this :
  HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f)
⊢ HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
have rw : (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f) =
  HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
Tactic: rw [this, C_mul', D.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivation (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this :
  HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f)
rw :
  (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f) =
    HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
⊢ HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
have rw₁ : (D : (a : R[X]) → A) (a • f) = HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
Tactic: rw [this, C_mul', D.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivation (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this :
  HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f)
rw :
  (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f) =
    HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
rw₁ : (D : (a : R[X]) → A) (a • f) = HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
⊢ HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
have rw₂ : HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A) = HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
Tactic: rw [this, C_mul', D.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivation (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
a b : A
⊢ ((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (a + b)) :
          LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
        (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
      derivative' =
    HAdd.hAdd (α := Derivation R R[X] A) (β := Derivation R R[X] A)
      (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
              LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
            (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
          derivative' :
        Derivation R R[X] A)
      (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A b) :
              LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
            (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
          derivative' :
        Derivation R R[X] A)
have h : Eq.{u_2 + 1} (α := A)
  (((((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (a + b)) :
                LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
              (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
            derivative' :
          Derivation R R[X] A) :
        (a : R[X]) → A)
      X :
    A)
  ((HAdd.hAdd (α := Derivation R R[X] A) (β := Derivation R R[X] A)
          (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
                  LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
              derivative' :
            Derivation R R[X] A)
          (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A b) :
                  LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
              derivative' :
            Derivation R R[X] A) :
        (a : R[X]) → A)
      X :
    A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivation (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
t : R
a : A
⊢ ((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (t • a)) :
          LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
        (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
      derivative' =
    HSMul.hSMul (α := R) (β := Derivation R R[X] A) ((RingHom.id R : (a : R) → R) t : R)
      (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
              LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
            (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
          derivative' :
        Derivation R R[X] A)
have h : Eq.{u_2 + 1} (α := A)
  (((((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (t • a)) :
                LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
              (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
            derivative' :
          Derivation R R[X] A) :
        (a : R[X]) → A)
      X :
    A)
  ((HSMul.hSMul (α := R) (β := Derivation R R[X] A) ((RingHom.id R : (a : R) → R) t : R)
          (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
                  LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
              derivative' :
            Derivation R R[X] A) :
        (a : R[X]) → A)
      X :
    A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := Derivation R R[X] R[X])
    (((mkDerivation R : R[X] →ₗ[R] Derivation R R[X] R[X]) : (a : R[X]) → Derivation R R[X] R[X]) 1) derivative'
have h : Eq (α := R[X])
  ((((mkDerivation R : R[X] →ₗ[R] Derivation R R[X] R[X]) : (a : R[X]) → Derivation R R[X] R[X]) 1 : (a : R[X]) → R[X])
      X :
    R[X])
  ((derivative' : (a : R[X]) → R[X]) X : R[X])
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
⊢ Eq (α := R[X])
    ((((mkDerivation R : R[X] →ₗ[R] Derivation R R[X] R[X]) : (a : R[X]) → Derivation R R[X] R[X]) 1 :
          (a : R[X]) → R[X])
        f :
      R[X])
    ((derivative : (a : R[X]) → R[X]) f : R[X])
have rw : Eq (α := R[X]) ((derivative' : (a : R[X]) → R[X]) f : R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X])
Tactic: rw [mkDerivation_one_eq_derivative']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst : Semiring R
p q : R[X]
⊢ ((p + q).sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HAdd.hAdd (α := R[X])
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
      (q.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
have hf : ∀ (i : ℕ),
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑i : R)) : R[X])
      (HPow.hPow (α := R[X]) X (i - 1)) =
    0
Tactic: rw [sum_add_index]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst : Semiring R
p q : R[X]
hf :
  ∀ (i : ℕ),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑i : R)) : R[X])
        (HPow.hPow (α := R[X]) X (i - 1)) =
      0
⊢ ((p + q).sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HAdd.hAdd (α := R[X])
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
      (q.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
have h_add : ∀ (a : ℕ) (b₁ b₂ : R),
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((b₁ + b₂) * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (b₁ * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (b₂ * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1))
Tactic: rw [sum_add_index]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a_1 b : R
n : ℕ
inst : Semiring R
a : R
p : R[X]
⊢ ((a • p).sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) a : R)
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
have dsimp : ((a • p).sum fun (n : ℕ) (a : R) ↦
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
  HSMul.hSMul (β := R[X]) a
    (p.sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a_1 b : R
n : ℕ
inst : Semiring R
a : R
p : R[X]
⊢ ((a • p).sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HSMul.hSMul (β := R[X]) a
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
have rw : (p.sum fun (n : ℕ) (a_2 : R) ↦
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a_2 * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
  HSMul.hSMul (β := R[X]) a
    (p.sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
Tactic: rw [sum_smul_index]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a_1 b : R
n : ℕ
inst : Semiring R
a : R
p : R[X]
rw :
  (p.sum fun (n : ℕ) (a_2 : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a_2 * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HSMul.hSMul (β := R[X]) a
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
⊢ ((a • p).sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HSMul.hSMul (β := R[X]) a
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
have hf : ∀ (i : ℕ),
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑i : R)) : R[X])
      (HPow.hPow (α := R[X]) X (i - 1)) =
    0
Tactic: rw [sum_smul_index]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ coeff ((derivative : (a : R[X]) → R[X]) p) n = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
have rw : coeff
    (p.sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
    n =
  p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [derivative_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ coeff
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
      n =
    p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
have simp : (p.sum fun (a : ℕ) (b : R) ↦ b * (↑a : R) * if n = a - 1 then 1 else 0) =
  p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
Tactic: simp only [coeff_X_pow, coeff_sum, coeff_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun (a : ℕ) (b : R) ↦ b * (↑a : R) * if n = a - 1 then 1 else 0) =
    p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
have rw : (p.coeff (n + 1) * (↑(n + 1) : R) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [sum, Finset.sum_eq_single (n + 1)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw :
  (p.coeff (n + 1) * (↑(n + 1) : R) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
⊢ (p.sum fun (a : ℕ) (b : R) ↦ b * (↑a : R) * if n = a - 1 then 1 else 0) =
    p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
have h₀ : ∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * (↑b : R) * if n = b - 1 then 1 else 0) = 0
Tactic: rw [sum, Finset.sum_eq_single (n + 1)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw :
  (p.coeff (n + 1) * (↑(n + 1) : R) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
h₀ : ∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * (↑b : R) * if n = b - 1 then 1 else 0) = 0
⊢ (p.sum fun (a : ℕ) (b : R) ↦ b * (↑a : R) * if n = a - 1 then 1 else 0) =
    p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
have h₁ : n + 1 ∉ p.support → (p.coeff (n + 1) * (↑(n + 1) : R) * if n = n + 1 - 1 then 1 else 0) = 0
Tactic: rw [sum, Finset.sum_eq_single (n + 1)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p.coeff (n + 1) * (↑(n + 1) : R) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
have simp : p.coeff (n + 1) * (↑(n + 1) : R) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
Tactic: simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff (n + 1) * (↑(n + 1) : R) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
have norm_cast : p.coeff (n + 1) * (↑(n + 1) : R) = p.coeff (n + 1) * (↑(n + 1) : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n b : ℕ
⊢ b ∈ p.support → b ≠ n + 1 → (p.coeff b * (↑b : R) * if n = b - 1 then 1 else 0) = 0
have h₀ : 0 ∈ p.support → 0 ≠ n + 1 → (p.coeff 0 * (↑0 : R) * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n b : ℕ
h₀ : 0 ∈ p.support → 0 ≠ n + 1 → (p.coeff 0 * (↑0 : R) * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
⊢ b ∈ p.support → b ≠ n + 1 → (p.coeff b * (↑b : R) * if n = b - 1 then 1 else 0) = 0
have h₁ : ∀ (n_1 : ℕ),
  n_1 + 1 ∈ p.support → n_1 + 1 ≠ n + 1 → (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 + 1 - 1 then 1 else 0) = 0
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : 0 ∈ p.support
h_1 : 0 ≠ n + 1
⊢ (p.coeff 0 * (↑0 : R) * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
have h₀ : (p.coeff 0 * 0 * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
Tactic: rw [Nat.cast_zero, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : 0 ∈ p.support
h_1 : 0 ≠ n + 1
h₀ : (p.coeff 0 * 0 * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
⊢ (p.coeff 0 * (↑0 : R) * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
have h₁ : HMul.hMul (α := R) 0 (if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
Tactic: rw [Nat.cast_zero, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : 0 ∈ p.support
h_1 : 0 ≠ n + 1
h₀ : (p.coeff 0 * 0 * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
h₁ : HMul.hMul (α := R) 0 (if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
⊢ (p.coeff 0 * (↑0 : R) * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
have h₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [Nat.cast_zero, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n n_1 : ℕ
h : n_1 + 1 ∈ p.support
H : n_1 + 1 ≠ n + 1
⊢ (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 + 1 - 1 then 1 else 0) = 0
have h₀ : (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 then 1 else 0) = 0
Tactic: rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n n_1 : ℕ
h : n_1 + 1 ∈ p.support
H : n_1 + 1 ≠ n + 1
h₀ : (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 then 1 else 0) = 0
⊢ (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 + 1 - 1 then 1 else 0) = 0
have h₁ : p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * 0 = 0
Tactic: rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n n_1 : ℕ
h : n_1 + 1 ∈ p.support
H : n_1 + 1 ≠ n + 1
h₀ : (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 then 1 else 0) = 0
h₁ : p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * 0 = 0
⊢ (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 + 1 - 1 then 1 else 0) = 0
have h₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a) : R[X])
    ((monomial (n - 1) : (a : R) → R[X]) (a * (↑n : R)) : R[X])
have hf : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)) =
  0
Tactic: rw [derivative_apply, sum_monomial_index, C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial (n + 1) : (a : R) → R[X]) a) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
have rw : Eq (α := R[X]) ((monomial (n + 1 - 1) : (a : R) → R[X]) (a * (↑(n + 1) : R)) : R[X])
  ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
Tactic: rw [derivative_monomial, add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw :
  Eq (α := R[X]) ((monomial (n + 1 - 1) : (a : R) → R[X]) (a * (↑(n + 1) : R)) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial (n + 1) : (a : R) → R[X]) a) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
have rw₁ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * (↑(n + 1) : R)) : R[X])
  ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
Tactic: rw [derivative_monomial, add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw :
  Eq (α := R[X]) ((monomial (n + 1 - 1) : (a : R) → R[X]) (a * (↑(n + 1) : R)) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
rw₁ :
  Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * (↑(n + 1) : R)) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial (n + 1) : (a : R) → R[X]) a) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
have rw₂ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) (↑1 : R)) : R[X])
  ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
Tactic: rw [derivative_monomial, add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw :
  Eq (α := R[X]) ((monomial (n + 1 - 1) : (a : R) → R[X]) (a * (↑(n + 1) : R)) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
rw₁ :
  Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * (↑(n + 1) : R)) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
rw₂ :
  Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) (↑1 : R)) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial (n + 1) : (a : R) → R[X]) a) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
have rw₃ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
  ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
Tactic: rw [derivative_monomial, add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]