awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝔸
f : 𝕜 → 𝔸
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ c * f z) s x = c * iteratedDerivWithin n f s x

Tactic:
iteratedDerivWithin_fun_const_smul hx h c hf

Premises used: iteratedDerivWithin_fun_const_smul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ c • f z) s x = c • iteratedDerivWithin n f s x

Tactic:
iteratedDerivWithin_const_smul_field c f

Premises used: iteratedDerivWithin_const_smul_field
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
𝕜' : Type u_6
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c : 𝕜'
f : 𝕜 → 𝕜'
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ c * f z) s x = c * iteratedDerivWithin n f s x

Tactic:
iteratedDerivWithin_fun_const_smul_field c f

Premises used: iteratedDerivWithin_fun_const_smul_field
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
inst_5 : Module 𝔸 F
inst_6 : IsBoundedSMul 𝔸 F
inst_7 : IsScalarTower 𝕜 𝔸 F
f : 𝕜 → 𝔸
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
v : F
⊢ iteratedDerivWithin n (fun (y : 𝕜) ↦ f y • v) s x = iteratedDerivWithin n f s x • v

Tactic:
simp [iteratedDerivWithin, iteratedFDerivWithin_smul_const_apply hf h hx]

Premises used: iteratedDerivWithin, iteratedFDerivWithin_smul_const_apply
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
d : 𝔸
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin n f s x * d

Tactic:
iteratedDerivWithin_smul_const hx h hf d

Premises used: iteratedDerivWithin_smul_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
𝕜' : Type u_6
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
d : 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
⊢ iteratedDerivWithin 0 (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin 0 f s x * d

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
𝕜' : Type u_6
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
d : 𝕜'
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → 𝕜'), iteratedDerivWithin n (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin n f s x * d
x : 𝕜
f : 𝕜 → 𝕜'
succ :
  derivWithin (iteratedDerivWithin n (fun (z : 𝕜) ↦ f z * d) s) s x = derivWithin (iteratedDerivWithin n f s) s x * d
succ₁ :
  derivWithin (fun (x : 𝕜) ↦ iteratedDerivWithin n f s x * d) s x = derivWithin (iteratedDerivWithin n f s) s x * d
⊢ iteratedDerivWithin (n + 1) (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin (n + 1) f s x * d

Tactic:
simp_rw [iteratedDerivWithin_succ, funext (@IH · f), derivWithin_mul_const_field]

Premises used: derivWithin_mul_const_field, funext, iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
𝕜' : Type u_6
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
d : 𝕜'
zero : ∀ {x : 𝕜} (f : 𝕜 → 𝕜'), iteratedDerivWithin 0 (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin 0 f s x * d
succ :
  ∀ (n : ℕ)
    (IH : ∀ {x : 𝕜} (f : 𝕜 → 𝕜'), iteratedDerivWithin n (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin n f s x * d)
    {x : 𝕜} (f : 𝕜 → 𝕜'),
    iteratedDerivWithin (n + 1) (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin (n + 1) f s x * d
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin n f s x * d

Tactic:
induction n generalizing f x with
  | zero => simp
  | succ n IH =>
    simp_rw [iteratedDerivWithin_succ, funext (@IH · f), derivWithin_mul_const_field]

Premises used: derivWithin_mul_const_field, iteratedDerivWithin_succ
-- 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 𝕜
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin 0 (-f) s x = -iteratedDerivWithin 0 f s x

Tactic:
simp
-- 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 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x : 𝕜
succ : derivWithin (iteratedDerivWithin n (-f) s) s x = -derivWithin (iteratedDerivWithin n f s) s x
⊢ iteratedDerivWithin (n + 1) (-f) s x = -iteratedDerivWithin (n + 1) f s x

Tactic:
simp only [iteratedDerivWithin_succ]

Premises used: iteratedDerivWithin_succ
-- 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 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x : 𝕜
succ : derivWithin (iteratedDerivWithin n (-f) s) s x = derivWithin (-iteratedDerivWithin n f s) s x
⊢ derivWithin (iteratedDerivWithin n (-f) s) s x = -derivWithin (iteratedDerivWithin n f s) s x

Tactic:
rw [← derivWithin.neg]

Premises used: derivWithin.neg
-- 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 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x : 𝕜
succ : ∀ (y : 𝕜), iteratedDerivWithin n (-f) s y = (-iteratedDerivWithin n f s) y
⊢ derivWithin (iteratedDerivWithin n (-f) s) s x = derivWithin (-iteratedDerivWithin n f s) s x

Tactic:
congr with y
-- 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 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x y : 𝕜
⊢ iteratedDerivWithin n (-f) s y = (-iteratedDerivWithin n f s) y

Tactic:
IH
-- 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 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x y : 𝕜
⊢ iteratedDerivWithin n (-f) s y = (-iteratedDerivWithin n f s) y

Tactic:
exact IH
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
zero : ∀ {x : 𝕜}, iteratedDerivWithin 0 (-f) s x = -iteratedDerivWithin 0 f s x
succ :
  ∀ (n : ℕ) (IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x) {x : 𝕜},
    iteratedDerivWithin (n + 1) (-f) s x = -iteratedDerivWithin (n + 1) f s x
⊢ iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x

Tactic:
induction n generalizing x with
  | zero => simp
  | succ n IH =>
    simp only [iteratedDerivWithin_succ]
    rw [← derivWithin.neg]
    congr with y
    exact IH

Premises used: derivWithin.neg, iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ -f z) s x = -iteratedDerivWithin n f s x

Tactic:
iteratedDerivWithin_neg f

Premises used: iteratedDerivWithin_neg
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x
rw : iteratedDerivWithin n (f + -g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x
rw₁ : iteratedDerivWithin n (f + -g) s x = iteratedDerivWithin n f s x + -iteratedDerivWithin n g s x
rw₂ : iteratedDerivWithin n (f + fun (i : 𝕜) ↦ -g i) s x = iteratedDerivWithin n f s x + -iteratedDerivWithin n g s x
rw₃ :
  iteratedDerivWithin n f s x + iteratedDerivWithin n (fun (x : 𝕜) ↦ -g x) s x =
    iteratedDerivWithin n f s x + -iteratedDerivWithin n g s x
rw₄ rw₅ :
  iteratedDerivWithin n f s x + -iteratedDerivWithin n g s x =
    iteratedDerivWithin n f s x + -iteratedDerivWithin n g s x
⊢ iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, Pi.neg_def, iteratedDerivWithin_add hx h hf hg.neg,
    iteratedDerivWithin_fun_neg]

Premises used: sub_eq_add_neg, ContDiffWithinAt.neg, iteratedDerivWithin_add, Pi.neg_def, iteratedDerivWithin_fun_neg
-- 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
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑0 : WithTop ℕ∞) f s
⊢ iteratedDerivWithin 0 (fun (x : 𝕜) ↦ f (c * x)) s x = HPow.hPow (β := ℕ) c 0 • iteratedDerivWithin 0 f s (c * x)

Tactic:
simp
-- 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
⊢ c * x ∈ s

Tactic:
have hcx : c * x ∈ s := hs hx
-- 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
⊢ 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

Tactic:
have h₀ : s.EqOn
        (iteratedDerivWithin n (fun x ↦ f (c * x)) s)
        (fun x => c ^ n • iteratedDerivWithin n f s (c * x)) :=
      fun x hx => ih hx hf.of_succ
-- 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
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)

Tactic:
have h₁ : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x) :=
      hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) h _ hcx
-- 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)
rw : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s ∘ HMul.hMul c) s x
⊢ DifferentiableWithinAt.{u_1, u_1, u_2} 𝕜 (F := F) (fun (x : 𝕜) ↦ iteratedDerivWithin n f s (c * x)) s x

Tactic:
rw [← Function.comp_def]

Premises used: Function.comp_def
-- 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)
⊢ DifferentiableWithinAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ c * x) s x

Tactic:
fun_prop
-- 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)
apply : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s ∘ HMul.hMul c) s x

Tactic:
apply DifferentiableWithinAt.comp _ ?_ (by fun_prop) hs

Premises used: DifferentiableWithinAt.comp
-- 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)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)

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

Premises used: Iff.mpr, Nat.lt_succ_self, ContDiffOn.differentiableOn_iteratedDerivWithin, Nat.cast_lt
-- 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)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)

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

Premises used: Iff.mpr, Nat.lt_succ_self, ContDiffOn.differentiableOn_iteratedDerivWithin, Nat.cast_lt
-- 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)
⊢ DifferentiableWithinAt.{u_1, u_1, u_2} 𝕜 (F := F) (fun (x : 𝕜) ↦ iteratedDerivWithin n f s (c * x)) s x

Tactic:
have h₂ : DifferentiableWithinAt 𝕜 (fun x => iteratedDerivWithin n f s (c * x)) s x := by
      rw [← Function.comp_def]
      apply DifferentiableWithinAt.comp _ ?_ (by fun_prop) hs
      exact hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) h _ hcx
-- 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
⊢ DifferentiableWithinAt 𝕜 (HMul.hMul c) s x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
hf : ContDiffOn 𝕜 (↑n : WithTop ℕ∞) f s
c : 𝕜
hs : Set.MapsTo (fun (x : 𝕜) ↦ c * x) s s
zero :
  ∀ {x : 𝕜} (hx : x ∈ s) (hf : ContDiffOn 𝕜 (↑0 : WithTop ℕ∞) f s),
    iteratedDerivWithin 0 (fun (x : 𝕜) ↦ f (c * x)) s x = HPow.hPow (β := ℕ) c 0 • iteratedDerivWithin 0 f s (c * x)
succ :
  ∀ (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),
    iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
⊢ iteratedDerivWithin n (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)

Tactic:
induction n generalizing x with
  | zero => simp
  | succ n ih =>
    have hcx : c * x ∈ s := hs hx
    have h₀ : s.EqOn
        (iteratedDerivWithin n (fun x ↦ f (c * x)) s)
        (fun x => c ^ n • iteratedDerivWithin n f s (c * x)) :=
      fun x hx => ih hx hf.of_succ
    have h₁ : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x) :=
      hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) h _ hcx
    have h₂ : DifferentiableWithinAt 𝕜 (fun x => iteratedDerivWithin n f s (c * x)) s x := by
      rw [← Function.comp_def]
      apply DifferentiableWithinAt.comp _ ?_ (by fun_prop) hs
      exact hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) h _ hcx
    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', pow_succ, smul_smul, Function.comp_def, iteratedDerivWithin_succ, mul_one, derivWithin_const_mul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
s : Set 𝕜
f : 𝕜 → F
a : 𝕜
⊢ iteratedDerivWithin n (fun (x : 𝕜) ↦ f (-x)) s a = HPow.hPow (α := 𝕜) (-1) n • iteratedDerivWithin n f (-s) (-a)

Tactic:
simp [iteratedDerivWithin, iteratedFDerivWithin_comp_neg n a]

Premises used: iteratedDerivWithin, iteratedFDerivWithin_comp_neg
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
s : Set 𝕜
f : 𝕜 → F
c : 𝕜
h : ∀ (x : 𝕜), iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c + z)) s x = iteratedDerivWithin n f (c +ᵥ s) (c + x)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c + z)) s) fun (x : 𝕜) ↦
    iteratedDerivWithin n f (c +ᵥ s) (c + x)

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
s : Set 𝕜
f : 𝕜 → F
c x : 𝕜
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c + z)) s x = iteratedDerivWithin n f (c +ᵥ s) (c + x)

Tactic:
simp [iteratedDerivWithin, ← iteratedFDerivWithin_comp_add_left n c x]

Premises used: iteratedFDerivWithin_comp_add_left, iteratedDerivWithin
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
s : Set 𝕜
f : 𝕜 → F
c : 𝕜
h : ∀ (x : 𝕜), iteratedDerivWithin n (fun (z : 𝕜) ↦ f (z + c)) s x = iteratedDerivWithin n f (c +ᵥ s) (x + c)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDerivWithin n (fun (z : 𝕜) ↦ f (z + c)) s) fun (x : 𝕜) ↦
    iteratedDerivWithin n f (c +ᵥ s) (x + c)

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
s : Set 𝕜
f : 𝕜 → F
c x : 𝕜
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ f (z + c)) s x = iteratedDerivWithin n f (c +ᵥ s) (x + c)

Tactic:
simp [iteratedDerivWithin, ← iteratedFDerivWithin_comp_add_right n c x]

Premises used: iteratedDerivWithin, iteratedFDerivWithin_comp_add_right
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
s : Set 𝕜
f : 𝕜 → F
c : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDerivWithin n (fun (z : 𝕜) ↦ f (z - c)) s) fun (x : 𝕜) ↦
    iteratedDerivWithin n f (-c +ᵥ s) (x - c)

Tactic:
simpa only [sub_eq_add_neg] using iteratedDerivWithin_comp_add_const (-c)

Premises used: iteratedDerivWithin_comp_add_const, sub_eq_add_neg, Neg.neg