awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
        (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y :
          E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        x)
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
              ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
          (iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
rw₂ rw₃ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f x)

Tactic:
rw [iteratedFDeriv_succ_eq_comp_right, comp_apply, LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map, iteratedFDeriv_succ_eq_comp_right, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
m : Fin 1 → E
rw :
  Eq.{uF + 1} (α := F)
    ((((iteratedFDeriv 𝕜 0 (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin 0) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last 0)) :
      F)
    ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
rw₁ : Eq.{uF + 1} (α := F) ((fderiv 𝕜 f x : (a : E) → F) (m (last 0)) : F) ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
rw₂ rw₃ : Eq.{uF + 1} (α := F) ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F) ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 1 f x : (a : (i : Fin 1) → E) → F) m : F)
    ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)

Tactic:
rw [iteratedFDeriv_succ_apply_right, iteratedFDeriv_zero_apply, last_zero]

Premises used: Fin.last_zero, iteratedFDeriv_zero_apply, iteratedFDeriv_succ_apply_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
f : E → F
rw :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 1) ↦ E) F) (iteratedFDerivWithin 𝕜 1 f univ x) =
    norm (E := E →L[𝕜] F) (fderivWithin 𝕜 f univ x)
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 1) ↦ E) F) (iteratedFDeriv 𝕜 1 f x) =
    norm (E := E →L[𝕜] F) (fderiv 𝕜 f x)

Tactic:
rw [← iteratedFDerivWithin_univ, ← fderivWithin_univ]

Premises used: fderivWithin_univ, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
f : E → F
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 1) ↦ E) F) (iteratedFDerivWithin 𝕜 1 f univ x) =
    norm (E := E →L[𝕜] F) (fderivWithin 𝕜 f univ x)

Tactic:
norm_iteratedFDerivWithin_one f uniqueDiffWithinAt_univ

Premises used: norm_iteratedFDerivWithin_one, uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
f : E → F
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 1) ↦ E) F) (iteratedFDerivWithin 𝕜 1 f univ x) =
    norm (E := E →L[𝕜] F) (fderivWithin 𝕜 f univ x)

Tactic:
exact norm_iteratedFDerivWithin_one f uniqueDiffWithinAt_univ

Premises used: norm_iteratedFDerivWithin_one, uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
z : E
m : Fin 2 → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 2 f z : (a : (i : Fin 2) → E) → F) m : F)
    ((((fderiv 𝕜 (fderiv 𝕜 f) z : (a : E) → E →L[𝕜] F) (m 0) : E →L[𝕜] F) : (a : E) → F) (m 1) : F)

Tactic:
simp [iteratedFDeriv_succ_apply_right, init]

Premises used: Fin.init, iteratedFDeriv_succ_apply_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n fun (z : E) ↦ f (a + z)) fun (x : E) ↦ iteratedFDeriv 𝕜 n f (a + x)

Tactic:
simpa [← iteratedFDerivWithin_univ] using iteratedFDerivWithin_comp_add_left' n a (s := univ)

Premises used: iteratedFDerivWithin_comp_add_left', iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
a x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n (fun (z : E) ↦ f (a + z)) x) (iteratedFDeriv 𝕜 n f (a + x))

Tactic:
simp [iteratedFDeriv_comp_add_left']

Premises used: iteratedFDeriv_comp_add_left'
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n fun (z : E) ↦ f (z + a)) fun (x : E) ↦ iteratedFDeriv 𝕜 n f (x + a)

Tactic:
simpa [add_comm a] using iteratedFDeriv_comp_add_left' n a

Premises used: add_comm, iteratedFDeriv_comp_add_left'
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
a x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n (fun (z : E) ↦ f (z + a)) x) (iteratedFDeriv 𝕜 n f (x + a))

Tactic:
simp [iteratedFDeriv_comp_add_right']

Premises used: iteratedFDeriv_comp_add_right'
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n fun (z : E) ↦ f (z - a)) fun (x : E) ↦ iteratedFDeriv 𝕜 n f (x - a)

Tactic:
simpa [sub_eq_add_neg] using iteratedFDeriv_comp_add_right' n (-a)

Premises used: sub_eq_add_neg, iteratedFDeriv_comp_add_right', Neg.neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
a x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n (fun (z : E) ↦ f (z - a)) x) (iteratedFDeriv 𝕜 n f (x - a))

Tactic:
simp [iteratedFDeriv_comp_sub']

Premises used: iteratedFDeriv_comp_sub'
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
a : 𝕜
⊢ iteratedFDerivWithin 𝕜 0 (fun (x : 𝕜) ↦ f (-x)) s a =
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (β := ℕ) (-1) 0)
      (iteratedFDerivWithin 𝕜 0 f (-s) (-a))

Tactic:
simp [iteratedFDerivWithin]

Premises used: iteratedFDerivWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih :
  ∀ (a : 𝕜),
    iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
      HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
        (iteratedFDerivWithin 𝕜 n f (-s) (-a))
a : 𝕜
h :
  ∀ (b : 𝕜),
    Eq.{uF + 1} (α := F)
      (((iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s b : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
            (a : (i : Fin n) → 𝕜) → F)
          fun (x : Fin n) ↦ 1 :
        F)
      ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
              (iteratedFDerivWithin 𝕜 n f (-s) (-b)) :
            (a : (i : Fin n) → 𝕜) → F)
          fun (x : Fin n) ↦ 1 :
        F)
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s)
    fun (a : 𝕜) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
      (iteratedFDerivWithin 𝕜 n f (-s) (-a))

Tactic:
ext b
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih :
  ∀ (a : 𝕜),
    iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
      HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
        (iteratedFDerivWithin 𝕜 n f (-s) (-a))
a b : 𝕜
h h₁ :
  Eq.{uF + 1} (α := F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (-s) (-b)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (-s) (-b)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
⊢ Eq.{uF + 1} (α := F)
    (((iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s b : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (-s) (-b)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)

Tactic:
rw [ih b]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih :
  ∀ (a : 𝕜),
    iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
      HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
        (iteratedFDerivWithin 𝕜 n f (-s) (-a))
a : 𝕜
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s)
    fun (a : 𝕜) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
      (iteratedFDerivWithin 𝕜 n f (-s) (-a))

Tactic:
have ih' : iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s
        = fun a ↦ (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by
      ext b
      rw [ih b]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
a : 𝕜
zero :
  ∀ (a : 𝕜),
    iteratedFDerivWithin 𝕜 0 (fun (x : 𝕜) ↦ f (-x)) s a =
      HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (β := ℕ) (-1) 0)
        (iteratedFDerivWithin 𝕜 0 f (-s) (-a))
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ (a : 𝕜),
        iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
          HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (-s) (-a)))
    (a : 𝕜),
    iteratedFDerivWithin 𝕜 (n + 1) (fun (x : 𝕜) ↦ f (-x)) s a =
      HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) (n + 1))
        (iteratedFDerivWithin 𝕜 (n + 1) f (-s) (-a))
⊢ iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
      (iteratedFDerivWithin 𝕜 n f (-s) (-a))

Tactic:
induction n generalizing a with
  | zero => simp [iteratedFDerivWithin]
  | succ n ih =>
    have ih' : iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s
        = fun a ↦ (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by
      ext b
      rw [ih b]
    set g := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) a
    rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left,
      Function.comp_apply, Function.comp_apply, ih', ← Pi.smul_def,
      fderivWithin_const_smul_field' ((-1 : 𝕜) ^ n) (f := fun a ↦ g (-a)),
      fderivWithin_comp_neg (f := g), ← neg_one_smul 𝕜 (fderivWithin 𝕜 _ (-s) (-a)),
      ← mul_smul _ (-1), ← pow_succ (-1) n, map_smul]

Premises used: iteratedFDerivWithin_succ_eq_comp_left, Fin.succ, neg_one_smul, pow_succ, iteratedFDerivWithin, fderivWithin, Function.comp_apply, OfNat.ofNat, Pi.smul_def, SemigroupAction.mul_smul, Neg.neg, map_smul
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c : 𝕜
h :
  ∀ (a : 𝕜),
    Eq.{uF + 1} (α := F)
      (((iteratedFDerivWithin 𝕜 n (fun (z : 𝕜) ↦ f (c - z)) s a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
            (a : (i : Fin n) → 𝕜) → F)
          fun (x : Fin n) ↦ 1 :
        F)
      ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
              (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) :
            (a : (i : Fin n) → 𝕜) → F)
          fun (x : Fin n) ↦ 1 :
        F)
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : 𝕜) ↦ f (c - z)) s) fun (x : 𝕜) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
      (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - x))

Tactic:
ext a
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c a : 𝕜
⊢ Eq (α := (z : 𝕜) → F) (fun (z : 𝕜) ↦ f (c - z)) fun (z : 𝕜) ↦ (fun (w : 𝕜) ↦ f (c + w)) (-z)

Tactic:
simp only [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c a : 𝕜
⊢ Eq (α := (z : 𝕜) → F) (fun (z : 𝕜) ↦ f (c - z)) fun (z : 𝕜) ↦ (fun (w : 𝕜) ↦ f (c + w)) (-z)

Tactic:
have : (fun z : 𝕜 => f (c - z)) = fun z => (fun w => f (c + w)) (-z) := by
    simp only [sub_eq_add_neg]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c a : 𝕜
this : Eq (α := (z : 𝕜) → F) (fun (z : 𝕜) ↦ f (c - z)) fun (z : 𝕜) ↦ (fun (w : 𝕜) ↦ f (c + w)) (-z)
h :
  Eq.{uF + 1} (α := F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c + -a)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
⊢ Eq.{uF + 1} (α := F)
    (((iteratedFDerivWithin 𝕜 n (fun (z : 𝕜) ↦ f (c - z)) s a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)

Tactic:
rw [this, iteratedFDerivWithin_comp_neg (f := fun w => f (c + w)) n a,
    iteratedFDerivWithin_comp_add_left]

Premises used: iteratedFDerivWithin_comp_add_left, iteratedFDerivWithin_comp_neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c a : 𝕜
this : Eq (α := (z : 𝕜) → F) (fun (z : 𝕜) ↦ f (c - z)) fun (z : 𝕜) ↦ (fun (w : 𝕜) ↦ f (c + w)) (-z)
⊢ Eq.{uF + 1} (α := F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c + -a)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
x : Fin n
h_1 : Membership.mem (γ := Set (Fin n)) univ x
x_1 : Fin n
h_2 : Membership.mem (γ := Set (Fin n)) univ x_1
h : x ≠ x_1
⊢ onFun (β := Set (Fin n)) Disjoint (fun (m : Fin n) ↦ range fun (x : Fin 1) ↦ m) x x_1

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
m : Fin n
⊢ ∃ (m_1 : Fin n), Membership.mem (γ := Set (Fin n)) (range fun (x : Fin 1) ↦ m_1) m

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
⊢ default = atomic n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
⊢ c.length ≤ n

Tactic:
simpa only [Fintype.card_fin] using Fintype.card_le_of_injective _ c.parts_strictMono.injective

Premises used: Fintype.card_le_of_injective, Fintype.card_fin, StrictMono.injective, OrderedFinpartition.parts_strictMono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
⊢ c.partSize m ≤ n

Tactic:
simpa only [Fintype.card_fin] using Fintype.card_le_of_injective _ (c.emb_strictMono m).injective

Premises used: Fintype.card_le_of_injective, Fintype.card_fin, StrictMono.injective, OrderedFinpartition.emb_strictMono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos_1 : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin qlength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin qlength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin qlength), x ∈ range (qemb m)
hpq :
  embSigma n
      { length := plength, partSize := psize, partSize_pos := partSize_pos, emb := pemb,
        emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover :
        OrderedFinpartition n } =
    embSigma n
      { length := qlength, partSize := qsize, partSize_pos := partSize_pos_1, emb := qemb,
        emb_strictMono := emb_strictMono_1, parts_strictMono := parts_strictMono_1, disjoint := disjoint_1,
        cover := cover_1 }
simp_all :
  ∀
    (hpq :
      plength = qlength ∧
        HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
          (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
            (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (j : Fin plength) ↦ pemb j)
          (β := (p : Fin qlength → Fin (n + 1)) × ((i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n))
          (Sigma.mk (β := fun (p : Fin qlength → Fin (n + 1)) ↦ (i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n)
            (fun (m : Fin qlength) ↦ ⟨qsize m, ⋯⟩) fun (j : Fin qlength) ↦ qemb j)),
    psize ≍ qsize ∧ pemb ≍ qemb
⊢ { length := plength, partSize := psize, partSize_pos := partSize_pos, emb := pemb, emb_strictMono := emb_strictMono,
      parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover : OrderedFinpartition n } =
    { length := qlength, partSize := qsize, partSize_pos := partSize_pos_1, emb := qemb,
      emb_strictMono := emb_strictMono_1, parts_strictMono := parts_strictMono_1, disjoint := disjoint_1,
      cover := cover_1 }

Tactic:
simp_all only [Sigma.mk.inj_iff, true_and, mk.injEq, Fin.mk.injEq, embSigma]

Premises used: OrderedFinpartition.mk.injEq, Fin.mk.injEq, Sigma.mk.inj_iff, OrderedFinpartition.embSigma, true_and