awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
⊢ f.Splits
have pos : ∀ (hf0 : f = 0), f.Splits
Tactic: classical
  by_cases hf0 : f = 0
  · simp [hf0]
  obtain ⟨u, hu⟩ := factors_prod hf0
  rw [← hu]
  refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
  exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
pos : ∀ (hf0 : f = 0), f.Splits
⊢ f.Splits
have neg : ∀ (hf0 : ¬f = 0), f.Splits
Tactic: classical
  by_cases hf0 : f = 0
  · simp [hf0]
  obtain ⟨u, hu⟩ := factors_prod hf0
  rw [← hu]
  refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
  exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
pos : ∀ (hf0 : f = 0), f.Splits
neg neg₁ : ∀ (hf0 : ¬f = 0), f.Splits
⊢ f.Splits
have neg₂ : ∀ (hf0 : ¬f = 0) (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f), f.Splits
Tactic: classical
  by_cases hf0 : f = 0
  · simp [hf0]
  obtain ⟨u, hu⟩ := factors_prod hf0
  rw [← hu]
  refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
  exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
pos : ∀ (hf0 : f = 0), f.Splits
neg neg₁ : ∀ (hf0 : ¬f = 0), f.Splits
neg₂ : ∀ (hf0 : ¬f = 0) (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f), f.Splits
⊢ f.Splits
have neg₃ : ∀ (hf0 : ¬f = 0) (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f), ((factors f).prod * (↑u : R[X])).Splits
Tactic: classical
  by_cases hf0 : f = 0
  · simp [hf0]
  obtain ⟨u, hu⟩ := factors_prod hf0
  rw [← hu]
  refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
  exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
pos : ∀ (hf0 : f = 0), f.Splits
neg neg₁ : ∀ (hf0 : ¬f = 0), f.Splits
neg₂ : ∀ (hf0 : ¬f = 0) (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f), f.Splits
neg₃ : ∀ (hf0 : ¬f = 0) (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f), ((factors f).prod * (↑u : R[X])).Splits
⊢ f.Splits
have neg₄ : ∀ (hf0 : ¬f = 0) (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f) (g : R[X]) (hg : g ∈ factors f), g.Splits
Tactic: classical
  by_cases hf0 : f = 0
  · simp [hf0]
  obtain ⟨u, hu⟩ := factors_prod hf0
  rw [← hu]
  refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
  exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
F : Type u
K : Type v
inst : CommRing K
inst_1 : Field F
L : Type u_2
inst_2 : CommRing L
i : K →+* L
j : L →+* F
f : K[X]
⊢ (map j (map i f)).Splits ↔ (map (j.comp i) f).Splits
have rw : (map (j.comp i) f).Splits ↔ (map (j.comp i) f).Splits
Tactic: rw [Polynomial.map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
K : Type v
L : Type w
inst : CommRing K
inst_1 : Field L
i : K →+* L
f : K[X]
⊢ (map (RingHom.id L) (map i f)).Splits ↔ (map i f).Splits
have rw : (map i f).Splits ↔ (map i f).Splits
Tactic: rw [map_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ Eq (α := R[X]) ((sumIDeriv : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) a) : R[X]) ((C : (a : R) → R[X]) a : R[X])
have rw : Eq (α := R[X])
  (∑ i ∈ range (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) + 1),
      (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) :
    R[X])
  ((C : (a : R) → R[X]) a : R[X])
Tactic: rw [sumIDeriv_apply, natDegree_C, zero_add, sum_range_one, Function.iterate_zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
rw :
  Eq (α := R[X])
    (∑ i ∈ range (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) + 1),
        (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) :
      R[X])
    ((C : (a : R) → R[X]) a : R[X])
⊢ Eq (α := R[X]) ((sumIDeriv : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) a) : R[X]) ((C : (a : R) → R[X]) a : R[X])
have rw₁ : Eq (α := R[X])
  (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) : R[X])
  ((C : (a : R) → R[X]) a : R[X])
Tactic: rw [sumIDeriv_apply, natDegree_C, zero_add, sum_range_one, Function.iterate_zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
rw :
  Eq (α := R[X])
    (∑ i ∈ range (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) + 1),
        (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) :
      R[X])
    ((C : (a : R) → R[X]) a : R[X])
rw₁ :
  Eq (α := R[X])
    (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) : R[X])
    ((C : (a : R) → R[X]) a : R[X])
rw₂ :
  Eq (α := R[X]) (∑ i ∈ range 1, (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) : R[X])
    ((C : (a : R) → R[X]) a : R[X])
⊢ Eq (α := R[X]) ((sumIDeriv : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) a) : R[X]) ((C : (a : R) → R[X]) a : R[X])
have rw₃ : Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0] ((C : (a : R) → R[X]) a) : R[X]) ((C : (a : R) → R[X]) a : R[X])
Tactic: rw [sumIDeriv_apply, natDegree_C, zero_add, sum_range_one, Function.iterate_zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
rw :
  Eq (α := R[X])
    (∑ i ∈ range (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) + 1),
        (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) :
      R[X])
    ((C : (a : R) → R[X]) a : R[X])
rw₁ :
  Eq (α := R[X])
    (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) : R[X])
    ((C : (a : R) → R[X]) a : R[X])
rw₂ :
  Eq (α := R[X]) (∑ i ∈ range 1, (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) : R[X])
    ((C : (a : R) → R[X]) a : R[X])
rw₃ :
  Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0] ((C : (a : R) → R[X]) a) : R[X]) ((C : (a : R) → R[X]) a : R[X])
⊢ Eq (α := R[X]) ((sumIDeriv : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) a) : R[X]) ((C : (a : R) → R[X]) a : R[X])
have rw₄ : Eq (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a : R[X])
Tactic: rw [sumIDeriv_apply, natDegree_C, zero_add, sum_range_one, Function.iterate_zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
have rw : ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
  HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
Tactic: rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
rw :
  ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
have rw₁ : ∑ i ∈ range (HAdd.hAdd (α := ℕ) 1 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
  HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
Tactic: rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
rw :
  ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₁ :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 1 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
have rw₂ : HAdd.hAdd (α := ℕ[X]) (∑ x ∈ range 1, (⇑derivative : (a : ℕ[X]) → ℕ[X])^[x] X)
    ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
  HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
Tactic: rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
rw :
  ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₁ :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 1 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₂ :
  HAdd.hAdd (α := ℕ[X]) (∑ x ∈ range 1, (⇑derivative : (a : ℕ[X]) → ℕ[X])^[x] X)
      ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
have rw₃ : HAdd.hAdd (α := ℕ[X]) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[0] X) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
  HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
Tactic: rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
rw :
  ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₁ :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 1 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₂ :
  HAdd.hAdd (α := ℕ[X]) (∑ x ∈ range 1, (⇑derivative : (a : ℕ[X]) → ℕ[X])^[x] X)
      ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₃ :
  HAdd.hAdd (α := ℕ[X]) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[0] X) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
have rw₄ : HAdd.hAdd (α := ℕ[X]) X ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
Tactic: rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
rw :
  ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₁ :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 1 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₂ :
  HAdd.hAdd (α := ℕ[X]) (∑ x ∈ range 1, (⇑derivative : (a : ℕ[X]) → ℕ[X])^[x] X)
      ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₃ :
  HAdd.hAdd (α := ℕ[X]) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[0] X) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₄ :
  HAdd.hAdd (α := ℕ[X]) X ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
have rw₅ : HAdd.hAdd (α := ℕ[X]) (β := ℕ[X]) X ((derivative : (a : ℕ[X]) → ℕ[X]) X : ℕ[X]) =
  HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
Tactic: rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
rw :
  ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₁ :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 1 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₂ :
  HAdd.hAdd (α := ℕ[X]) (∑ x ∈ range 1, (⇑derivative : (a : ℕ[X]) → ℕ[X])^[x] X)
      ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₃ :
  HAdd.hAdd (α := ℕ[X]) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[0] X) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₄ :
  HAdd.hAdd (α := ℕ[X]) X ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₅ :
  HAdd.hAdd (α := ℕ[X]) (β := ℕ[X]) X ((derivative : (a : ℕ[X]) → ℕ[X]) X : ℕ[X]) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
have rw₆ : HAdd.hAdd (α := ℕ[X]) X 1 = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
Tactic: rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
rw :
  ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₁ :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 1 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₂ :
  HAdd.hAdd (α := ℕ[X]) (∑ x ∈ range 1, (⇑derivative : (a : ℕ[X]) → ℕ[X])^[x] X)
      ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₃ :
  HAdd.hAdd (α := ℕ[X]) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[0] X) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₄ :
  HAdd.hAdd (α := ℕ[X]) X ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₅ :
  HAdd.hAdd (α := ℕ[X]) (β := ℕ[X]) X ((derivative : (a : ℕ[X]) → ℕ[X]) X : ℕ[X]) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₆ : HAdd.hAdd (α := ℕ[X]) X 1 = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
have rw₇ : HAdd.hAdd (α := ℕ[X]) X 1 = HAdd.hAdd (α := ℕ[X]) X (↑1 : ℕ[X])
Tactic: rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
rw :
  ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₁ :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 1 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₂ :
  HAdd.hAdd (α := ℕ[X]) (∑ x ∈ range 1, (⇑derivative : (a : ℕ[X]) → ℕ[X])^[x] X)
      ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₃ :
  HAdd.hAdd (α := ℕ[X]) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[0] X) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₄ :
  HAdd.hAdd (α := ℕ[X]) X ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₅ :
  HAdd.hAdd (α := ℕ[X]) (β := ℕ[X]) X ((derivative : (a : ℕ[X]) → ℕ[X]) X : ℕ[X]) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₆ : HAdd.hAdd (α := ℕ[X]) X 1 = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₇ : HAdd.hAdd (α := ℕ[X]) X 1 = HAdd.hAdd (α := ℕ[X]) X (↑1 : ℕ[X])
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
have rw₈ : HAdd.hAdd (α := ℕ[X]) X 1 = HAdd.hAdd (α := ℕ[X]) X 1
Tactic: rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (map f p).natDegree p.natDegree
⊢ (sumIDeriv : (a : S[X]) → S[X]) (map f p) = map f ((sumIDeriv : (a : R[X]) → R[X]) p)
have rw : ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p) =
  map f ((sumIDeriv : (a : R[X]) → R[X]) p)
Tactic: rw [sumIDeriv_apply_of_le (le_max_left _ _ : _ ≤ n)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (map f p).natDegree p.natDegree
⊢ ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p) =
    map f ((sumIDeriv : (a : R[X]) → R[X]) p)
have rw : ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p) =
  map f (∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : R[X]) → R[X])^[i] p)
Tactic: rw [sumIDeriv_apply_of_le (le_max_right _ _ : _ ≤ n)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (map f p).natDegree p.natDegree
⊢ ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p) =
    map f (∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : R[X]) → R[X])^[i] p)
have simp_rw : Eq.{u_2 + 1} (α := S[X])
  (∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p))
  (∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), map f ((⇑derivative : (a : R[X]) → R[X])^[i] p))
Tactic: simp_rw [Polynomial.map_sum, iterate_derivative_map p f]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ Eq (α := R[X]) ((sumIDeriv : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p) : R[X])
    ((derivative : (a : R[X]) → R[X]) ((sumIDeriv : (a : R[X]) → R[X]) p) : R[X])
have rw : Eq.{u_1 + 1} (α := R[X])
  (∑ i ∈ range (p.natDegree + 1), (⇑derivative : (a : R[X]) → R[X])^[i] ((derivative : (a : R[X]) → R[X]) p))
  (∑ b ∈ range (p.natDegree + 1), (derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[b] p))
Tactic: rw [sumIDeriv_apply_of_le ((natDegree_derivative_le p).trans tsub_le_self), sumIDeriv_apply,
    derivative_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ (sumIDeriv : (a : R[X]) → R[X]) p =
    HAdd.hAdd (β := R[X]) p ((derivative : (a : R[X]) → R[X]) ((sumIDeriv : (a : R[X]) → R[X]) p) : R[X])
have rw : (⇑derivative : (a : R[X]) → R[X])^[0] p +
    HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
  p +
    HAdd.hAdd (α := R[X]) (β := R[X])
      (∑ x ∈ range p.natDegree, (derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : R[X])
      ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[p.natDegree] p) : R[X])
Tactic: rw [sumIDeriv_apply, derivative_sum, sum_range_succ', sum_range_succ,
    add_comm, ← add_zero (Finset.sum _ _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] p +
      HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
    p +
      HAdd.hAdd (α := R[X]) (β := R[X])
        (∑ x ∈ range p.natDegree, (derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : R[X])
        ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[p.natDegree] p) : R[X])
have simp_rw : (⇑derivative : (a : R[X]) → R[X])^[0] p +
    HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
  p +
    (∑ x ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[x.succ] p +
      (⇑derivative : (a : R[X]) → R[X])^[p.natDegree.succ] p)
Tactic: simp_rw [← Function.iterate_succ_apply' derivative, Nat.succ_eq_add_one,
    Function.iterate_zero_apply, iterate_derivative_eq_zero (Nat.lt_succ_self _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
simp_rw :
  (⇑derivative : (a : R[X]) → R[X])^[0] p +
      HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
    p +
      (∑ x ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[x.succ] p +
        (⇑derivative : (a : R[X]) → R[X])^[p.natDegree.succ] p)
simp_rw₁ :
  (⇑derivative : (a : R[X]) → R[X])^[0] p +
      HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
    p +
      (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p +
        (⇑derivative : (a : R[X]) → R[X])^[p.natDegree + 1] p)
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] p +
      HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
    p +
      HAdd.hAdd (α := R[X]) (β := R[X])
        (∑ x ∈ range p.natDegree, (derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : R[X])
        ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[p.natDegree] p) : R[X])
have simp_rw₂ : p + HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
  p +
    (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p +
      (⇑derivative : (a : R[X]) → R[X])^[p.natDegree + 1] p)
Tactic: simp_rw [← Function.iterate_succ_apply' derivative, Nat.succ_eq_add_one,
    Function.iterate_zero_apply, iterate_derivative_eq_zero (Nat.lt_succ_self _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
k : ℕ
⊢ ∃ (gp : R[X]), gp.natDegree ≤ p.natDegree - k ∧ (⇑derivative : (a : R[X]) → R[X])^[k] p = k ! • gp
have refine : fold max 0
    (Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree fun (i : ℕ) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
        (HPow.hPow (α := R[X]) X i))
    ((⇑derivative : (a : R[X]) → R[X])^[k] p).support ≤
  p.natDegree - k
Tactic: refine ⟨_, (natDegree_sum_le _ _).trans ?_, iterate_derivative_eq_factorial_smul_sum p k⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
k : ℕ
⊢ fold max 0
      (Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree fun (i : ℕ) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
          (HPow.hPow (α := R[X]) X i))
      ((⇑derivative : (a : R[X]) → R[X])^[k] p).support ≤
    p.natDegree - k
have rw : 0 ≤ p.natDegree - k ∧
  ∀ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree
        (fun (i : ℕ) ↦
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
            (HPow.hPow (α := R[X]) X i))
        x ≤
      p.natDegree - k
Tactic: rw [fold_max_le]