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
s t : Set E
f : E → F
y x : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 f s) (iteratedFDerivWithin 𝕜 0 f s)

Tactic:
rfl
-- 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
s t : Set E
f : E → F
y : E
n : ℕ
ihn :
  ∀ {x : E} (h : s =ᶠ[𝓝[{y}ᶜ] x] t),
    (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n f s) (iteratedFDerivWithin 𝕜 n f t)
x : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f s) (iteratedFDerivWithin 𝕜 (n + 1) f t)

Tactic:
(eventually_nhds_nhdsWithin.2 h).mono fun y hy => ?_

Premises used: Iff.mpr, eventually_nhds_nhdsWithin, Filter.EventuallyEq, Filter.Eventually.mono
-- 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
s t : Set E
f : E → F
y : E
n : ℕ
ihn :
  ∀ {x : E} (h : s =ᶠ[𝓝[{y}ᶜ] x] t),
    (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n f s) (iteratedFDerivWithin 𝕜 n f t)
x : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
succ :
  ∀ (y_1 : E) (hy : ∀ᶠ (x : E) in 𝓝[{y}ᶜ] y_1, s x = t x),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s y_1) (iteratedFDerivWithin 𝕜 (n + 1) f t y_1)
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f s) (iteratedFDerivWithin 𝕜 (n + 1) f t)

Tactic:
refine (eventually_nhds_nhdsWithin.2 h).mono fun y hy => ?_

Premises used: Iff.mpr, eventually_nhds_nhdsWithin, Filter.Eventually.mono
-- 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
s t : Set E
f : E → F
y_1 : E
n : ℕ
ihn :
  ∀ {x : E} (h : s =ᶠ[𝓝[{y_1}ᶜ] x] t),
    (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n f s) (iteratedFDerivWithin 𝕜 n f t)
x : E
h : s =ᶠ[𝓝[{y_1}ᶜ] x] t
y : E
hy : ∀ᶠ (x : E) in 𝓝[{y_1}ᶜ] y, s x = t x
succ :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s y) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f s y) (iteratedFDerivWithin 𝕜 (n + 1) f t y)

Tactic:
simp only [iteratedFDerivWithin_succ_eq_comp_left, (· ∘ ·)]

Premises used: iteratedFDerivWithin_succ_eq_comp_left, Function.comp
-- 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
s t : Set E
f : E → F
x y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
n : ℕ
zero :
  ∀ {x : E} (h : s =ᶠ[𝓝[{y}ᶜ] x] t),
    (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (iteratedFDerivWithin 𝕜 0 f s) (iteratedFDerivWithin 𝕜 0 f s)
succ :
  ∀ (n : ℕ)
    (ihn :
      ∀ {x : E} (h : s =ᶠ[𝓝[{y}ᶜ] x] t),
        (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
          (iteratedFDerivWithin 𝕜 n f s) (iteratedFDerivWithin 𝕜 n f t))
    {x : E} (h : s =ᶠ[𝓝[{y}ᶜ] x] t),
    (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s) (iteratedFDerivWithin 𝕜 (n + 1) f t)
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n f s) (iteratedFDerivWithin 𝕜 n f t)

Tactic:
induction n generalizing x with
  | zero => rfl
  | succ n ihn =>
    refine (eventually_nhds_nhdsWithin.2 h).mono fun y hy => ?_
    simp only [iteratedFDerivWithin_succ_eq_comp_left, (· ∘ ·)]
    rw [(ihn hy).fderivWithin_eq_of_nhds, fderivWithin_congr_set' _ hy]

Premises used: Iff.mpr, eventually_nhds_nhdsWithin, iteratedFDerivWithin_succ_eq_comp_left, Fin.succ, Function.comp, Filter.Eventually.mono
-- 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
s t : Set E
f : E → F
x : E
h : s =ᶠ[𝓝 x] t
n : ℕ
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n f s) (iteratedFDerivWithin 𝕜 n f t)

Tactic:
iteratedFDerivWithin_eventually_congr_set' x (h.filter_mono inf_le_left) n

Premises used: Filter.EventuallyEq.filter_mono, iteratedFDerivWithin_eventually_congr_set', inf_le_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
s t : Set E
f : E → F
x y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f t x)

Tactic:
(iteratedFDerivWithin_eventually_congr_set' y h n).self_of_nhds

Premises used: Filter.Eventually.self_of_nhds, iteratedFDerivWithin_eventually_congr_set'
-- 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
s : Set E
f : E → F
x : E
n : ℕ
y x_1 : E
h : Membership.mem (γ := Set E) {x}ᶜ x_1
⊢ x_1 ∈ insert x s ↔ x_1 ∈ s

Tactic:
simp_all
-- 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
s t : Set E
f : E → F
x : E
h : s =ᶠ[𝓝 x] t
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f t x)

Tactic:
(iteratedFDerivWithin_eventually_congr_set h n).self_of_nhds

Premises used: iteratedFDerivWithin_eventually_congr_set, Filter.Eventually.self_of_nhds
-- 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
s : Set E
f : E → F
x : E
h :
  ∀ (y : E) (n : ℕ),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (ftaylorSeriesWithin 𝕜 f (insert x s) y n) (ftaylorSeriesWithin 𝕜 f s y n)
⊢ Eq (α := (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 f (insert x s)) (ftaylorSeriesWithin 𝕜 f s)

Tactic:
ext y n : 2
-- 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
s : Set E
f : E → F
x y : E
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (ftaylorSeriesWithin 𝕜 f (insert x s) y n)
    (ftaylorSeriesWithin 𝕜 f s y n)

Tactic:
apply iteratedFDerivWithin_insert

Premises used: iteratedFDerivWithin_insert
-- 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
s u : Set E
f : E → F
x : E
n : ℕ
hu : u ∈ 𝓝[s] x
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f s x)

Tactic:
iteratedFDerivWithin_congr_set (nhdsWithin_eq_iff_eventuallyEq.1 <| nhdsWithin_inter_of_mem' hu) _

Premises used: nhdsWithin_eq_iff_eventuallyEq, nhdsWithin_inter_of_mem', Iff.mp, iteratedFDerivWithin_congr_set
-- 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
s u : Set E
f : E → F
x : E
n : ℕ
hu : u ∈ 𝓝 x
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f s x)

Tactic:
iteratedFDerivWithin_inter' (mem_nhdsWithin_of_mem_nhds hu)

Premises used: iteratedFDerivWithin_inter', mem_nhdsWithin_of_mem_nhds
-- 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
s u : Set E
f : E → F
x : E
n : ℕ
hu : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hx : x ∈ u
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f s x)

Tactic:
iteratedFDerivWithin_inter (hu.mem_nhds hx)

Premises used: IsOpen.mem_nhds, iteratedFDerivWithin_inter
-- 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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
x : E
hmn : (↑0 : ℕ∞ω) ≤ n
hx : x ∈ s
zero :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
        (f x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 f s x : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
zero₁ :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
        (f x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
          f)
        x :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
zero₂ zero₃ :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
        (f x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
        (f x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0) (iteratedFDerivWithin 𝕜 0 f s x)

Tactic:
rw [h.zero_eq' hx, iteratedFDerivWithin_zero_eq_comp, comp_apply]

Premises used: HasFTaylorSeriesUpToOn.zero_eq', iteratedFDerivWithin_zero_eq_comp, 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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
m : ℕ
IH : ∀ {x : E} (hmn : (↑m : ℕ∞ω) ≤ n) (hx : x ∈ s), p x m = iteratedFDerivWithin 𝕜 m f s x
x : E
hmn : (↑(m + 1) : ℕ∞ω) ≤ n
hx : x ∈ s
⊢ (↑m : ℕ∞ω) < n

Tactic:
have A : m < n := lt_of_lt_of_le (mod_cast lt_add_one m) hmn
-- 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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
m : ℕ
IH : ∀ {x : E} (hmn : (↑m : ℕ∞ω) ≤ n) (hx : x ∈ s), p x m = iteratedFDerivWithin 𝕜 m f s x
x : E
hmn : (↑(m + 1) : ℕ∞ω) ≤ n
hx : x ∈ s
A : (↑m : ℕ∞ω) < n
⊢ HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (y : E) ↦ iteratedFDerivWithin 𝕜 m f s y)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x

Tactic:
have :
      HasFDerivWithinAt (fun y : E => iteratedFDerivWithin 𝕜 m f s y)
        (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x :=
      (h.fderivWithin m A x hx).congr (fun y hy => (IH (le_of_lt A) hy).symm)
        (IH (le_of_lt A) hx).symm
-- 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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
m : ℕ
IH : ∀ {x : E} (hmn : (↑m : ℕ∞ω) ≤ n) (hx : x ∈ s), p x m = iteratedFDerivWithin 𝕜 m f s x
x : E
hmn : (↑(m + 1) : ℕ∞ω) ≤ n
hx : x ∈ s
A : (↑m : ℕ∞ω) < n
this :
  HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (y : E) ↦ iteratedFDerivWithin 𝕜 m f s y)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x
succ :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p x (m + 1))
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (m + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (m + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (m + 1)) ↦ E) F)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)))
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p x (m + 1))
    (iteratedFDerivWithin 𝕜 (m + 1) f s x)

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_left, Function.comp_apply, this.fderivWithin (hs x hx)]

Premises used: iteratedFDerivWithin_succ_eq_comp_left, HasFDerivWithinAt.fderivWithin, 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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
m : ℕ
IH : ∀ {x : E} (hmn : (↑m : ℕ∞ω) ≤ n) (hx : x ∈ s), p x m = iteratedFDerivWithin 𝕜 m f s x
x : E
hmn : (↑(m + 1) : ℕ∞ω) ≤ n
hx : x ∈ s
A : (↑m : ℕ∞ω) < n
this :
  HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (y : E) ↦ iteratedFDerivWithin 𝕜 m f s y)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p x (m + 1))
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (m + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (m + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (m + 1)) ↦ E) F)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)))

Tactic:
(ContinuousMultilinearMap.uncurry_curryLeft _).symm

Premises used: ContinuousLinearMap.uncurryLeft, MultilinearMap.mkContinuous, ContinuousMultilinearMap.uncurry_curryLeft, Eq.symm
-- 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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
m : ℕ
IH : ∀ {x : E} (hmn : (↑m : ℕ∞ω) ≤ n) (hx : x ∈ s), p x m = iteratedFDerivWithin 𝕜 m f s x
x : E
hmn : (↑(m + 1) : ℕ∞ω) ≤ n
hx : x ∈ s
A : (↑m : ℕ∞ω) < n
this :
  HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (y : E) ↦ iteratedFDerivWithin 𝕜 m f s y)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) s x
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p x (m + 1))
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (m + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (m + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (m + 1)) ↦ E) F)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)))

Tactic:
exact (ContinuousMultilinearMap.uncurry_curryLeft _).symm

Premises used: ContinuousMultilinearMap.uncurry_curryLeft, Eq.symm
-- 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
s : Set E
f : E → F
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
m : ℕ
hmn : (↑m : ℕ∞ω) ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
zero :
  ∀ {x : E} (hmn : (↑0 : ℕ∞ω) ≤ n) (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0) (iteratedFDerivWithin 𝕜 0 f s x)
succ :
  ∀ (m : ℕ) (IH : ∀ {x : E} (hmn : (↑m : ℕ∞ω) ≤ n) (hx : x ∈ s), p x m = iteratedFDerivWithin 𝕜 m f s x) {x : E}
    (hmn : (↑(m + 1) : ℕ∞ω) ≤ n) (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p x (m + 1))
      (iteratedFDerivWithin 𝕜 (m + 1) f s x)
⊢ p x m = iteratedFDerivWithin 𝕜 m f s x

Tactic:
induction m generalizing x with
  | zero => rw [h.zero_eq' hx, iteratedFDerivWithin_zero_eq_comp, comp_apply]
  | succ m IH =>
    have A : m < n := lt_of_lt_of_le (mod_cast lt_add_one m) hmn
    have :
      HasFDerivWithinAt (fun y : E => iteratedFDerivWithin 𝕜 m f s y)
        (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x :=
      (h.fderivWithin m A x hx).congr (fun y hy => (IH (le_of_lt A) hy).symm)
        (IH (le_of_lt A) hx).symm
    rw [iteratedFDerivWithin_succ_eq_comp_left, Function.comp_apply, this.fderivWithin (hs x hx)]
    exact (ContinuousMultilinearMap.uncurry_curryLeft _).symm

Premises used: iteratedFDerivWithin_succ_eq_comp_left, HasFTaylorSeriesUpToOn.zero_eq', Fin.succ, ContinuousMultilinearMap.uncurry_curryLeft, iteratedFDerivWithin_zero_eq_comp, Function.comp_apply, Eq.symm
-- 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
s : Set E
f : E → F
a : E
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 0 f (a +ᵥ s) (a + x)

Tactic:
simp [iteratedFDerivWithin]

Premises used: iteratedFDerivWithin
-- 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
s : Set E
f : E → F
a : E
n : ℕ
IH :
  Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
succ :
  ∀ (v : E) (x : (i : Fin (n + 1)) → E),
    Eq.{uF + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 (n + 1) (fun (z : E) ↦ f (a + z)) s v : (a : (i : Fin (n + 1)) → E) → F) x : F)
      ((iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + v) : (a : (i : Fin (n + 1)) → E) → F) x : F)
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦
    iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + x)

Tactic:
ext v
-- 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
s : Set E
f : E → F
a : E
n : ℕ
IH :
  Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
v : E
x : (i : Fin (n + 1)) → E
⊢ Eq.{uF + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 (n + 1) (fun (z : E) ↦ f (a + z)) s v : (a : (i : Fin (n + 1)) → E) → F) x : F)
    ((iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + v) : (a : (i : Fin (n + 1)) → E) → F) x : F)

Tactic:
simp [iteratedFDerivWithin_succ_eq_comp_left, IH, fderivWithin_comp_add_left]

Premises used: fderivWithin_comp_add_left, iteratedFDerivWithin_succ_eq_comp_left