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 : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s) (m : Fin (n + 1) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f s x : (a : (i : Fin (n + 1)) → E) → F) m : F)
      ((((iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s 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)
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F :=
  LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)
A :
  ∀ y ∈ s,
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n.succ f s y)
      (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        ((⇑I :
            (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)
        (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
          E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        y)
⊢ Eq.{uF + 1} (α := F)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) :
                (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m (last n)) :
      F)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
                    (init (α := fun (i : Fin (n + 1 + 1)) ↦ E) m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) :
                (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last (n + 1))) :
      F)

Tactic:
simp [init, tail]

Premises used: Fin.init, Fin.tail
-- 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 : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
H :
  ∀ (m : (i : Fin (n + 1)) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f s 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)
              (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
                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)
    (iteratedFDerivWithin 𝕜 (n + 1) f s 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)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
        E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      x)

Tactic:
ext m
-- 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 : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : (i : Fin (n + 1)) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f s 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)
            (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
              E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            x :
          (a : (i : Fin (n + 1)) → E) → F)
        m :
      F)

Tactic:
simp [iteratedFDerivWithin_succ_apply_right hs hx]

Premises used: iteratedFDerivWithin_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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s 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)
        (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
          E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        x)
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s 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)
          (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s 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))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s x)

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_right hs hx, comp_apply, LinearIsometryEquiv.norm_map]

Premises used: iteratedFDerivWithin_succ_eq_comp_right, LinearIsometryEquiv.norm_map, 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
x : E
h : UniqueDiffWithinAt 𝕜 s x
m : Fin 1 → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 1 f s x : (a : (i : Fin 1) → E) → F) m : F)
    ((fderivWithin 𝕜 f s x : (a : E) → F) (m 0) : F)

Tactic:
simp [iteratedFDerivWithin_succ_apply_left, iteratedFDerivWithin_zero_eq_comp,
    (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_fderivWithin h]

Premises used: LinearIsometryEquiv.comp_fderivWithin, LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, iteratedFDerivWithin_succ_apply_left, iteratedFDerivWithin_zero_eq_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 : Set E
f : E → F
z : E
hs : UniqueDiffOn 𝕜 s
hz : z ∈ s
m : Fin 2 → E
simp :
  Eq.{uF + 1} (α := F)
    ((((((iteratedFDerivWithin 𝕜 0 (fun (y : E) ↦ fderivWithin 𝕜 (fun (y : E) ↦ fderivWithin 𝕜 f s y) s y) s z :
                      (a : (i : Fin 0) → E) → E →L[𝕜] E →L[𝕜] F)
                    (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
                      (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) m)) :
                  E →L[𝕜] E →L[𝕜] F) :
                (a : E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) m (last 0)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last 1)) :
      F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z : (a : E) → E →L[𝕜] F) (m 0) : E →L[𝕜] F) : (a : E) → F) (m 1) : F)
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 2 f s z : (a : (i : Fin 2) → E) → F) m : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z : (a : E) → E →L[𝕜] F) (m 0) : E →L[𝕜] F) : (a : E) → F) (m 1) : F)

Tactic:
simp only [iteratedFDerivWithin_succ_apply_right hs hz]

Premises used: iteratedFDerivWithin_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
s : Set E
f : E → F
z : E
hs : UniqueDiffOn 𝕜 s
hz : z ∈ s
m : Fin 2 → E
⊢ Eq.{uF + 1} (α := F)
    ((((((iteratedFDerivWithin 𝕜 0 (fun (y : E) ↦ fderivWithin 𝕜 (fun (y : E) ↦ fderivWithin 𝕜 f s y) s y) s z :
                      (a : (i : Fin 0) → E) → E →L[𝕜] E →L[𝕜] F)
                    (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
                      (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) m)) :
                  E →L[𝕜] E →L[𝕜] F) :
                (a : E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) m (last 0)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last 1)) :
      F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z : (a : E) → E →L[𝕜] F) (m 0) : E →L[𝕜] F) : (a : E) → F) (m 1) : F)

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 : Set E
f : E → F
z : E
hs : UniqueDiffOn 𝕜 s
hz : z ∈ s
v w : E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 2 f s z : (a : (i : Fin 2) → E) → F) ![v, w] : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)

Tactic:
iteratedFDerivWithin_two_apply f hs hz _

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, iteratedFDerivWithin_two_apply, Fin.cases, Matrix.vecCons
-- 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 f₁ t) (iteratedFDerivWithin 𝕜 0 f t)

Tactic:
h.mono fun y hy => DFunLike.ext _ _ fun _ => hy

Premises used: DFunLike.ext, Filter.EventuallyEq, iteratedFDerivWithin, Filter.Eventually.mono, OfNat.ofNat
-- 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 f₁ t) (iteratedFDerivWithin 𝕜 0 f t)

Tactic:
exact h.mono fun y hy => DFunLike.ext _ _ fun _ => hy

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

Tactic:
have : fderivWithin 𝕜 _ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 _ t := ihn.fderivWithin' ht
-- 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn :
  (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n f₁ t) (iteratedFDerivWithin 𝕜 n f t)
this :
  (𝓝[s] x).EventuallyEq (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t)
⊢ (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f₁ t) (iteratedFDerivWithin 𝕜 (n + 1) f t)

Tactic:
this.mono fun y hy => ?_

Premises used: 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn :
  (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n f₁ t) (iteratedFDerivWithin 𝕜 n f t)
this :
  (𝓝[s] x).EventuallyEq (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t)
succ :
  ∀ (y : E)
    (hy :
      Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t y) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y)),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f₁ t y) (iteratedFDerivWithin 𝕜 (n + 1) f t y)
⊢ (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f₁ t) (iteratedFDerivWithin 𝕜 (n + 1) f t)

Tactic:
refine this.mono fun y hy => ?_

Premises used: 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn :
  (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n f₁ t) (iteratedFDerivWithin 𝕜 n f t)
this :
  (𝓝[s] x).EventuallyEq (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t)
y : E
hy :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t y) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f₁ t y) (iteratedFDerivWithin 𝕜 (n + 1) f t y)

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

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

Tactic:
induction n with
  | zero => exact h.mono fun y hy => DFunLike.ext _ _ fun _ => hy
  | succ n ihn =>
    have : fderivWithin 𝕜 _ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 _ t := ihn.fderivWithin' ht
    refine this.mono fun y hy => ?_
    simp only [iteratedFDerivWithin_succ_eq_comp_left, hy, (· ∘ ·)]

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

Tactic:
h.iteratedFDerivWithin' Subset.rfl n

Premises used: Filter.EventuallyEq.iteratedFDerivWithin', Set.Subset.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 : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
h₁ :
  ∀ (x₁ : E) (h₁x₁ : ∀ᶠ (x : E) in 𝓝[s] x₁, f₁ x = f x) (h₂x₁ : x₁ ∈ s),
    Eq (α := FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 f₁ s x₁) (ftaylorSeriesWithin 𝕜 f s x₁)
⊢ (𝓝[s] x).EventuallyEq (β := FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 f₁ s) (ftaylorSeriesWithin 𝕜 f s)

Tactic:
filter_upwards [eventually_eventually_nhdsWithin.2 h, self_mem_nhdsWithin] with x₁ h₁x₁ h₂x₁

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

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

Tactic:
apply (Filter.EventuallyEq.iteratedFDerivWithin (𝕜 := 𝕜) h₁x₁ n).eq_of_nhdsWithin h₂x₁

Premises used: Filter.EventuallyEq.iteratedFDerivWithin, Filter.EventuallyEq.eq_of_nhdsWithin
-- 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
n : ℕ
⊢ f₁ =ᶠ[𝓝[insert x s] x] f

Tactic:
simpa [EventuallyEq, hx]

Premises used: Filter.EventuallyEq
-- 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 f₁ : E → F
x : E
hs : EqOn f₁ f s
hx : x ∈ s
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f₁ s x)
    (iteratedFDerivWithin 𝕜 n f s x)

Tactic:
(hs.eventuallyEq.filter_mono inf_le_right).iteratedFDerivWithin_eq (hs hx) _

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right, Filter.EventuallyEq.iteratedFDerivWithin_eq
-- 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 f₁ : E → F
hs : EqOn f₁ f s
n : ℕ
⊢ EqOn (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f₁ s)
    (iteratedFDerivWithin 𝕜 n f s) s

Tactic:
fun _x hx =>
  iteratedFDerivWithin_congr hs hx n

Premises used: Set.EqOn, iteratedFDerivWithin_congr