awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative : (a : R[X]) → R[X])^[q + k] p = (q + k)! • p'
r : A
simp_rw :
  (aeval r : (a : R[X]) → A) ((q + k)! • p') =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
simp_rw₁ :
  (aeval r : (a : R[X]) → A) ((↑(q + k)! : R[X]) * p') =
    HMul.hMul (α := A) (β := A) ((↑q ! : A) : A)
      ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
simp_rw₂ :
  HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑(q + k)! : R[X]) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    (↑q ! : A) *
      HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑((q + k).descFactorial k) : R[X]) : A)
        ((aeval r : (a : R[X]) → A) p' : A)
simp_rw₃ :
  HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    (↑q ! : A) * HMul.hMul (α := A) (β := A) ((↑((q + k).descFactorial k) : A) : A) ((aeval r : (a : R[X]) → A) p' : A)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
have simp_rw₄ : HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
  HMul.hMul (β := A) (HMul.hMul (α := A) (↑q ! : A) (↑((q + k).descFactorial k) : A))
    ((aeval r : (a : R[X]) → A) p' : A)
Tactic: simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
    Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative : (a : R[X]) → R[X])^[q + k] p = (q + k)! • p'
r : A
simp_rw :
  (aeval r : (a : R[X]) → A) ((q + k)! • p') =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
simp_rw₁ :
  (aeval r : (a : R[X]) → A) ((↑(q + k)! : R[X]) * p') =
    HMul.hMul (α := A) (β := A) ((↑q ! : A) : A)
      ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
simp_rw₂ :
  HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑(q + k)! : R[X]) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    (↑q ! : A) *
      HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑((q + k).descFactorial k) : R[X]) : A)
        ((aeval r : (a : R[X]) → A) p' : A)
simp_rw₃ :
  HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    (↑q ! : A) * HMul.hMul (α := A) (β := A) ((↑((q + k).descFactorial k) : A) : A) ((aeval r : (a : R[X]) → A) p' : A)
simp_rw₄ :
  HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    HMul.hMul (β := A) (HMul.hMul (α := A) (↑q ! : A) (↑((q + k).descFactorial k) : A))
      ((aeval r : (a : R[X]) → A) p' : A)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
have simp_rw₅ : HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
  HMul.hMul (α := A) (β := A) ((↑(q ! * (q + k).descFactorial k) : A) : A) ((aeval r : (a : R[X]) → A) p' : A)
Tactic: simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
    Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative : (a : R[X]) → R[X])^[q + k] p = (q + k)! • p'
r : A
simp_rw :
  (aeval r : (a : R[X]) → A) ((q + k)! • p') =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
simp_rw₁ :
  (aeval r : (a : R[X]) → A) ((↑(q + k)! : R[X]) * p') =
    HMul.hMul (α := A) (β := A) ((↑q ! : A) : A)
      ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
simp_rw₂ :
  HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑(q + k)! : R[X]) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    (↑q ! : A) *
      HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑((q + k).descFactorial k) : R[X]) : A)
        ((aeval r : (a : R[X]) → A) p' : A)
simp_rw₃ :
  HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    (↑q ! : A) * HMul.hMul (α := A) (β := A) ((↑((q + k).descFactorial k) : A) : A) ((aeval r : (a : R[X]) → A) p' : A)
simp_rw₄ :
  HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    HMul.hMul (β := A) (HMul.hMul (α := A) (↑q ! : A) (↑((q + k).descFactorial k) : A))
      ((aeval r : (a : R[X]) → A) p' : A)
simp_rw₅ :
  HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    HMul.hMul (α := A) (β := A) ((↑(q ! * (q + k).descFactorial k) : A) : A) ((aeval r : (a : R[X]) → A) p' : A)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
have simp_rw₆ : HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
  HMul.hMul (α := A) (β := A) ((↑(q ! * (q + 1).ascFactorial k) : A) : A) ((aeval r : (a : R[X]) → A) p' : A)
Tactic: simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
    Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
r : A
⊢ (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
have rw : eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
  eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
Tactic: rw [aeval_def, eval, sumIDeriv_map, eval₂_map, RingHom.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
r : A
rw :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
⊢ (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
have rw₁ : eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
  eval₂ (RingHom.id A) r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
Tactic: rw [aeval_def, eval, sumIDeriv_map, eval₂_map, RingHom.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
r : A
rw :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
rw₁ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (RingHom.id A) r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
⊢ (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
have rw₂ : eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
  eval₂ (RingHom.id A) r (map (algebraMap R A) ((sumIDeriv : (a : R[X]) → R[X]) p))
Tactic: rw [aeval_def, eval, sumIDeriv_map, eval₂_map, RingHom.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
r : A
rw :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
rw₁ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (RingHom.id A) r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
rw₂ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (RingHom.id A) r (map (algebraMap R A) ((sumIDeriv : (a : R[X]) → R[X]) p))
⊢ (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
have rw₃ : eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
  eval₂ (RingHom.comp (RingHom.id A) (algebraMap R A)) r ((sumIDeriv : (a : R[X]) → R[X]) p)
Tactic: rw [aeval_def, eval, sumIDeriv_map, eval₂_map, RingHom.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
r : A
rw :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
rw₁ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (RingHom.id A) r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
rw₂ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (RingHom.id A) r (map (algebraMap R A) ((sumIDeriv : (a : R[X]) → R[X]) p))
rw₃ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (RingHom.comp (RingHom.id A) (algebraMap R A)) r ((sumIDeriv : (a : R[X]) → R[X]) p)
⊢ (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
have rw₄ : eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p)
Tactic: rw [aeval_def, eval, sumIDeriv_map, eval₂_map, RingHom.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have h : natDegree.{u_1} (R := R) 0 ≤ p.natDegree - q ∧
  ∀ (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
        HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ 0 ≤ p.natDegree - q ∧
    ∀ (r : A),
      HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
        (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
          HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
have right : ∀ (r : A),
  HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
Tactic: use Nat.zero_le _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
r : A
⊢ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
have right : ∀ (p' : A[X])
  (hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q * p'),
  (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
Tactic: ⟨p', hp⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q * p'
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
have right : (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) = HSMul.hSMul (β := A) q ! 0
Tactic: rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q * p'
right : (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) = HSMul.hSMul (β := A) q ! 0
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
have right₁ : Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) : A) (0 : A)
Tactic: rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q * p'
right : (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) = HSMul.hSMul (β := A) q ! 0
right₁ : Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) : A) (0 : A)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
have right₂ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q k : ℕ
hk : q ≤ k
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have inr : ∀ (gp : R[X]) (gp_le : gp.natDegree ≤ p.natDegree - k)
  (h :
    ∀ (r : A),
      (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
        HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)),
  ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
Tactic: obtain ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q k : ℕ
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have x : k < q ∨ q ≤ k
Tactic: cases lt_or_ge k q with
    | inl hk =>
      use 0
      rw [natDegree_zero]
      use Nat.zero_le _
      intro r ⟨p', hp⟩
      rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
    | inr hk =>
      obtain ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk
      exact ⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have h : ∀ (k : ℕ),
  ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
Tactic: have h (k) :
      ∃ gp : R[X], gp.natDegree ≤ p.natDegree - q ∧
        ∀ (r : A), (X - C r) ^ q ∣ p.map (algebraMap R A) →
          aeval r (derivative^[k] p) = q ! • aeval r gp := by
    cases lt_or_ge k q with
    | inl hk =>
      use 0
      rw [natDegree_zero]
      use Nat.zero_le _
      intro r ⟨p', hp⟩
      rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
    | inr hk =>
      obtain ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk
      exact ⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
h :
  ∀ (k : ℕ),
    ∃ (gp : R[X]),
      gp.natDegree ≤ p.natDegree - q ∧
        ∀ (r : A),
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have choose : ∀ (c : (k : ℕ) → R[X])
  (h :
    ∀ (k : ℕ),
      (c k).natDegree ≤ p.natDegree - q ∧
        ∀ (r : A),
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)),
  ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
Tactic: choose c h using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
c : (k : ℕ) → R[X]
h :
  ∀ (k : ℕ),
    (c k).natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
Tactic: choose c_le hc using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
c : (k : ℕ) → R[X]
h :
  ∀ (k : ℕ),
    (c k).natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have hc : ∀ (k : ℕ) (r : A),
  HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
Tactic: choose c_le hc using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
c : (k : ℕ) → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc :
  ∀ (k : ℕ) (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
        HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have refine_1 : ((range (p.natDegree + 1)).sum c).natDegree ≤ p.natDegree - q
Tactic: refine ⟨(range (p.natDegree + 1)).sum c, ?_, ?_⟩