awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
simp :
  iteratedDerivWithin 3 (g ∘ f) univ x =
    HAdd.hAdd (β := F)
      (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDerivWithin 𝕜 3 g univ (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦
              derivWithin f univ x :
            F)
          ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F)
              ![iteratedDerivWithin 2 f univ x, derivWithin f univ x] :
            F) +
        HSMul.hSMul (α := ℕ) (β := F) 2
          ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f univ x, iteratedDerivWithin 2 f univ x] :
            F))
      ((fderivWithin 𝕜 g univ (f x) : (a : E) → F) (iteratedDerivWithin 3 f univ x) : F)
⊢ iteratedDeriv 3 (g ∘ f) x =
    HAdd.hAdd (β := F)
      (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDeriv 𝕜 3 g (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ deriv f x : F)
          ((iteratedFDeriv 𝕜 2 g (f x) : (a : (i : Fin 2) → E) → F) ![iteratedDeriv 2 f x, deriv f x] : F) +
        HSMul.hSMul (α := ℕ) (β := F) 2
          ((iteratedFDeriv 𝕜 2 g (f x) : (a : (i : Fin 2) → E) → F) ![deriv f x, iteratedDeriv 2 f x] : F))
      ((fderiv 𝕜 g (f x) : (a : E) → F) (iteratedDeriv 3 f x) : F)

Tactic:
simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ,
    ← derivWithin_univ, ← fderivWithin_univ]

Premises used: derivWithin_univ, fderivWithin_univ, iteratedDerivWithin_univ, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    HAdd.hAdd (β := F)
      (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDerivWithin 𝕜 3 g univ (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦
              derivWithin f univ x :
            F)
          ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F)
              ![iteratedDerivWithin 2 f univ x, derivWithin f univ x] :
            F) +
        HSMul.hSMul (α := ℕ) (β := F) 2
          ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f univ x, iteratedDerivWithin 2 f univ x] :
            F))
      ((fderivWithin 𝕜 g univ (f x) : (a : E) → F) (iteratedDerivWithin 3 f univ x) : F)

Tactic:
iteratedDerivWithin_vcomp_three hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)

Premises used: Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ, iteratedDerivWithin_vcomp_three
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    HAdd.hAdd (β := F)
      (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDerivWithin 𝕜 3 g univ (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦
              derivWithin f univ x :
            F)
          ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F)
              ![iteratedDerivWithin 2 f univ x, derivWithin f univ x] :
            F) +
        HSMul.hSMul (α := ℕ) (β := F) 2
          ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f univ x, iteratedDerivWithin 2 f univ x] :
            F))
      ((fderivWithin 𝕜 g univ (f x) : (a : E) → F) (iteratedDerivWithin 3 f univ x) : F)

Tactic:
exact iteratedDerivWithin_vcomp_three hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)

Premises used: Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ, iteratedDerivWithin_vcomp_three
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : (↑i : ℕ∞ω) ≤ n
rw :
  Eq.{u_2 + 1} (α := E)
    (∑ c : OrderedFinpartition i,
      (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → 𝕜) → E) fun (j : Fin c.length) ↦
        iteratedDerivWithin (c.partSize j) f s x)
    (∑ c : OrderedFinpartition i,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
        (iteratedDerivWithin c.length g t (f x)))
⊢ iteratedDerivWithin i (g ∘ f) s x =
    ∑ c : OrderedFinpartition i,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
        (iteratedDerivWithin c.length g t (f x))

Tactic:
rw [iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf ht hs hx hst hi]

Premises used: iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq.{u_2 + 1} (α := E)
    (∑ c : OrderedFinpartition i,
      (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → 𝕜) → E) fun (j : Fin c.length) ↦
        iteratedDerivWithin (c.partSize j) f s x)
    (∑ c : OrderedFinpartition i,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
        (iteratedDerivWithin c.length g t (f x)))

Tactic:
simp only [iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod]

Premises used: iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
rw :
  Eq.{u_2 + 1} (α := E)
    (∑ c : OrderedFinpartition i,
      (iteratedFDeriv 𝕜 c.length g (f x) : (a : (i : Fin c.length) → 𝕜) → E) fun (j : Fin c.length) ↦
        iteratedDeriv (c.partSize j) f x)
    (∑ c : OrderedFinpartition i,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x)
        (iteratedDeriv c.length g (f x)))
⊢ iteratedDeriv i (g ∘ f) x =
    ∑ c : OrderedFinpartition i,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x)
        (iteratedDeriv c.length g (f x))

Tactic:
rw [iteratedDeriv_vcomp_eq_sum_orderedFinpartition hg hf hi]

Premises used: iteratedDeriv_vcomp_eq_sum_orderedFinpartition
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq.{u_2 + 1} (α := E)
    (∑ c : OrderedFinpartition i,
      (iteratedFDeriv 𝕜 c.length g (f x) : (a : (i : Fin c.length) → 𝕜) → E) fun (j : Fin c.length) ↦
        iteratedDeriv (c.partSize j) f x)
    (∑ c : OrderedFinpartition i,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x)
        (iteratedDeriv c.length g (f x)))

Tactic:
simp only [iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod]

Premises used: iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 2 g t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
rw :
  HAdd.hAdd (α := E) (β := E)
      ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E) fun (x_1 : Fin 2) ↦ derivWithin f s x : E)
      ((fderivWithin 𝕜 g t (f x) : (a : 𝕜) → E) (iteratedDerivWithin 2 f s x) : E) =
    HPow.hPow (β := ℕ) (derivWithin f s x) 2 • iteratedDerivWithin 2 g t (f x) +
      iteratedDerivWithin 2 f s x • derivWithin g t (f x)
⊢ iteratedDerivWithin 2 (g ∘ f) s x =
    HPow.hPow (β := ℕ) (derivWithin f s x) 2 • iteratedDerivWithin 2 g t (f x) +
      iteratedDerivWithin 2 f s x • derivWithin g t (f x)

Tactic:
rw [iteratedDerivWithin_vcomp_two hg hf ht hs hx hst]

Premises used: iteratedDerivWithin_vcomp_two
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 2 g t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ HAdd.hAdd (α := E) (β := E)
      ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E) fun (x_1 : Fin 2) ↦ derivWithin f s x : E)
      ((fderivWithin 𝕜 g t (f x) : (a : 𝕜) → E) (iteratedDerivWithin 2 f s x) : E) =
    HPow.hPow (β := ℕ) (derivWithin f s x) 2 • iteratedDerivWithin 2 g t (f x) +
      iteratedDerivWithin 2 f s x • derivWithin g t (f x)

Tactic:
simp [← toSpanSingleton_derivWithin, iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod]

Premises used: toSpanSingleton_derivWithin, iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
simp :
  iteratedDerivWithin 2 (g ∘ f) univ x =
    HPow.hPow (β := ℕ) (derivWithin f univ x) 2 • iteratedDerivWithin 2 g univ (f x) +
      iteratedDerivWithin 2 f univ x • derivWithin g univ (f x)
⊢ iteratedDeriv 2 (g ∘ f) x =
    HPow.hPow (β := ℕ) (deriv f x) 2 • iteratedDeriv 2 g (f x) + iteratedDeriv 2 f x • deriv g (f x)

Tactic:
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]

Premises used: derivWithin_univ, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDerivWithin 2 (g ∘ f) univ x =
    HPow.hPow (β := ℕ) (derivWithin f univ x) 2 • iteratedDerivWithin 2 g univ (f x) +
      iteratedDerivWithin 2 f univ x • derivWithin g univ (f x)

Tactic:
iteratedDerivWithin_scomp_two hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ, iteratedDerivWithin_scomp_two
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDerivWithin 2 (g ∘ f) univ x =
    HPow.hPow (β := ℕ) (derivWithin f univ x) 2 • iteratedDerivWithin 2 g univ (f x) +
      iteratedDerivWithin 2 f univ x • derivWithin g univ (f x)

Tactic:
exact iteratedDerivWithin_scomp_two hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ, iteratedDerivWithin_scomp_two
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
rw :
  HAdd.hAdd (β := E)
      (HAdd.hAdd (α := E) (β := E)
          ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → 𝕜) → E) fun (x_1 : Fin 3) ↦ derivWithin f s x : E)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E)
              ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
            E) +
        HSMul.hSMul (α := ℕ) (β := E) 2
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            E))
      ((fderivWithin 𝕜 g t (f x) : (a : 𝕜) → E) (iteratedDerivWithin 3 f s x) : E) =
    HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
      iteratedDerivWithin 3 f s x • derivWithin g t (f x)
⊢ iteratedDerivWithin 3 (g ∘ f) s x =
    HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
      iteratedDerivWithin 3 f s x • derivWithin g t (f x)

Tactic:
rw [iteratedDerivWithin_vcomp_three hg hf ht hs hx hst]

Premises used: iteratedDerivWithin_vcomp_three
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
simp :
  HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x) +
      HSMul.hSMul (α := ℕ) 2 (derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x)) =
    HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
      HSMul.hSMul (α := ℕ) 3 (derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x))
⊢ HAdd.hAdd (β := E)
      (HAdd.hAdd (α := E) (β := E)
          ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → 𝕜) → E) fun (x_1 : Fin 3) ↦ derivWithin f s x : E)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E)
              ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
            E) +
        HSMul.hSMul (α := ℕ) (β := E) 2
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → 𝕜) → E)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            E))
      ((fderivWithin 𝕜 g t (f x) : (a : 𝕜) → E) (iteratedDerivWithin 3 f s x) : E) =
    HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
      iteratedDerivWithin 3 f s x • derivWithin g t (f x)

Tactic:
simp [← toSpanSingleton_derivWithin, mul_smul, smul_comm (iteratedDerivWithin 2 f s x),
        iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod]

Premises used: iteratedDerivWithin, toSpanSingleton_derivWithin, SMulCommClass.smul_comm, OfNat.ofNat, iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x) +
      HSMul.hSMul (α := ℕ) 2 (derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x)) =
    HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
      HSMul.hSMul (α := ℕ) 3 (derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x))

Tactic:
abel
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
simp :
  iteratedDerivWithin 3 (g ∘ f) univ x =
    HPow.hPow (β := ℕ) (derivWithin f univ x) 3 • iteratedDerivWithin 3 g univ (f x) +
        HSMul.hSMul (α := ℕ) 3
          (iteratedDerivWithin 2 f univ x • derivWithin f univ x • iteratedDerivWithin 2 g univ (f x)) +
      iteratedDerivWithin 3 f univ x • derivWithin g univ (f x)
⊢ iteratedDeriv 3 (g ∘ f) x =
    HPow.hPow (β := ℕ) (deriv f x) 3 • iteratedDeriv 3 g (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDeriv 2 f x • deriv f x • iteratedDeriv 2 g (f x)) +
      iteratedDeriv 3 f x • deriv g (f x)

Tactic:
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]

Premises used: derivWithin_univ, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    HPow.hPow (β := ℕ) (derivWithin f univ x) 3 • iteratedDerivWithin 3 g univ (f x) +
        HSMul.hSMul (α := ℕ) 3
          (iteratedDerivWithin 2 f univ x • derivWithin f univ x • iteratedDerivWithin 2 g univ (f x)) +
      iteratedDerivWithin 3 f univ x • derivWithin g univ (f x)

Tactic:
iteratedDerivWithin_scomp_three hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, iteratedDerivWithin_scomp_three, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    HPow.hPow (β := ℕ) (derivWithin f univ x) 3 • iteratedDerivWithin 3 g univ (f x) +
        HSMul.hSMul (α := ℕ) 3
          (iteratedDerivWithin 2 f univ x • derivWithin f univ x • iteratedDerivWithin 2 g univ (f x)) +
      iteratedDerivWithin 3 f univ x • derivWithin g univ (f x)

Tactic:
exact iteratedDerivWithin_scomp_three hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, iteratedDerivWithin_scomp_three, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : (↑i : ℕ∞ω) ≤ n
rw :
  Eq.{u_1 + 1} (α := 𝕜)
    (∑ c : OrderedFinpartition i,
      HSMul.hSMul (α := 𝕜) (∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
        (iteratedDerivWithin c.length g t (f x)))
    (∑ c : OrderedFinpartition i,
      iteratedDerivWithin c.length g t (f x) * ∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
⊢ iteratedDerivWithin i (g ∘ f) s x =
    ∑ c : OrderedFinpartition i,
      iteratedDerivWithin c.length g t (f x) * ∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x

Tactic:
rw [iteratedDerivWithin_scomp_eq_sum_orderedFinpartition hg hf ht hs hx hst hi]

Premises used: iteratedDerivWithin_scomp_eq_sum_orderedFinpartition
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ c : OrderedFinpartition i,
      HSMul.hSMul (α := 𝕜) (∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)
        (iteratedDerivWithin c.length g t (f x)))
    (∑ c : OrderedFinpartition i,
      iteratedDerivWithin c.length g t (f x) * ∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x)

Tactic:
simp only [smul_eq_mul, mul_comm]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
rw :
  Eq.{u_1 + 1} (α := 𝕜)
    (∑ c : OrderedFinpartition i,
      HSMul.hSMul (α := 𝕜) (∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x) (iteratedDeriv c.length g (f x)))
    (∑ c : OrderedFinpartition i, iteratedDeriv c.length g (f x) * ∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x)
⊢ iteratedDeriv i (g ∘ f) x =
    ∑ c : OrderedFinpartition i, iteratedDeriv c.length g (f x) * ∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x

Tactic:
rw [iteratedDeriv_scomp_eq_sum_orderedFinpartition hg hf hi]

Premises used: iteratedDeriv_scomp_eq_sum_orderedFinpartition
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ c : OrderedFinpartition i,
      HSMul.hSMul (α := 𝕜) (∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x) (iteratedDeriv c.length g (f x)))
    (∑ c : OrderedFinpartition i, iteratedDeriv c.length g (f x) * ∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x)

Tactic:
simp only [smul_eq_mul, mul_comm]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 2 g t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
rw :
  HPow.hPow (β := ℕ) (derivWithin f s x) 2 • iteratedDerivWithin 2 g t (f x) +
      iteratedDerivWithin 2 f s x • derivWithin g t (f x) =
    iteratedDerivWithin 2 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 2 +
      derivWithin g t (f x) * iteratedDerivWithin 2 f s x
⊢ iteratedDerivWithin 2 (g ∘ f) s x =
    iteratedDerivWithin 2 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 2 +
      derivWithin g t (f x) * iteratedDerivWithin 2 f s x

Tactic:
rw [iteratedDerivWithin_scomp_two hg hf ht hs hx hst]

Premises used: iteratedDerivWithin_scomp_two
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 2 g t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ HPow.hPow (β := ℕ) (derivWithin f s x) 2 • iteratedDerivWithin 2 g t (f x) +
      iteratedDerivWithin 2 f s x • derivWithin g t (f x) =
    iteratedDerivWithin 2 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 2 +
      derivWithin g t (f x) * iteratedDerivWithin 2 f s x

Tactic:
simp only [smul_eq_mul, mul_comm]

Premises used: mul_comm, smul_eq_mul