awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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 : 𝕜
⊢ derivWithin (iteratedDerivWithin n (-f) s) s x = derivWithin (-iteratedDerivWithin n f s) s x
have succ : ∀ (y : 𝕜), iteratedDerivWithin n (-f) s y = (-iteratedDerivWithin n f s) y
Tactic: congr with y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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 (-f) s x = -iteratedDerivWithin n f s x
have zero : ∀ {x : 𝕜}, iteratedDerivWithin 0 (-f) s x = -iteratedDerivWithin 0 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
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
⊢ iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
have 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
Tactic: induction n generalizing x with
  | zero => simp
  | succ n IH =>
    simp only [iteratedDerivWithin_succ]
    rw [← derivWithin.neg]
    congr with y
    exact IH
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
⊢ iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x
have rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
⊢ iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
⊢ iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x
have rw₂ : iteratedDerivWithin n (f + fun (i : 𝕜) ↦ -g i) 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
⊢ iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x
have rw₃ : iteratedDerivWithin n f s x + iteratedDerivWithin n (fun (x : 𝕜) ↦ -g x) 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
⊢ iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x
have rw₄ : iteratedDerivWithin n f s x + -iteratedDerivWithin n 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (hypothesis)
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
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have hcx : c * x ∈ s
Tactic: have hcx : c * x ∈ s := hs hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (hypothesis)
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
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (hypothesis)
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
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have h₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
have rw : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s ∘ HMul.hMul c) s x
Tactic: rw [← Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (hypothesis)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have h₂ : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have succ : derivWithin (iteratedDerivWithin n (fun (x : 𝕜) ↦ f (c * x)) s) 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have succ₁ : derivWithin (fun (x : 𝕜) ↦ c ^ n • iteratedDerivWithin n f s (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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have succ₄ : c ^ n • derivWithin (iteratedDerivWithin n f s ∘ HMul.hMul c) s x =
  c ^ (n + 1) • derivWithin (iteratedDerivWithin n f s) 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have 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)
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]