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 𝕜
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have 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)
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)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have succ₇ : c ^ n • (c * 1) • 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]
-- 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)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have succ₈ : (c ^ n * (c * 1)) • 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]
-- 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)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have succ₉ : (c ^ n * c) • 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]
-- 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)
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)
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
have succ₁₀ : (c ^ n * c) • derivWithin (iteratedDerivWithin n f s) s (c * x) =
  (c ^ n * c) • 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
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
⊢ iteratedDerivWithin n (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
have 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)
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]
Cleared hypotheses: n, x, hx, hf
-- 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 : 𝕜 → 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)
⊢ iteratedDerivWithin n (fun (x : 𝕜) ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
have 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)
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]
Cleared hypotheses: n, x, hx, hf
-- 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 : ℕ
s : Set 𝕜
f : 𝕜 → F
c : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c + z)) s) fun (x : 𝕜) ↦
    iteratedDerivWithin n f (c +ᵥ s) (c + x)
have h : ∀ (x : 𝕜), iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c + z)) s x = iteratedDerivWithin n f (c +ᵥ s) (c + x)
Tactic: ext 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 : ℕ
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)
have h : ∀ (x : 𝕜), iteratedDerivWithin n (fun (z : 𝕜) ↦ f (z + c)) s x = iteratedDerivWithin n f (c +ᵥ s) (x + c)
Tactic: ext 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 : ℕ
s : Set 𝕜
f : 𝕜 → F
c : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c - z)) s) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) n • iteratedDerivWithin n f (c +ᵥ -s) (c - x)
have h : ∀ (a : 𝕜),
  iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c - z)) s a =
    HPow.hPow (α := 𝕜) (-1) n • iteratedDerivWithin n f (c +ᵥ -s) (c - a)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
⊢ iteratedDerivWithin n id s x = if n = 0 then x else if n = 1 then 1 else 0
have zero : iteratedDerivWithin 0 id s x = if Eq (α := ℕ) 0 0 then x else if Eq (α := ℕ) 0 1 then 1 else 0
Tactic: obtain (_ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
zero : iteratedDerivWithin 0 id s x = if Eq (α := ℕ) 0 0 then x else if Eq (α := ℕ) 0 1 then 1 else 0
⊢ iteratedDerivWithin n id s x = if n = 0 then x else if n = 1 then 1 else 0
have succ : ∀ (n : ℕ), iteratedDerivWithin (n + 1) id s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0
Tactic: obtain (_ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin (n + 1) id s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0
have succ : iteratedDerivWithin n (fun (x : 𝕜) ↦ 1) s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0
Tactic: rw [iteratedDerivWithin_succ', iteratedDerivWithin_congr (g := fun _ ↦ 1) _ hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
succ : iteratedDerivWithin n (fun (x : 𝕜) ↦ 1) s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0
⊢ iteratedDerivWithin (n + 1) id s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0
have rw : Set.EqOn (derivWithin id s) (fun (x : 𝕜) ↦ 1) s
Tactic: rw [iteratedDerivWithin_succ', iteratedDerivWithin_congr (g := fun _ ↦ 1) _ hx]
-- 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_1 : ℕ
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
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F} (hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x)
    (hg : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x),
    iteratedDerivWithin n (f • g) s x =
      ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
⊢ iteratedDerivWithin (n + 1) (f • g) s x =
    ∑ i ∈ Finset.range (n + 1 + 1),
      (n + 1).choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n + 1 - i) g s x
have succ : ∀ (U : Set 𝕜) (hU : U ∈ 𝓝[insert x s] x)
  (H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s y),
  iteratedDerivWithin (n + 1) (f • g) s x =
    ∑ i ∈ Finset.range (n + 1 + 1),
      (n + 1).choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n + 1 - i) g s x
Tactic: obtain ⟨U, hU, H⟩ := ((hf.eventually (by simp)).and (hg.eventually (by simp))).exists_mem
-- 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_1 : ℕ
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
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F} (hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x)
    (hg : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x),
    iteratedDerivWithin n (f • g) s x =
      ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s y
⊢ iteratedDerivWithin (n + 1) (f • g) s x =
    ∑ i ∈ Finset.range (n + 1 + 1),
      (n + 1).choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n + 1 - i) g s x
have succ : iteratedDerivWithin n (f • derivWithin g s + derivWithin f s • g) s x =
  ∑ i ∈ Finset.range (n + 1 + 1), (n + 1).choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n + 1 - i) g s x
Tactic: rw [iteratedDerivWithin_succ', Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert
        (g := f • derivWithin g s + derivWithin f s • g)]