-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDerivWithin_succ {x : 𝕜} :
    iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Proof state:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Tactic:
rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
  iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_fderivWithin _ hxs, derivWithin]

Result:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ (((↑{ toLinearEquiv := (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).comp
          (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x))
        1)
      (Fin.tail fun x => 1) =
    (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : 𝓝[s \ {x}] x = ⊥
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Proof state:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1)) fun x => 1) =
    (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1

Tactic:
simp

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : 𝓝[s \ {x}] x = ⊥
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Tactic:
simp [derivWithin_zero_of_isolated hxs, iteratedDerivWithin, iteratedFDerivWithin,
  fderivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ (((↑{ toLinearEquiv := (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).comp
          (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x))
        1)
      (Fin.tail fun x => 1) =
    (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1

Tactic:
change ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜
  (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun _ : Fin n => 1) =
  (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1

Result:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1)) fun x => 1) =
    (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1