𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ HasDerivWithinAt (fun z => (((↑k + 1) * ↑k !)⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z)
    ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
      ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
    t y
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt (fun z => (((↑k + 1) * ↑k !)⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z)
    ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
      ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
    t y
replace hf :
  HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y := by
  convert (hf.mono_of_mem hs).hasDerivWithinAt using 1
  rw [iteratedDerivWithin_succ (ht.mono_nhds (nhdsWithin_le_iff.mpr hs))]
  exact (derivWithin_of_mem hs ht hf).symm
case h.e'_7
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y
⊢ (((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
      ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y =
    (((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y +
      -((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y
⊢ HasDerivWithinAt (fun z => (((↑k + 1) * ↑k !)⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z)
    ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
      ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
    t y
convert this.smul hf using 1
case h.e'_7
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y
⊢ ((x - y) ^ (k + 1) / ((↑k + 1) * ↑k !)) • iteratedDerivWithin (k + 2) f s y -
      ((x - y) ^ k / ↑k !) • iteratedDerivWithin (k + 1) f s y =
    ((x - y) ^ (k + 1) / ((↑k + 1) * ↑k !)) • iteratedDerivWithin (k + 2) f s y +
      (-(x - y) ^ k / ↑k !) • iteratedDerivWithin (k + 1) f s y
case h.e'_7
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y
⊢ (((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
      ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y =
    (((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y +
      -((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y
field_simp [Nat.cast_add_one_ne_zero k, Nat.factorial_ne_zero k]
no goals
case h.e'_7
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y
⊢ ((x - y) ^ (k + 1) / ((↑k + 1) * ↑k !)) • iteratedDerivWithin (k + 2) f s y -
      ((x - y) ^ k / ↑k !) • iteratedDerivWithin (k + 1) f s y =
    ((x - y) ^ (k + 1) / ((↑k + 1) * ↑k !)) • iteratedDerivWithin (k + 2) f s y +
      (-(x - y) ^ k / ↑k !) • iteratedDerivWithin (k + 1) f s y
rw [neg_div, neg_smul, sub_eq_add_neg]
case h.e'_7
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ iteratedDerivWithin (k + 2) f s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
convert (hf.mono_of_mem hs).hasDerivWithinAt using 1
case h.e'_7
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ derivWithin (iteratedDerivWithin (k + 1) f s) s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
case h.e'_7
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ iteratedDerivWithin (k + 2) f s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
rw [iteratedDerivWithin_succ (ht.mono_nhds (nhdsWithin_le_iff.mpr hs))]
no goals
case h.e'_7
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ derivWithin (iteratedDerivWithin (k + 1) f s) s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
exact (derivWithin_of_mem hs ht hf).symm
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : -((↑k !)⁻¹ * (x - y) ^ k) = ((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)
⊢ HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k))
    t y
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : -((↑k !)⁻¹ * (x - y) ^ k) = ((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)
⊢ HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y
rw [this]
no goals
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : -((↑k !)⁻¹ * (x - y) ^ k) = ((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)
⊢ HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k))
    t y
exact (monomial_has_deriv_aux y x _).hasDerivWithinAt.const_mul _
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ -(x - y) ^ k = (-1 + -↑k) * (x - y) ^ k * ↑k ! / ((↑k + 1) * ↑k !)
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ -((↑k !)⁻¹ * (x - y) ^ k) = ((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)
field_simp [k.factorial_ne_zero]
case ha
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ ↑k + 1 ≠ 0

case hc
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ ↑k ! ≠ 0
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ -(x - y) ^ k = (-1 + -↑k) * (x - y) ^ k * ↑k ! / ((↑k + 1) * ↑k !)
rw [mul_div_mul_right, ← neg_add_rev, neg_mul, neg_div, mul_div_cancel_left]
no goals
case ha
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ ↑k + 1 ≠ 0
exact k.cast_add_one_ne_zero
no goals
case hc
𝕜 : Type ?u.264755
E : Type u_1
F : Type ?u.264761
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ ↑k ! ≠ 0
simp [k.factorial_ne_zero]