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
⊢ tsupport (α := 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) ⊆
    tsupport f

Tactic:
closure_minimal ((support_comp_subset (map_zero _) _).trans subset_closure)
      isClosed_closure

Premises used: subset_closure, closure_minimal, Function.support_comp_subset, map_zero, HasSubset.Subset.trans, tsupport, isClosed_closure
-- 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
⊢ tsupport (α := 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) ⊆
    tsupport f

Tactic:
exact closure_minimal ((support_comp_subset (map_zero _) _).trans subset_closure)
      isClosed_closure

Premises used: subset_closure, closure_minimal, Function.support_comp_subset, map_zero, HasSubset.Subset.trans, isClosed_closure
-- 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 : ℕ
IH :
  tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
succ :
  tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ 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)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 n f))) ⊆
    tsupport f
⊢ tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f) ⊆
    tsupport f

Tactic:
rw [iteratedFDeriv_succ_eq_comp_left]

Premises used: iteratedFDeriv_succ_eq_comp_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 : ℕ
IH :
  tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ 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)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 n f))) ⊆
    tsupport f

Tactic:
closure_minimal ((support_comp_subset (map_zero _) _).trans
      ((support_fderiv_subset 𝕜).trans IH)) isClosed_closure

Premises used: closure_minimal, Function.support_comp_subset, map_zero, HasSubset.Subset.trans, tsupport, support_fderiv_subset, isClosed_closure
-- 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 : ℕ
zero :
  tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f) ⊆ tsupport f
succ :
  ∀ (n : ℕ)
    (IH :
      tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) ⊆
        tsupport f),
    tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (iteratedFDeriv 𝕜 (n + 1) f) ⊆
      tsupport f
⊢ tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) ⊆ tsupport f

Tactic:
induction n with
  | zero =>
    rw [iteratedFDeriv_zero_eq_comp]
    exact closure_minimal ((support_comp_subset (map_zero _) _).trans subset_closure)
      isClosed_closure
  | succ n IH =>
    rw [iteratedFDeriv_succ_eq_comp_left]
    exact closure_minimal ((support_comp_subset (map_zero _) _).trans
      ((support_fderiv_subset 𝕜).trans IH)) isClosed_closure

Premises used: Fin.succ, subset_closure, closure_minimal, Function.support_comp_subset, map_zero, HasSubset.Subset.trans, iteratedFDeriv_zero_eq_comp, iteratedFDeriv_succ_eq_comp_left, isClosed_closure
-- 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 : ℕ
⊢ support (M := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) ⊆ tsupport f

Tactic:
subset_closure.trans (tsupport_iteratedFDeriv_subset n)

Premises used: subset_closure, HasSubset.Subset.trans, tsupport_iteratedFDeriv_subset
-- 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
hf : HasCompactSupport f
n : ℕ
⊢ HasCompactSupport (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (_root_.iteratedFDeriv 𝕜 n f)

Tactic:
hf.of_isClosed_subset isClosed_closure (tsupport_iteratedFDeriv_subset n)

Premises used: IsCompact.of_isClosed_subset, tsupport_iteratedFDeriv_subset, isClosed_closure, HasCompactSupport
-- 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 := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ 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)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) x)
rw₁ :
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
    norm (E := 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)
          (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
rw₂ rw₃ :
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
    norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x)
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n 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_left, comp_apply, LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map, Function.comp_apply, iteratedFDeriv_succ_eq_comp_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 : ℕ
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f univ)
    (iteratedFDeriv 𝕜 n f)

Tactic:
simp [iteratedFDerivWithin, iteratedFDeriv]

Premises used: iteratedFDerivWithin, iteratedFDeriv
-- 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₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
n : ℕ
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f₁)
    (iteratedFDeriv 𝕜 n f₂)

Tactic:
simp_all [← nhdsWithin_univ, ← iteratedFDerivWithin_univ, EventuallyEq.iteratedFDerivWithin]

Premises used: nhdsWithin_univ, Filter.EventuallyEq.iteratedFDerivWithin, 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
h₁ :
  ∀ (e₁ : E) (he₁ : f₁ =ᶠ[𝓝 e₁] f),
    Eq (α := FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 f₁ e₁) (ftaylorSeries 𝕜 f e₁)
⊢ (𝓝 x).EventuallyEq (β := FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 f₁) (ftaylorSeries 𝕜 f)

Tactic:
filter_upwards [eventually_eventuallyEq_nhds.2 h] with e₁ he₁

Premises used: Iff.mpr, eventually_eventuallyEq_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
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
e₁ : E
he₁ : f₁ =ᶠ[𝓝 e₁] f
h₁ :
  ∀ (n : ℕ),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (ftaylorSeries 𝕜 f₁ e₁ n)
      (ftaylorSeries 𝕜 f e₁ n)
⊢ Eq (α := FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 f₁ e₁) (ftaylorSeries 𝕜 f e₁)

Tactic:
ext n : 1
-- 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
e₁ : E
he₁ : f₁ =ᶠ[𝓝 e₁] f
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (ftaylorSeries 𝕜 f₁ e₁ n)
    (ftaylorSeries 𝕜 f e₁ n)

Tactic:
(he₁.iteratedFDeriv 𝕜 n).eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds, ftaylorSeries, Filter.EventuallyEq.iteratedFDeriv
-- 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
e₁ : E
he₁ : f₁ =ᶠ[𝓝 e₁] f
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (ftaylorSeries 𝕜 f₁ e₁ n)
    (ftaylorSeries 𝕜 f e₁ n)

Tactic:
exact (he₁.iteratedFDeriv 𝕜 n).eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds, Filter.EventuallyEq.iteratedFDeriv
-- 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : (↑m : ℕ∞ω) ≤ n
x : E
rw : p x m = iteratedFDerivWithin 𝕜 m f univ x
⊢ p x m = iteratedFDeriv 𝕜 m f x

Tactic:
rw [← iteratedFDerivWithin_univ]

Premises used: 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : (↑m : ℕ∞ω) ≤ n
x : E
rw :
  ∀ (h : HasFTaylorSeriesUpToOn n f p univ) {m : ℕ} (hmn : (↑m : ℕ∞ω) ≤ n) (x : E),
    p x m = iteratedFDerivWithin 𝕜 m f univ x
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff] at h

Premises used: hasFTaylorSeriesUpToOn_univ_iff
-- 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hmn : (↑m : ℕ∞ω) ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x

Tactic:
h.eq_iteratedFDerivWithin_of_uniqueDiffOn hmn uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn
-- 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hmn : (↑m : ℕ∞ω) ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x

Tactic:
exact h.eq_iteratedFDerivWithin_of_uniqueDiffOn hmn uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn
-- 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 : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
hx : x ∈ s
rw :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f univ x)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDeriv 𝕜 n f x)

Tactic:
rw [← iteratedFDerivWithin_univ]

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

Tactic:
iteratedFDerivWithin_congr_set (Filter.eventuallyEq_univ.mpr <| hs.mem_nhds hx) n

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

Tactic:
exact iteratedFDerivWithin_congr_set (Filter.eventuallyEq_univ.mpr <| hs.mem_nhds hx) n

Premises used: Iff.mpr, IsOpen.mem_nhds, Filter.eventuallyEq_univ, 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
f : E → F
h : ∀ (x : E), Eq (α := FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 f univ x) (ftaylorSeries 𝕜 f x)
⊢ Eq (α := (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 f univ) (ftaylorSeries 𝕜 f)

Tactic:
ext1 x
-- 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
h :
  ∀ (n : ℕ),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (ftaylorSeriesWithin 𝕜 f univ x n)
      (ftaylorSeries 𝕜 f x n)
⊢ Eq (α := FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 f univ x) (ftaylorSeries 𝕜 f x)

Tactic:
ext1 n
-- 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 : ℕ
h h₁ :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f x)
    (iteratedFDeriv 𝕜 n f x)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f univ x)
    (iteratedFDeriv 𝕜 n f x)

Tactic:
rw [iteratedFDerivWithin_univ]

Premises used: 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
x : E
n : ℕ
m : Fin (n + 1) → E
rw :
  Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f univ x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((((iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f univ y) univ x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last n)) :
      F)
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((((iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last n)) :
      F)

Tactic:
rw [← iteratedFDerivWithin_univ, ← 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
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f univ x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((((iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f univ y) univ x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last n)) :
      F)

Tactic:
iteratedFDerivWithin_succ_apply_right uniqueDiffOn_univ (mem_univ _) _

Premises used: iteratedFDerivWithin_succ_apply_right, uniqueDiffOn_univ, Set.mem_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
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f univ x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((((iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f univ y) univ x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last n)) :
      F)

Tactic:
exact iteratedFDerivWithin_succ_apply_right uniqueDiffOn_univ (mem_univ _) _

Premises used: iteratedFDerivWithin_succ_apply_right, uniqueDiffOn_univ, Set.mem_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
x : E
n : ℕ
H :
  ∀ (m : (i : Fin (n + 1)) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) m : 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 :
            (a : (i : Fin (n + 1)) → E) → F)
          m :
        F)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f x)
    (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)

Tactic:
ext m