awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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) s x

Tactic:
fun_prop (disch := simp_all)
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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
⊢ LE.le (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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 ℕ∞)
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x

Tactic:
fun_prop (disch := simp_all)
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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 ℕ∞)
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x

Tactic:
fun_prop (disch := simp_all)
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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 g s) s x

Tactic:
fun_prop (disch := simp_all)
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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
funProp₂ : HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 ≤ (↑(n + 1) : WithTop ℕ∞)
funProp₃ : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f • derivWithin g s) s x

Tactic:
fun_prop (disch := simp_all)
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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
funProp₃ : LE.le (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin f s • g) s x

Tactic:
fun_prop (disch := simp_all)
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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
⊢ Ne (α := WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
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
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
⊢ derivWithin (f • g) s =ᶠ[𝓝[insert x s] x] f • derivWithin g s + derivWithin f s • g

Tactic:
filter_upwards [hf.eventually (by simp), hg.eventually (by simp)] with y hfy hgy

Premises used: ContDiffWithinAt.eventually
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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
rw rw₁ : Ne (α := WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞) 0
⊢ derivWithin (f • g) s y = (f • derivWithin g s + derivWithin f s • g) y

Tactic:
rw [derivWithin_smul (hfy.differentiableWithinAt _) (hgy.differentiableWithinAt _)]

Premises used: derivWithin_smul, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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
⊢ f y • derivWithin g s y + derivWithin f s y • g y = (f • derivWithin g s + derivWithin f s • g) y

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
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
⊢ Ne (α := WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
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
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
⊢ 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

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

Premises used: ContDiffWithinAt.eventually, Finset.sum_add_distrib, Filter.Eventually.and, Nat.sub_sub, Filter.Eventually.exists_mem, Nat.sub_add_cancel, add_smul, iteratedDerivWithin_succ', Nat.choose_succ_succ', iteratedDerivWithin_add, Finset.sum_range_succ', Finset.sum_range_succ, Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f g : 𝕜 → 𝔸
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

Tactic:
simp [← smul_eq_mul, iteratedDerivWithin_smul hx h hf hg]

Premises used: iteratedDerivWithin_smul, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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
zero₁ :
  ∀ (n : ℕ),
    iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x =
      (↑(Nat.descFactorial 0 (n + 1)) : 𝕜) * x ^ (0 - (n + 1))
⊢ iteratedDerivWithin k (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x = (↑(Nat.descFactorial 0 k) : 𝕜) * x ^ (0 - k)

Tactic:
cases k
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
⊢ iteratedDerivWithin 0 (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x =
    (↑(Nat.descFactorial 0 0) : 𝕜) * x ^ HSub.hSub (α := ℕ) 0 0

Tactic:
simp [iteratedDerivWithin_const]

Premises used: iteratedDerivWithin_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x =
    (↑(Nat.descFactorial 0 (n + 1)) : 𝕜) * x ^ (0 - (n + 1))

Tactic:
simp [iteratedDerivWithin_const]

Premises used: iteratedDerivWithin_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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)
succ₁ :
  ∀ (k : ℕ),
    iteratedDerivWithin (k + 1) (fun (x : 𝕜) ↦ x ^ (i + 1)) s x =
      (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
⊢ iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ (i + 1)) s x = (↑((i + 1).descFactorial k) : 𝕜) * x ^ (i + 1 - k)

Tactic:
obtain (_ | k) := k
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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)
⊢ iteratedDerivWithin 0 (fun (x : 𝕜) ↦ x ^ (i + 1)) s x = (↑((i + 1).descFactorial 0) : 𝕜) * x ^ (i + 1 - 0)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 (k + 1) (fun (x : 𝕜) ↦ x ^ i * x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))
⊢ iteratedDerivWithin (k + 1) (fun (x : 𝕜) ↦ x ^ (i + 1)) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))

Tactic:
simp only [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 : ℕ
⊢ ContDiffWithinAt 𝕜 (F := 𝕜) (↑(k + 1) : WithTop ℕ∞) (fun (x : 𝕜) ↦ x ^ i) s x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 : ℕ
⊢ ContDiffWithinAt 𝕜 (F := 𝕜) (↑(k + 1) : WithTop ℕ∞) (fun (x : 𝕜) ↦ x) s x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 :
  ∑ 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))
⊢ iteratedDerivWithin (k + 1) (fun (x : 𝕜) ↦ x ^ i * 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 ?_

Premises used: iteratedDerivWithin_mul, Eq.trans
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 : ℕ
rw : (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
⊢ (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)

Tactic:
rw [Nat.succ_descFactorial_succ]

Premises used: Nat.succ_descFactorial_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 : ℕ
inl : k ≤ i → (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
inr : i < k → (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)

Tactic:
cases le_or_gt k i

Premises used: le_or_gt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 : ℕ
h_1 : k ≤ i
inl : i + 1 = k + 1 + (i - k) ∨ i < k
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)

Tactic:
simp [Nat.descFactorial, ← add_mul, *]

Premises used: add_mul, Nat.descFactorial
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 : ℕ
h_1 : i < k
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)

Tactic:
simp [Nat.descFactorial, ← add_mul, *]

Premises used: add_mul, Nat.descFactorial
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 : ℕ
h_1 : k ≤ i
⊢ i + 1 = k + 1 + (i - k) ∨ i < k

Tactic:
lia
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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)

Tactic:
have : ((i + 1).descFactorial (k + 1)) =
        (k + 1) * (i.descFactorial k) + (i.descFactorial (k + 1)) := by
      rw [Nat.succ_descFactorial_succ]
      cases le_or_gt k i <;> simp [Nat.descFactorial, ← add_mul, *]; lia
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
succ :
  ∀ (hik : i ≤ k),
    ∑ 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))
succ₁ :
  ∀ (hik : k < i),
    ∑ 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))
⊢ ∑ 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:
obtain hik | hik := le_or_gt i k

Premises used: le_or_gt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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 : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
simp : ∀ x < k, ¬k + 1 - x = 0
⊢ ∀ x ∈ Finset.range k, k + 1 - x ≠ 0

Tactic:
simp