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 : ℕ
s : Set 𝕜
f : 𝕜 → F
c : 𝕜
h :
  ∀ (a : 𝕜),
    iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c - z)) s a =
      HPow.hPow (α := 𝕜) (-1) n • iteratedDerivWithin n f (c +ᵥ -s) (c - a)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c - z)) s) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) n • iteratedDerivWithin n f (c +ᵥ -s) (c - x)

Tactic:
ext a
-- 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 : ℕ
s : Set 𝕜
f : 𝕜 → F
c a : 𝕜
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ f (c - z)) s a =
    HPow.hPow (α := 𝕜) (-1) n • iteratedDerivWithin n f (c +ᵥ -s) (c - a)

Tactic:
simp [iteratedDerivWithin, iteratedFDerivWithin_comp_const_sub]

Premises used: iteratedDerivWithin, iteratedFDerivWithin_comp_const_sub
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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
succ : ∀ (n : ℕ), iteratedDerivWithin (n + 1) id s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0
⊢ iteratedDerivWithin n id s x = if n = 0 then x else if n = 1 then 1 else 0

Tactic:
obtain (_ | n) := n
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
⊢ iteratedDerivWithin 0 id s x = if Eq (α := ℕ) 0 0 then x else if Eq (α := ℕ) 0 1 then 1 else 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
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
rw : Set.EqOn (derivWithin id s) (fun (x : 𝕜) ↦ 1) s
⊢ iteratedDerivWithin (n + 1) id 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]

Premises used: iteratedDerivWithin_succ', iteratedDerivWithin_congr
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin n (fun (x : 𝕜) ↦ 1) s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 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 : ℕ
⊢ Set.EqOn (derivWithin id s) (fun (x : 𝕜) ↦ 1) s

Tactic:
fun y hy ↦ derivWithin_id _ _ (h.uniqueDiffWithinAt hy)

Premises used: UniqueDiffOn.uniqueDiffWithinAt, Set.EqOn, derivWithin_id
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ Set.EqOn (derivWithin id s) (fun (x : 𝕜) ↦ 1) s

Tactic:
exact fun y hy ↦ derivWithin_id _ _ (h.uniqueDiffWithinAt hy)

Premises used: UniqueDiffOn.uniqueDiffWithinAt, derivWithin_id
-- 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 𝕜 (↑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:
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
⊢ 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
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
⊢ 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

Premises used: ContDiffWithinAt.eventually, Filter.Eventually.and, Filter.Eventually.exists_mem
-- 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
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
succ₁ : derivWithin (f • g) s =ᶠ[𝓝[insert x s] x] f • derivWithin g s + derivWithin f s • g
⊢ 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:
rw [iteratedDerivWithin_succ', Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert
        (g := f • derivWithin g s + derivWithin f s • g)]

Premises used: iteratedDerivWithin_succ', Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert
-- 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
succ :
  ∑ 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 =
    ∑ k ∈ Finset.range (n + 1),
        (n + 1).choose (k + 1) • iteratedDerivWithin (k + 1) f s x • iteratedDerivWithin (n + 1 - (k + 1)) g s x +
      (n + 1).choose 0 • iteratedDerivWithin 0 f s x • iteratedDerivWithin (n + 1 - 0) g s x
succ₁ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin f s) s x
succ₂ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x
succ₃ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
succ₄ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin g s) s x
succ₅ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f • derivWithin g s) s x
succ₆ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin f s • g) s x
⊢ 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 [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]

Premises used: iteratedDerivWithin_add, Finset.sum_range_succ'
-- 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
succ :
  ∑ 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 =
    HAdd.hAdd (α := F)
        (∑ 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 + 1),
          n.choose (x_1 + 1) • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n + 1 - (x_1 + 1)) g s x) +
      (n + 1).choose 0 • iteratedDerivWithin 0 f s x • iteratedDerivWithin (n + 1 - 0) g s x
⊢ ∑ 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 =
    ∑ k ∈ Finset.range (n + 1),
        (n + 1).choose (k + 1) • iteratedDerivWithin (k + 1) f s x • iteratedDerivWithin (n + 1 - (k + 1)) g s x +
      (n + 1).choose 0 • iteratedDerivWithin 0 f s x • iteratedDerivWithin (n + 1 - 0) g s x

Tactic:
simp only [Nat.choose_succ_succ', add_smul, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, add_smul, Nat.choose_succ_succ'
-- 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
succ :
  ∑ 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
⊢ ∑ 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 =
    HAdd.hAdd (α := F)
        (∑ 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 + 1),
          n.choose (x_1 + 1) • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n + 1 - (x_1 + 1)) g s x) +
      (n + 1).choose 0 • iteratedDerivWithin 0 f s x • iteratedDerivWithin (n + 1 - 0) g s x

Tactic:
nth_rw 3 [Finset.sum_range_succ]

Premises used: Finset.sum_range_succ
-- 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
simp : ∀ i < n, 1 ≤ n - i
⊢ ∀ i ∈ Finset.range n, 1 ≤ n - i

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
⊢ ∀ i < n, 1 ≤ n - i

Tactic:
lia
-- 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
⊢ ∀ i ∈ Finset.range n, 1 ≤ n - i

Tactic:
have : ∀ i ∈ Finset.range n, 1 ≤ n - i := by simp; lia
-- 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
this : ∀ i ∈ Finset.range n, 1 ≤ n - i
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
⊢ ∑ 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

Tactic:
simp +contextual [← iteratedDerivWithin_succ', ← n.sub_sub, Nat.sub_add_cancel, this]

Premises used: Nat.sub_sub, Nat.sub_add_cancel, iteratedDerivWithin_succ'
-- 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
this : ∀ i ∈ Finset.range n, 1 ≤ n - i
⊢ ∑ 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:
abel
-- 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
⊢ HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 ≤ (↑(n + 1) : WithTop ℕ∞)

Tactic:
simp_all