case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ ∀ (m : ℕ),
    coeff ((↑derivative^[Nat.zero]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ Nat.zero), i) • coeff p (m + Nat.zero)

case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
⊢ ∀ (m : ℕ),
    coeff ((↑derivative^[Nat.succ k]) p) m =
      (∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i) • coeff p (m + Nat.succ k)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
k : ℕ
p : R[X]
⊢ ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
induction' k with k ih
no goals
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ ∀ (m : ℕ),
    coeff ((↑derivative^[Nat.zero]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ Nat.zero), i) • coeff p (m + Nat.zero)
simp  [add_zero, forall_const, one_smul, Ico_self, eq_self_iff_true,
  Function.iterate_zero_apply, prod_empty]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ coeff ((↑derivative^[Nat.succ k]) p) m =
    (∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i) • coeff p (m + Nat.succ k)
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
⊢ ∀ (m : ℕ),
    coeff ((↑derivative^[Nat.succ k]) p) m =
      (∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i) • coeff p (m + Nat.succ k)
intro m
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ ((∏ i in Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k), i) * (m + 1)) • coeff p (m + 1 + k) =
    (∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i) • coeff p (m + Nat.succ k)
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ coeff ((↑derivative^[Nat.succ k]) p) m =
    (∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i) • coeff p (m + Nat.succ k)
rw [Function.iterate_succ_apply', coeff_derivative, ih (m + 1), ← Nat.cast_add_one, ←
  nsmul_eq_mul', smul_smul, mul_comm]
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ (∏ i in Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k), i) * (m + 1) =
    ∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i

case succ.hy
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ coeff p (m + 1 + k) = coeff p (m + Nat.succ k)
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ ((∏ i in Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k), i) * (m + 1)) • coeff p (m + 1 + k) =
    (∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i) • coeff p (m + Nat.succ k)
apply congr_arg₂
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
set_eq : Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
⊢ (∏ i in Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k), i) * (m + 1) =
    ∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ (∏ i in Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k), i) * (m + 1) =
    ∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i
have set_eq : Ico m.succ (m + k.succ.succ) = Ico (m + 1).succ (m + 1 + k.succ) ∪ {m + 1} := by
  simp_rw [← Nat.Ico_succ_singleton, union_comm, Nat.succ_eq_add_one, add_comm (k + 1),
    add_assoc]
  rw [Ico_union_Ico_eq_Ico] <;> simp
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
set_eq : Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
⊢ Disjoint (Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k)) {m + 1}
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
set_eq : Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
⊢ (∏ i in Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k), i) * (m + 1) =
    ∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i
rw [set_eq, prod_union, prod_singleton]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ Ico (m + 1) (m + (1 + (k + 1))) = Ico (m + 1) (m + (1 + 1)) ∪ Ico (m + (1 + 1)) (m + (1 + (k + 1)))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
simp_rw [← Nat.Ico_succ_singleton, union_comm, Nat.succ_eq_add_one, add_comm (k + 1),
  add_assoc]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ Ico (m + 1) (m + (1 + (k + 1))) = Ico (m + 1) (m + (1 + 1)) ∪ Ico (m + (1 + 1)) (m + (1 + (k + 1)))
rw [Ico_union_Ico_eq_Ico] <;> simp
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
set_eq : Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
⊢ ¬(Nat.succ (m + 1) ≤ m + 1 ∧ m + 1 < m + 1 + Nat.succ k)
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
set_eq : Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
⊢ Disjoint (Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k)) {m + 1}
rw [disjoint_singleton_right, mem_Ico]
no goals
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
set_eq : Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
⊢ ¬(Nat.succ (m + 1) ≤ m + 1 ∧ m + 1 < m + 1 + Nat.succ k)
exact fun h => (Nat.lt_succ_self _).not_le h.1
no goals
case succ.hy
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative^[k]) p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ coeff p (m + 1 + k) = coeff p (m + Nat.succ k)
exact congr_arg _ (Nat.succ_add m k)