-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDerivWithin_comp_const_smul (hf : ContDiffOn 𝕜 n f s) (c : 𝕜)
    (hs : Set.MapsTo (c * ·) s s) :
    iteratedDerivWithin n (fun x => f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)

Proof state:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x => c * x) s s
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑0) f s
⊢ iteratedDerivWithin 0 (fun x => f (c * x)) s x = c ^ 0 • iteratedDerivWithin 0 f s (c * x)

Tactic:
simp

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x => c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) 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)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (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)
⊢ Set.MapsTo (HMul.hMul c) s s

Tactic:
exact hs

Result:
no goals

Proof state:
case hg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x => c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) 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)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (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)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) ?t (c * x)

Tactic:
exact hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) h _ hcx

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x => c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) 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)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (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 𝕜 (fun x => iteratedDerivWithin n f s (c * x)) s 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_const_smul (c ^ n) h₂, iteratedDerivWithin_succ,
  ← Function.comp_def,
  derivWithin.scomp x h₁ (differentiableWithinAt_id'.const_mul _) hs,
  derivWithin_const_mul _ differentiableWithinAt_id', derivWithin_id' _ _ (h _ hx),
  smul_smul, mul_one, pow_succ]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x => c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) 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)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (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)
⊢ DifferentiableWithinAt 𝕜 (fun x => iteratedDerivWithin n f s (c * x)) s x

Tactic:
rw [← Function.comp_def]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x => c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) 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)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (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)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s ∘ HMul.hMul c) s x

Proof state:
case hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x => c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) 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)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (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)
⊢ DifferentiableWithinAt 𝕜 (HMul.hMul c) s x

Tactic:
exact differentiableWithinAt_id'.const_mul _

Result:
no goals