-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun (x : 𝕜) ↦ c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜} (hx : x ∈ s) (hf : ContDiffOn 𝕜 (↑n : WithTop ℕ∞) f s),
    iteratedDerivWithin n (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑(n + 1) : WithTop ℕ∞) f s
hcx : c * x ∈ s
h₀ :
  Set.EqOn.{u_1, u_2} (β := F) (iteratedDerivWithin n (fun (x : 𝕜) ↦ f (c * x)) s)
    (fun (x : 𝕜) ↦ c ^ n • iteratedDerivWithin n f s (c * x)) s
h₁ : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)
h₂ : DifferentiableWithinAt.{u_1, u_1, u_2} 𝕜 (F := F) (fun (x : 𝕜) ↦ iteratedDerivWithin n f s (c * x)) s x
succ :
  derivWithin (iteratedDerivWithin n (fun (x : 𝕜) ↦ f (c * x)) s) s x =
    c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
succ₁ :
  derivWithin (fun (x : 𝕜) ↦ c ^ n • iteratedDerivWithin n f s (c * x)) s x =
    c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
succ₂ :
  HSMul.hSMul (β := F) (c ^ n) (derivWithin (fun (x : 𝕜) ↦ iteratedDerivWithin n f s (c * x)) s x) =
    c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
succ₃ :
  HSMul.hSMul (β := F) (c ^ n) (derivWithin (fun (x : 𝕜) ↦ iteratedDerivWithin n f s (c * x)) s x) =
    c ^ (n + 1) • derivWithin (iteratedDerivWithin n f s) s (c * x)
succ₄ :
  c ^ n • derivWithin (iteratedDerivWithin n f s ∘ HMul.hMul c) s x =
    c ^ (n + 1) • derivWithin (iteratedDerivWithin n f s) s (c * x)
succ₅ :
  c ^ n • derivWithin (HMul.hMul c) s x • derivWithin (iteratedDerivWithin n f s) s (c * x) =
    c ^ (n + 1) • derivWithin (iteratedDerivWithin n f s) s (c * x)
succ₆ :
  c ^ n • (c * derivWithin (fun (y : 𝕜) ↦ y) s x) • derivWithin (iteratedDerivWithin n f s) s (c * x) =
    c ^ (n + 1) • derivWithin (iteratedDerivWithin n f s) s (c * x)
succ₇ :
  c ^ n • (c * 1) • derivWithin (iteratedDerivWithin n f s) s (c * x) =
    c ^ (n + 1) • derivWithin (iteratedDerivWithin n f s) s (c * x)
succ₈ :
  (c ^ n * (c * 1)) • derivWithin (iteratedDerivWithin n f s) s (c * x) =
    c ^ (n + 1) • derivWithin (iteratedDerivWithin n f s) s (c * x)
succ₉ :
  (c ^ n * c) • derivWithin (iteratedDerivWithin n f s) s (c * x) =
    c ^ (n + 1) • derivWithin (iteratedDerivWithin n f s) s (c * x)
succ₁₀ succ₁₁ :
  (c ^ n * c) • derivWithin (iteratedDerivWithin n f s) s (c * x) =
    (c ^ n * c) • derivWithin (iteratedDerivWithin n f s) s (c * x)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)

Tactic:
rw [iteratedDerivWithin_succ, derivWithin_congr h₀ (ih hx hf.of_succ),
      derivWithin_fun_const_smul (c ^ n) h₂, iteratedDerivWithin_succ,
      ← Function.comp_def, derivWithin.scomp x h₁ (by fun_prop) hs,
      derivWithin_const_mul _ differentiableWithinAt_id, derivWithin_id' _ _ (h _ hx),
      smul_smul, mul_one, pow_succ]

Premises used: derivWithin_id', derivWithin_congr, derivWithin.scomp, pow_succ, smul_smul, derivWithin_fun_const_smul, Function.comp_def, HPow.hPow, ContDiffOn.of_succ, iteratedDerivWithin_succ, mul_one, derivWithin_const_mul