awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ ∑ k ∈ Finset.range n,
          n.choose (k + 1) •
            iteratedDerivWithin (k + 1) f s x • iteratedDerivWithin (n - (k + 1)) (derivWithin g s) s x +
        n.choose 0 • iteratedDerivWithin 0 f s x • iteratedDerivWithin (n - 0) (derivWithin g s) s x +
      ∑ i ∈ Finset.range (n + 1),
        n.choose i • iteratedDerivWithin i (derivWithin f s) s x • iteratedDerivWithin (n - i) g s x =
    ∑ x_1 ∈ Finset.range (n + 1),
          n.choose x_1 • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n + 1 - (x_1 + 1)) g s x +
        (∑ x_1 ∈ Finset.range n,
            n.choose (x_1 + 1) • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n + 1 - (x_1 + 1)) g s x +
          n.choose (n + 1) • iteratedDerivWithin (n + 1) f s x • iteratedDerivWithin (n + 1 - (n + 1)) g s x) +
      (n + 1).choose 0 • iteratedDerivWithin 0 f s x • iteratedDerivWithin (n + 1 - 0) g s x
have this : ∀ i ∈ Finset.range n, 1 ≤ n - i
Tactic: have : ∀ i ∈ Finset.range n, 1 ≤ n - i := by simp; lia
-- 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
this : ∀ i ∈ Finset.range n, 1 ≤ n - i
⊢ ∑ k ∈ Finset.range n,
          n.choose (k + 1) •
            iteratedDerivWithin (k + 1) f s x • iteratedDerivWithin (n - (k + 1)) (derivWithin g s) s x +
        n.choose 0 • iteratedDerivWithin 0 f s x • iteratedDerivWithin (n - 0) (derivWithin g s) s x +
      ∑ i ∈ Finset.range (n + 1),
        n.choose i • iteratedDerivWithin i (derivWithin f s) s x • iteratedDerivWithin (n - i) g s x =
    ∑ x_1 ∈ Finset.range (n + 1),
          n.choose x_1 • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n + 1 - (x_1 + 1)) g s x +
        (∑ x_1 ∈ Finset.range n,
            n.choose (x_1 + 1) • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n + 1 - (x_1 + 1)) g s x +
          n.choose (n + 1) • iteratedDerivWithin (n + 1) f s x • iteratedDerivWithin (n + 1 - (n + 1)) g s x) +
      (n + 1).choose 0 • iteratedDerivWithin 0 f s x • iteratedDerivWithin (n + 1 - 0) g s x
have succ : ∑ x_1 ∈ Finset.range n, n.choose (x_1 + 1) • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n - x_1) g s x +
      f x • iteratedDerivWithin (n + 1) g s x +
    ∑ x_1 ∈ Finset.range (n + 1),
      n.choose x_1 • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n - x_1) g s x =
  HAdd.hAdd (α := F)
      (∑ x_1 ∈ Finset.range (n + 1),
        n.choose x_1 • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n - x_1) g s x)
      (∑ x_1 ∈ Finset.range n,
        n.choose (x_1 + 1) • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n - x_1) g s x) +
    f x • iteratedDerivWithin (n + 1) g s x
Tactic: simp +contextual [← iteratedDerivWithin_succ', ← n.sub_sub, Nat.sub_add_cancel, this]
-- 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 : ℕ
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
funProp : UniqueDiffOn 𝕜 s
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin f s) s x
have funProp₁ : HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 ≤ (↑(n + 1) : WithTop ℕ∞)
Tactic: fun_prop (disch := simp_all)
-- 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 : ℕ
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x
have funProp : LE.le (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
Tactic: fun_prop (disch := simp_all)
-- 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 : ℕ
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
have funProp : LE.le (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
Tactic: fun_prop (disch := simp_all)
-- 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 : ℕ
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
funProp : UniqueDiffOn 𝕜 s
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin g s) s x
have funProp₁ : HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 ≤ (↑(n + 1) : WithTop ℕ∞)
Tactic: fun_prop (disch := simp_all)
-- 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 : ℕ
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f • derivWithin g s) s x
have funProp : LE.le (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
Tactic: fun_prop (disch := simp_all)
-- 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 : ℕ
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
funProp : LE.le (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
funProp₁ : UniqueDiffOn 𝕜 s
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f • derivWithin g s) s x
have funProp₂ : HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 ≤ (↑(n + 1) : WithTop ℕ∞)
Tactic: fun_prop (disch := simp_all)
-- 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 : ℕ
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
funProp : UniqueDiffOn 𝕜 s
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin f s • g) s x
have funProp₁ : HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 ≤ (↑(n + 1) : WithTop ℕ∞)
Tactic: fun_prop (disch := simp_all)
-- 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 : ℕ
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
funProp : UniqueDiffOn 𝕜 s
funProp₁ : HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 ≤ (↑(n + 1) : WithTop ℕ∞)
funProp₂ : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin f s • g) s x
have funProp₃ : LE.le (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
Tactic: fun_prop (disch := simp_all)
-- 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
⊢ derivWithin (f • g) s =ᶠ[𝓝[insert x s] x] f • derivWithin g s + derivWithin f s • g
have h₁ : ∀ (y : 𝕜) (hfy : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s y)
  (hgy : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s y),
  derivWithin (f • g) s y = (f • derivWithin g s + derivWithin f s • g) y
Tactic: filter_upwards [hf.eventually (by simp), hg.eventually (by simp)] with y hfy hgy
-- 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
y : 𝕜
hfy : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s y
hgy : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s y
⊢ derivWithin (f • g) s y = (f • derivWithin g s + derivWithin f s • g) y
have h₁ : f y • derivWithin g s y + derivWithin f s y • g y = (f • derivWithin g s + derivWithin f s • g) y
Tactic: rw [derivWithin_smul (hfy.differentiableWithinAt _) (hgy.differentiableWithinAt _)]
-- 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
y : 𝕜
hfy : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s y
hgy : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s y
h₁ : f y • derivWithin g s y + derivWithin f s y • g y = (f • derivWithin g s + derivWithin f s • g) y
⊢ derivWithin (f • g) s y = (f • derivWithin g s + derivWithin f s • g) y
have rw : Ne (α := WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞) 0
Tactic: rw [derivWithin_smul (hfy.differentiableWithinAt _) (hgy.differentiableWithinAt _)]
-- 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
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
inst_5 : Module 𝔸 F
inst_6 : IsBoundedSMul 𝔸 F
inst_7 : IsScalarTower 𝕜 𝔸 F
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
have zero : ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F} (hf : ContDiffWithinAt 𝕜 (↑0 : WithTop ℕ∞) f s x)
  (hg : ContDiffWithinAt 𝕜 (↑0 : WithTop ℕ∞) g s x),
  iteratedDerivWithin 0 (f • g) s x =
    ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      Nat.choose 0 i • iteratedDerivWithin i f s x • iteratedDerivWithin (0 - i) g s x
Tactic: induction n generalizing f g with
  | zero => simp
  | succ n IH =>
    obtain ⟨U, hU, H⟩ := ((hf.eventually (by simp)).and (hg.eventually (by simp))).exists_mem
    rw [iteratedDerivWithin_succ', Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert
        (g := f • derivWithin g s + derivWithin f s • g)]
    · rw [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]
      · simp only [Nat.choose_succ_succ', add_smul, Finset.sum_add_distrib]
        nth_rw 3 [Finset.sum_range_succ]
        have : ∀ i ∈ Finset.range n, 1 ≤ n - i := by simp; lia
        simp +contextual [← iteratedDerivWithin_succ', ← n.sub_sub, Nat.sub_add_cancel, this]
        abel
      all_goals clear IH H U hU; fun_prop (disch := simp_all)
    · filter_upwards [hf.eventually (by simp), hg.eventually (by simp)] with y hfy hgy
      rw [derivWithin_smul (hfy.differentiableWithinAt _) (hgy.differentiableWithinAt _)]
      all_goals simp
Cleared hypotheses: f, g, hf, hg
-- 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
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
inst_5 : Module 𝔸 F
inst_6 : IsBoundedSMul 𝔸 F
inst_7 : IsScalarTower 𝕜 𝔸 F
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x
zero :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F} (hf : ContDiffWithinAt 𝕜 (↑0 : WithTop ℕ∞) f s x)
    (hg : ContDiffWithinAt 𝕜 (↑0 : WithTop ℕ∞) g s x),
    iteratedDerivWithin 0 (f • g) s x =
      ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
        Nat.choose 0 i • iteratedDerivWithin i f s x • iteratedDerivWithin (0 - i) 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
have succ : ∀ (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
Tactic: induction n generalizing f g with
  | zero => simp
  | succ n IH =>
    obtain ⟨U, hU, H⟩ := ((hf.eventually (by simp)).and (hg.eventually (by simp))).exists_mem
    rw [iteratedDerivWithin_succ', Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert
        (g := f • derivWithin g s + derivWithin f s • g)]
    · rw [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]
      · simp only [Nat.choose_succ_succ', add_smul, Finset.sum_add_distrib]
        nth_rw 3 [Finset.sum_range_succ]
        have : ∀ i ∈ Finset.range n, 1 ≤ n - i := by simp; lia
        simp +contextual [← iteratedDerivWithin_succ', ← n.sub_sub, Nat.sub_add_cancel, this]
        abel
      all_goals clear IH H U hU; fun_prop (disch := simp_all)
    · filter_upwards [hf.eventually (by simp), hg.eventually (by simp)] with y hfy hgy
      rw [derivWithin_smul (hfy.differentiableWithinAt _) (hgy.differentiableWithinAt _)]
      all_goals simp
Cleared hypotheses: f, g, hf, hg
-- 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
k : ℕ
⊢ iteratedDerivWithin k (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x = (↑(Nat.descFactorial 0 k) : 𝕜) * x ^ (0 - k)
have zero : iteratedDerivWithin 0 (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x =
  (↑(Nat.descFactorial 0 0) : 𝕜) * x ^ HSub.hSub (α := ℕ) 0 0
Tactic: cases k
Cleared hypotheses: k
-- 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
k : ℕ
zero :
  iteratedDerivWithin 0 (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x =
    (↑(Nat.descFactorial 0 0) : 𝕜) * x ^ HSub.hSub (α := ℕ) 0 0
⊢ iteratedDerivWithin k (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x = (↑(Nat.descFactorial 0 k) : 𝕜) * x ^ (0 - k)
have zero₁ : ∀ (n : ℕ),
  iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x =
    (↑(Nat.descFactorial 0 (n + 1)) : 𝕜) * x ^ (0 - (n + 1))
Tactic: cases k
Cleared hypotheses: k
-- 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
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
⊢ iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ (i + 1)) s x = (↑((i + 1).descFactorial k) : 𝕜) * x ^ (i + 1 - k)
have succ : iteratedDerivWithin 0 (fun (x : 𝕜) ↦ x ^ (i + 1)) s x = (↑((i + 1).descFactorial 0) : 𝕜) * x ^ (i + 1 - 0)
Tactic: obtain (_ | k) := k
Cleared hypotheses: k
-- 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
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
succ : iteratedDerivWithin 0 (fun (x : 𝕜) ↦ x ^ (i + 1)) s x = (↑((i + 1).descFactorial 0) : 𝕜) * x ^ (i + 1 - 0)
⊢ iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ (i + 1)) s x = (↑((i + 1).descFactorial k) : 𝕜) * x ^ (i + 1 - k)
have succ₁ : ∀ (k : ℕ),
  iteratedDerivWithin (k + 1) (fun (x : 𝕜) ↦ x ^ (i + 1)) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
Tactic: obtain (_ | k) := k
Cleared hypotheses: k
-- 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
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
⊢ iteratedDerivWithin (k + 1) (fun (x : 𝕜) ↦ x ^ (i + 1)) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
have succ : iteratedDerivWithin (k + 1) (fun (x : 𝕜) ↦ x ^ i * x) s x =
  (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
Tactic: simp only [pow_succ]
-- 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
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
⊢ iteratedDerivWithin (k + 1) (fun (x : 𝕜) ↦ x ^ i * x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
have succ : ∑ i_1 ∈ Finset.range (k + 1 + 1),
    HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
      iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
  (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
Tactic: refine (iteratedDerivWithin_mul hx h (by fun_prop) (by fun_prop)).trans ?_
-- 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
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
⊢ (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
have rw : (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
Tactic: rw [Nat.succ_descFactorial_succ]
-- 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
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
have inl : k ≤ i → (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
Tactic: cases le_or_gt k i