awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDeriv 3 (g ∘ f) x =
    HPow.hPow (β := ℕ) (deriv f x) 3 • iteratedDeriv 3 g (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDeriv 2 f x • deriv f x • iteratedDeriv 2 g (f x)) +
      iteratedDeriv 3 f x • deriv g (f x)
have simp : iteratedDerivWithin 3 (g ∘ f) univ x =
  HPow.hPow (β := ℕ) (derivWithin f univ x) 3 • iteratedDerivWithin 3 g univ (f x) +
      HSMul.hSMul (α := ℕ) 3
        (iteratedDerivWithin 2 f univ x • derivWithin f univ x • iteratedDerivWithin 2 g univ (f x)) +
    iteratedDerivWithin 3 f univ x • derivWithin g univ (f x)
Tactic: simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : (↑i : ℕ∞ω) ≤ n
⊢ iteratedDerivWithin i (g ∘ f) s x =
    ∑ c : OrderedFinpartition i,
      iteratedDerivWithin c.length g t (f x) * ∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x
have rw : Eq.{u_1 + 1} (α := 𝕜)
  (∑ c : OrderedFinpartition i,
    HSMul.hSMul (α := 𝕜) (∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
      (iteratedDerivWithin c.length g t (f x)))
  (∑ c : OrderedFinpartition i,
    iteratedDerivWithin c.length g t (f x) * ∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
Tactic: rw [iteratedDerivWithin_scomp_eq_sum_orderedFinpartition hg hf ht hs hx hst hi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
⊢ iteratedDeriv i (g ∘ f) x =
    ∑ c : OrderedFinpartition i, iteratedDeriv c.length g (f x) * ∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x
have rw : Eq.{u_1 + 1} (α := 𝕜)
  (∑ c : OrderedFinpartition i,
    HSMul.hSMul (α := 𝕜) (∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x) (iteratedDeriv c.length g (f x)))
  (∑ c : OrderedFinpartition i, iteratedDeriv c.length g (f x) * ∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x)
Tactic: rw [iteratedDeriv_scomp_eq_sum_orderedFinpartition hg hf hi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 2 g t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ iteratedDerivWithin 2 (g ∘ f) s x =
    iteratedDerivWithin 2 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 2 +
      derivWithin g t (f x) * iteratedDerivWithin 2 f s x
have rw : HPow.hPow (β := ℕ) (derivWithin f s x) 2 • iteratedDerivWithin 2 g t (f x) +
    iteratedDerivWithin 2 f s x • derivWithin g t (f x) =
  iteratedDerivWithin 2 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 2 +
    derivWithin g t (f x) * iteratedDerivWithin 2 f s x
Tactic: rw [iteratedDerivWithin_scomp_two hg hf ht hs hx hst]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDeriv 2 (g ∘ f) x =
    iteratedDeriv 2 g (f x) * HPow.hPow (β := ℕ) (deriv f x) 2 + deriv g (f x) * iteratedDeriv 2 f x
have simp : iteratedDerivWithin 2 (g ∘ f) univ x =
  iteratedDerivWithin 2 g univ (f x) * HPow.hPow (β := ℕ) (derivWithin f univ x) 2 +
    derivWithin g univ (f x) * iteratedDerivWithin 2 f univ x
Tactic: simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ iteratedDerivWithin 3 (g ∘ f) s x =
    iteratedDerivWithin 3 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 3 +
        3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
      derivWithin g t (f x) * iteratedDerivWithin 3 f s x
have rw : HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
      HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
    iteratedDerivWithin 3 f s x • derivWithin g t (f x) =
  iteratedDerivWithin 3 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 3 +
      3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
    derivWithin g t (f x) * iteratedDerivWithin 3 f s x
Tactic: rw [iteratedDerivWithin_scomp_three hg hf ht hs hx hst]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
      iteratedDerivWithin 3 f s x • derivWithin g t (f x) =
    iteratedDerivWithin 3 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 3 +
        3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
      derivWithin g t (f x) * iteratedDerivWithin 3 f s x
have simp : HPow.hPow (β := ℕ) (derivWithin f s x) 3 * iteratedDerivWithin 3 g t (f x) +
      3 * (iteratedDerivWithin 2 f s x * (derivWithin f s x * iteratedDerivWithin 2 g t (f x))) +
    iteratedDerivWithin 3 f s x * derivWithin g t (f x) =
  iteratedDerivWithin 3 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 3 +
      3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
    derivWithin g t (f x) * iteratedDerivWithin 3 f s x
Tactic: simp only [nsmul_eq_mul, smul_eq_mul, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDeriv 3 (g ∘ f) x =
    iteratedDeriv 3 g (f x) * HPow.hPow (β := ℕ) (deriv f x) 3 +
        3 * iteratedDeriv 2 g (f x) * iteratedDeriv 2 f x * deriv f x +
      deriv g (f x) * iteratedDeriv 3 f x
have simp : iteratedDerivWithin 3 (g ∘ f) univ x =
  iteratedDerivWithin 3 g univ (f x) * HPow.hPow (β := ℕ) (derivWithin f univ x) 3 +
      3 * iteratedDerivWithin 2 g univ (f x) * iteratedDerivWithin 2 f univ x * derivWithin f univ x +
    derivWithin g univ (f x) * iteratedDerivWithin 3 f univ x
Tactic: simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]
-- 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
x : 𝕜
f g : 𝕜 → F
s t : Set 𝕜
h : f =ᶠ[𝓝[s] x] g
ht : t ⊆ s
n : ℕ
⊢ iteratedDerivWithin n f t =ᶠ[𝓝[s] x] iteratedDerivWithin n g t
have unfold : EventuallyEq.{u_1, u_2} (β := F) (𝓝[s] x)
  (fun (x : 𝕜) ↦ (iteratedFDerivWithin 𝕜 n f t x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) fun (x : 𝕜) ↦
  (iteratedFDerivWithin 𝕜 n g t x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1
Tactic: unfold iteratedDerivWithin
-- 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 simp_rw : ((iteratedFDerivWithin 𝕜 n (f + g) s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) =
  HAdd.hAdd (α := F) (β := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
    ((iteratedFDerivWithin 𝕜 n g s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: simp_rw [iteratedDerivWithin, iteratedFDerivWithin_add_apply hf hg h hx,
    ContinuousMultilinearMap.add_apply]
-- 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
simp_rw :
  ((iteratedFDerivWithin 𝕜 n (f + g) s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) =
    HAdd.hAdd (α := F) (β := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
      ((iteratedFDerivWithin 𝕜 n g s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
⊢ iteratedDerivWithin n (f + g) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x
have simp_rw₁ : ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x)
        (iteratedFDerivWithin 𝕜 n g s x) :
      (a : (i : Fin n) → 𝕜) → F)
    fun (x : Fin n) ↦ 1) =
  HAdd.hAdd (α := F) (β := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
    ((iteratedFDerivWithin 𝕜 n g s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: simp_rw [iteratedDerivWithin, iteratedFDerivWithin_add_apply hf hg h hx,
    ContinuousMultilinearMap.add_apply]
-- 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
hn : 0 < n
c : F
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ c + f z) s x = iteratedDerivWithin n f s x
have obtain : ∀ (n : ℕ) (hn : 0 < n.succ), iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ c + f z) s x = iteratedDerivWithin n.succ f s x
Tactic: obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn.ne'
Cleared hypotheses: n, hn
-- 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
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ c + f z) s x = iteratedDerivWithin n.succ f s x
have rw : iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ c + f z) s) s x = iteratedDerivWithin n (derivWithin f s) s x
Tactic: rw [iteratedDerivWithin_succ', iteratedDerivWithin_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
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ c + f z) s) s x = iteratedDerivWithin n (derivWithin f s) s x
have e_f : ∀ (y : 𝕜), derivWithin (fun (z : 𝕜) ↦ c + f z) s y = derivWithin f s y
Tactic: congr 1 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
hn : 0 < n
c : F
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (fun (z : 𝕜) ↦ c - f z) s x)
    (iteratedDerivWithin n (fun (z : 𝕜) ↦ -f z) s x)
have obtain : ∀ (n : ℕ) (hn : 0 < n.succ),
  Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ c - f z) s x)
    (iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ -f z) s x)
Tactic: obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn.ne'
Cleared hypotheses: n, hn
-- 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
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ c - f z) s x)
    (iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ -f z) s x)
have rw : Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ c - f z) s) s x)
  (iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ -f z) s) s x)
Tactic: rw [iteratedDerivWithin_succ', iteratedDerivWithin_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
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ c - f z) s) s x)
    (iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ -f z) s) s x)
have e_f : ∀ (y : 𝕜), Eq.{u_2 + 1} (α := F) (derivWithin (fun (z : 𝕜) ↦ c - f z) s y) (derivWithin (fun (z : 𝕜) ↦ -f z) s y)
Tactic: congr 1 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
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
y : 𝕜
⊢ Eq.{u_2 + 1} (α := F) (derivWithin (fun (z : 𝕜) ↦ c - f z) s y) (derivWithin (fun (z : 𝕜) ↦ -f z) s y)
have e_f : derivWithin (fun (z : 𝕜) ↦ c - f z) s y = -derivWithin f s y
Tactic: rw [derivWithin.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 : 𝕜 → F
R : Type u_3
inst_3 : DistribSMul R F
inst_4 : SMulCommClass 𝕜 R F
inst_5 : ContinuousConstSMul R F
c : R
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
⊢ iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
have simp_rw : ((iteratedFDerivWithin 𝕜 n (c • f) s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) =
  HSMul.hSMul (β := F) c ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: simp_rw [iteratedDerivWithin]
-- 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
R : Type u_3
inst_3 : DistribSMul R F
inst_4 : SMulCommClass 𝕜 R F
inst_5 : ContinuousConstSMul R F
c : R
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
⊢ ((iteratedFDerivWithin 𝕜 n (c • f) s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) =
    HSMul.hSMul (β := F) c ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
have rw : ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) c (iteratedFDerivWithin 𝕜 n f s x) :
      (a : (i : Fin n) → 𝕜) → F)
    fun (x : Fin n) ↦ 1) =
  HSMul.hSMul (β := F) c ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
Tactic: rw [iteratedFDerivWithin_const_smul_apply (a := c) hf h 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
s : Set 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
x : 𝕜
f : 𝕜 → F
⊢ iteratedDerivWithin (n + 1) (c • f) s x = c • iteratedDerivWithin (n + 1) f s x
have succ : derivWithin (iteratedDerivWithin n (c • f) s) s x = c • derivWithin (iteratedDerivWithin n f s) s x
Tactic: simp_rw [iteratedDerivWithin_succ, funext (@IH · f), ← Pi.smul_def,
      derivWithin_const_smul_field]
-- 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 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
x : 𝕜
f : 𝕜 → F
succ : derivWithin (iteratedDerivWithin n (c • f) s) s x = c • derivWithin (iteratedDerivWithin n f s) s x
⊢ iteratedDerivWithin (n + 1) (c • f) s x = c • iteratedDerivWithin (n + 1) f s x
have succ₁ : derivWithin (fun (x : 𝕜) ↦ c • iteratedDerivWithin n f s x) s x = c • derivWithin (iteratedDerivWithin n f s) s x
Tactic: simp_rw [iteratedDerivWithin_succ, funext (@IH · f), ← Pi.smul_def,
      derivWithin_const_smul_field]
-- 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 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
x : 𝕜
f : 𝕜 → F
succ : derivWithin (iteratedDerivWithin n (c • f) s) s x = c • derivWithin (iteratedDerivWithin n f s) s x
succ₁ :
  derivWithin (fun (x : 𝕜) ↦ c • iteratedDerivWithin n f s x) s x = c • derivWithin (iteratedDerivWithin n f s) s x
⊢ iteratedDerivWithin (n + 1) (c • f) s x = c • iteratedDerivWithin (n + 1) f s x
have succ₂ : derivWithin (c • iteratedDerivWithin n f s) s x = c • derivWithin (iteratedDerivWithin n f s) s x
Tactic: simp_rw [iteratedDerivWithin_succ, funext (@IH · f), ← Pi.smul_def,
      derivWithin_const_smul_field]
-- 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 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
⊢ iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
have zero : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin 0 (c • f) s x = c • iteratedDerivWithin 0 f s x
Tactic: induction n generalizing f x with
  | zero => simp
  | succ n IH =>
    simp_rw [iteratedDerivWithin_succ, funext (@IH · f), ← Pi.smul_def,
      derivWithin_const_smul_field]
Cleared hypotheses: n, x, f
-- 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 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
zero : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin 0 (c • f) s x = c • iteratedDerivWithin 0 f s x
⊢ iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
have succ : ∀ (n : ℕ) (IH : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x) {x : 𝕜}
  (f : 𝕜 → F), iteratedDerivWithin (n + 1) (c • f) s x = c • iteratedDerivWithin (n + 1) f s x
Tactic: induction n generalizing f x with
  | zero => simp
  | succ n IH =>
    simp_rw [iteratedDerivWithin_succ, funext (@IH · f), ← Pi.smul_def,
      derivWithin_const_smul_field]
Cleared hypotheses: n, x, f
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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 : 𝕜 → 𝕜'
⊢ iteratedDerivWithin (n + 1) (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin (n + 1) f s x * d
have succ : derivWithin (iteratedDerivWithin n (fun (z : 𝕜) ↦ f z * d) s) s x = derivWithin (iteratedDerivWithin n f s) s x * d
Tactic: simp_rw [iteratedDerivWithin_succ, funext (@IH · f), derivWithin_mul_const_field]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
⊢ iteratedDerivWithin (n + 1) (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin (n + 1) f s x * d
have succ₁ : derivWithin (fun (x : 𝕜) ↦ iteratedDerivWithin n f s x * d) s x = derivWithin (iteratedDerivWithin n f s) s x * d
Tactic: simp_rw [iteratedDerivWithin_succ, funext (@IH · f), derivWithin_mul_const_field]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
𝕜' : Type u_6
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
d : 𝕜'
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin n f s x * d
have zero : ∀ {x : 𝕜} (f : 𝕜 → 𝕜'), iteratedDerivWithin 0 (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin 0 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]
Cleared hypotheses: n, x, f
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
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
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ f z * d) s x = iteratedDerivWithin n f s x * d
have 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
Tactic: induction n generalizing f x with
  | zero => simp
  | succ n IH =>
    simp_rw [iteratedDerivWithin_succ, funext (@IH · f), derivWithin_mul_const_field]
Cleared hypotheses: n, x, f
-- 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 : 𝕜
⊢ iteratedDerivWithin (n + 1) (-f) s x = -iteratedDerivWithin (n + 1) f s x
have succ : derivWithin (iteratedDerivWithin n (-f) s) s x = -derivWithin (iteratedDerivWithin n f s) s x
Tactic: simp only [iteratedDerivWithin_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 𝕜
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 : derivWithin (iteratedDerivWithin n (-f) s) s x = derivWithin (-iteratedDerivWithin n f s) s x
Tactic: rw [← derivWithin.neg]