awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
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
⊢ iteratedDerivWithin (n + 1) (f • g) s x =
    ∑ i ∈ Finset.range (n + 1 + 1),
      (n + 1).choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n + 1 - i) g s x
have succ₁ : derivWithin (f • g) s =ᶠ[𝓝[insert x s] x] f • derivWithin g s + derivWithin f s • g
Tactic: rw [iteratedDerivWithin_succ', Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert
        (g := f • derivWithin g s + derivWithin f s • g)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_1 : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
inst_5 : Module 𝔸 F
inst_6 : IsBoundedSMul 𝔸 F
inst_7 : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F} (hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x)
    (hg : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x),
    iteratedDerivWithin n (f • g) s x =
      ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1) : WithTop ℕ∞) g s y
⊢ iteratedDerivWithin n (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
have 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
Tactic: rw [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]
-- 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
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
⊢ 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
have succ₁ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin f s) s x
Tactic: rw [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]
-- 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
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
⊢ 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
have succ₂ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x
Tactic: rw [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]
-- 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
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
⊢ 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
have succ₃ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
Tactic: rw [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]
-- 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
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
⊢ 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
have succ₄ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin g s) s x
Tactic: rw [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]
-- 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
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
⊢ 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
have succ₅ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f • derivWithin g s) s x
Tactic: rw [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]
-- 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
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
⊢ 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
have succ₆ : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (derivWithin f s • g) s x
Tactic: rw [Finset.sum_range_succ', iteratedDerivWithin_add hx h, IH, Finset.sum_range_succ', IH]
-- 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
⊢ ∑ 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
have 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
Tactic: simp only [Nat.choose_succ_succ', add_smul, Finset.sum_add_distrib]
-- 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
⊢ ∑ 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
have 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
Tactic: nth_rw 3 [Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_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
have simp : ∀ i < n, 1 ≤ n - i
Tactic: simp