awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
c : ℝ
hc : 0 < c
⊢ Tendsto (fun (y : E) ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s] x ×ˢ 𝓝[insert x s] x)

Tactic:
exact Tendsto.prodMk tendsto_id (tendsto_const_nhdsWithin (by simp))

Premises used: Filter.tendsto_id, Filter.Tendsto.prodMk, tendsto_const_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
c : ℝ
hc : 0 < c
⊢ Tendsto (fun (y : E) ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x))

Tactic:
have : Tendsto (fun y ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x)) := by
    rw [nhdsWithin_prod_eq]
    exact Tendsto.prodMk tendsto_id (tendsto_const_nhdsWithin (by simp))
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
c : ℝ
hc : 0 < c
this : Tendsto (fun (y : E) ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x))
⊢ ∀ᶠ (x_1 : E) in 𝓝[insert x s] x,
    ‖HSub.hSub (β := F) (f x_1 - f x)
          ((((continuousMultilinearCurryFin1 𝕜 E F :
                      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                    (p 1) :
                  E →L[𝕜] F) :
                (a : E) → F)
              (x_1 - x) :
            F)‖ ≤
      c * ‖x_1 - x‖

Tactic:
this (isLittleO_iff.1 h.hasStrictFDerivWithinAt hc)

Premises used: HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, Set.Mem, Filter.Eventually, setOf, Set.preimage, Iff.mp, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
c : ℝ
hc : 0 < c
this : Tendsto (fun (y : E) ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x))
⊢ ∀ᶠ (x_1 : E) in 𝓝[insert x s] x,
    ‖HSub.hSub (β := F) (f x_1 - f x)
          ((((continuousMultilinearCurryFin1 𝕜 E F :
                      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                    (p 1) :
                  E →L[𝕜] F) :
                (a : E) → F)
              (x_1 - x) :
            F)‖ ≤
      c * ‖x_1 - x‖

Tactic:
exact this (isLittleO_iff.1 h.hasStrictFDerivWithinAt hc)

Premises used: HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, Iff.mp, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
h : HasFPowerSeriesAt f p x
⊢ HasFDerivAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p 1))
    x

Tactic:
h.hasStrictFDerivAt.hasFDerivAt

Premises used: HasStrictFDerivAt.hasFDerivAt, HasFPowerSeriesAt.hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
h.hasFDerivWithinAt.differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, HasFPowerSeriesWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
h : HasFPowerSeriesAt f p x
⊢ DifferentiableAt 𝕜 f x

Tactic:
h.hasFDerivAt.differentiableAt

Premises used: HasFPowerSeriesAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : AnalyticWithinAt 𝕜 f s x
obtain :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesWithinAt f p s x),
    DifferentiableWithinAt 𝕜 f (insert x s) x
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
obtain ⟨p, hp⟩ := h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
hp.differentiableWithinAt

Premises used: HasFPowerSeriesWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
exact hp.differentiableWithinAt

Premises used: HasFPowerSeriesWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : AnalyticAt 𝕜 f x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
h.differentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, AnalyticAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
hu : UniqueDiffWithinAt 𝕜 (insert x s) x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s) x)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p 1))

Tactic:
h.hasFDerivWithinAt.fderivWithin hu

Premises used: HasFDerivWithinAt.fderivWithin, HasFPowerSeriesWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
h : HasFPowerSeriesAt f p x
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p 1))

Tactic:
h.hasFDerivAt.fderiv

Premises used: HasFPowerSeriesAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticAt 𝕜 f x
rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesAt f p x), HasStrictFDerivAt f (fderiv 𝕜 f x) x
⊢ HasStrictFDerivAt f (fderiv 𝕜 f x) x

Tactic:
rcases h with ⟨p, hp⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt f p x
rw :
  HasStrictFDerivAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p 1))
    x
⊢ HasStrictFDerivAt f (fderiv 𝕜 f x) x

Tactic:
rw [hp.fderiv_eq]

Premises used: HasFPowerSeriesAt.fderiv_eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p 1))
    x

Tactic:
hp.hasStrictFDerivAt

Premises used: HasFPowerSeriesAt.hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p 1))
    x

Tactic:
exact hp.hasStrictFDerivAt

Premises used: HasFPowerSeriesAt.hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ HasStrictDerivAt f (deriv f x) x

Tactic:
simpa [hasStrictDerivAt_iff_hasStrictFDerivAt, toSpanSingleton_deriv] using hf.hasStrictFDerivAt

Premises used: toSpanSingleton_deriv, hasStrictDerivAt_iff_hasStrictFDerivAt, AnalyticAt.hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ Metric.eball x r
⊢ DifferentiableWithinAt 𝕜 f (insert y s) y

Tactic:
have Z := (h.analyticWithinAt_of_mem hy).differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
inl :
  ∀ (h : HasFPowerSeriesWithinOnBall f p s y r) (hy : y ∈ insert y s ∩ Metric.eball y r),
    DifferentiableWithinAt 𝕜 f (insert y s ∩ Metric.eball y r) y
inr : ∀ (hy : y ≠ x), DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y

Tactic:
rcases eq_or_ne y x with rfl | hy

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
s : Set E
inst_5 : CompleteSpace F
y : E
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
h : HasFPowerSeriesWithinOnBall f p s y r
hy : y ∈ insert y s ∩ Metric.eball y r
⊢ DifferentiableWithinAt 𝕜 f (insert y s ∩ Metric.eball y r) y

Tactic:
Z.mono inter_subset_left

Premises used: Set.inter_subset_left, DifferentiableWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
s : Set E
inst_5 : CompleteSpace F
y : E
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
h : HasFPowerSeriesWithinOnBall f p s y r
hy : y ∈ insert y s ∩ Metric.eball y r
⊢ DifferentiableWithinAt 𝕜 f (insert y s ∩ Metric.eball y r) y

Tactic:
exact Z.mono inter_subset_left

Premises used: Set.inter_subset_left, DifferentiableWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy_1 : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
inr : s ∈ 𝓝[insert x s ∩ Metric.eball x r] y
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y

Tactic:
apply (Z.mono (subset_insert _ _)).mono_of_mem_nhdsWithin

Premises used: DifferentiableWithinAt.mono, DifferentiableWithinAt.mono_of_mem_nhdsWithin, Set.subset_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy_1 : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
inr : s ∈ 𝓝[insert x s] y
⊢ s ∈ 𝓝[insert x s ∩ Metric.eball x r] y

Tactic:
suffices s ∈ 𝓝[insert x s] y from nhdsWithin_mono _ inter_subset_left this
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy_1 : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
inr : s ∈ 𝓝[s] y
⊢ s ∈ 𝓝[insert x s] y

Tactic:
rw [nhdsWithin_insert_of_ne hy]

Premises used: nhdsWithin_insert_of_ne
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy_1 : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[s] y

Tactic:
self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy_1 : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[s] y

Tactic:
exact self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ DifferentiableOn 𝕜 f (Metric.eball x r)

Tactic:
fun _ hy =>
  (h.analyticAt_of_mem hy).differentiableWithinAt

Premises used: HasFPowerSeriesOnBall.analyticAt_of_mem, DifferentiableOn, AnalyticAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
inst_5 : CompleteSpace F
hp : HasFPowerSeriesAt f p x
obtain : ∀ (r : ℝ≥0∞) (hp : HasFPowerSeriesOnBall f p x r), ∀ᶠ (z : E) in 𝓝 x, DifferentiableAt 𝕜 f z
⊢ ∀ᶠ (z : E) in 𝓝 x, DifferentiableAt 𝕜 f z

Tactic:
obtain ⟨r, hp⟩ := hp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
inst_5 : CompleteSpace F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ ∀ᶠ (z : E) in 𝓝 x, DifferentiableAt 𝕜 f z

Tactic:
hp.differentiableOn.eventually_differentiableAt (Metric.eball_mem_nhds _ hp.r_pos)

Premises used: DifferentiableOn.eventually_differentiableAt, HasFPowerSeriesOnBall.differentiableOn, Metric.eball_mem_nhds, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
inst_5 : CompleteSpace F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ ∀ᶠ (z : E) in 𝓝 x, DifferentiableAt 𝕜 f z

Tactic:
exact hp.differentiableOn.eventually_differentiableAt (Metric.eball_mem_nhds _ hp.r_pos)

Premises used: DifferentiableOn.eventually_differentiableAt, HasFPowerSeriesOnBall.differentiableOn, Metric.eball_mem_nhds, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
y : E
hy : y ∈ s
⊢ s ⊆ insert y s

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOnNhd 𝕜 f s
⊢ DifferentiableOn 𝕜 f s

Tactic:
fun y hy ↦ (h y hy).differentiableWithinAt

Premises used: DifferentiableOn, AnalyticAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
inl :
  ∀ (hy : (↑(nnnorm.{u} (E := E) 0) : ℝ≥0∞) < r) (h'y : x + 0 ∈ insert x s),
    HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
      ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p.changeOrigin 0 1))
      (insert x s) (x + 0)
inr :
  ∀ (h''y : y ≠ 0),
    HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
      ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p.changeOrigin y 1))
      (insert x s) (x + y)
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert x s) (x + y)

Tactic:
rcases eq_or_ne y 0 with rfl | h''y

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hy : (↑(nnnorm.{u} (E := E) 0) : ℝ≥0∞) < r
h'y : x + 0 ∈ insert x s
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin 0 1))
    (insert (x + 0) s) (x + 0)

Tactic:
(h.changeOrigin hy h'y).hasFPowerSeriesWithinAt.hasFDerivWithinAt

Premises used: HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt, HasFPowerSeriesWithinOnBall.changeOrigin, HasFPowerSeriesWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hy : (↑(nnnorm.{u} (E := E) 0) : ℝ≥0∞) < r
h'y : x + 0 ∈ insert x s
h₁ : x = x + 0
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin 0 1))
    (insert x s) (x + 0)

Tactic:
convert! (h.changeOrigin hy h'y).hasFPowerSeriesWithinAt.hasFDerivWithinAt

Premises used: HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt, HasFPowerSeriesWithinOnBall.changeOrigin, HasFPowerSeriesWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hy : (↑(nnnorm.{u} (E := E) 0) : ℝ≥0∞) < r
h'y : x + 0 ∈ insert x s
⊢ x = x + 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert (x + y) s) (x + y)

Tactic:
have Z := (h.changeOrigin hy h'y).hasFPowerSeriesWithinAt.hasFDerivWithinAt