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
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) s

Tactic:
(h.iteratedFDerivWithin hs.uniqueDiffOn n).congr
    (fun x hx ↦ (iteratedFDerivWithin_of_isOpen n hs hx).symm)

Premises used: AnalyticOn.iteratedFDerivWithin, iteratedFDerivWithin_of_isOpen, AnalyticOn.congr, IsOpen.uniqueDiffOn, Eq.symm
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) s

Tactic:
exact (h.iteratedFDerivWithin hs.uniqueDiffOn n).congr
    (fun x hx ↦ (iteratedFDerivWithin_of_isOpen n hs hx).symm)

Premises used: AnalyticOn.iteratedFDerivWithin, iteratedFDerivWithin_of_isOpen, AnalyticOn.congr, IsOpen.uniqueDiffOn, Eq.symm
-- 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 : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h : AnalyticAt 𝕜 (↑f : E → F) a
h' : fderiv 𝕜 (↑f : E → F) a = (↑i : E →L[𝕜] F)
rcases :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesAt (↑f : E → F) p a),
    AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) a)
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) a)

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 : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f : E → F) a = (↑i : E →L[𝕜] F)
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f : E → F) p a
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))

Tactic:
simp [← h', 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 : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f : E → F) a = (↑i : E →L[𝕜] F)
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f : E → F) p a
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))

Tactic:
have : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i := by simp [← h', hp.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 : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f : E → F) a = (↑i : E →L[𝕜] F)
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f : E → F) p a
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) a)

Tactic:
(f.hasFPowerSeriesAt_symm h0 hp this).analyticAt

Premises used: OpenPartialHomeomorph.hasFPowerSeriesAt_symm, HasFPowerSeriesAt.analyticAt
-- 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 : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f : E → F) a = (↑i : E →L[𝕜] F)
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f : E → F) p a
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) a)

Tactic:
exact (f.hasFPowerSeriesAt_symm h0 hp this).analyticAt

Premises used: OpenPartialHomeomorph.hasFPowerSeriesAt_symm, HasFPowerSeriesAt.analyticAt
-- 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 : OpenPartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f : E → F) ((↑f.symm : F → E) a)
h' : fderiv 𝕜 (↑f : E → F) ((↑f.symm : F → E) a) = (↑i : E →L[𝕜] F)
⊢ a = (↑f : E → F) ((↑f.symm : F → E) a)

Tactic:
simp [h0]
-- 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 : OpenPartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f : E → F) ((↑f.symm : F → E) a)
h' : fderiv 𝕜 (↑f : E → F) ((↑f.symm : F → E) a) = (↑i : E →L[𝕜] F)
⊢ a = (↑f : E → F) ((↑f.symm : F → E) a)

Tactic:
have : a = f (f.symm a) := by simp [h0]
-- 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 : OpenPartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f : E → F) ((↑f.symm : F → E) a)
h' : fderiv 𝕜 (↑f : E → F) ((↑f.symm : F → E) a) = (↑i : E →L[𝕜] F)
this : a = (↑f : E → F) ((↑f.symm : F → E) a)
rw : AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) ((↑f.symm : F → E) a))
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) a

Tactic:
rw [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
f : OpenPartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f : E → F) ((↑f.symm : F → E) a)
h' : fderiv 𝕜 (↑f : E → F) ((↑f.symm : F → E) a) = (↑i : E →L[𝕜] F)
this : a = (↑f : E → F) ((↑f.symm : F → E) a)
⊢ (↑f.symm : F → E) a ∈ f.source

Tactic:
simp [h0]
-- 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 : OpenPartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f : E → F) ((↑f.symm : F → E) a)
h' : fderiv 𝕜 (↑f : E → F) ((↑f.symm : F → E) a) = (↑i : E →L[𝕜] F)
this : a = (↑f : E → F) ((↑f.symm : F → E) a)
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) ((↑f.symm : F → E) a))

Tactic:
exact f.analyticAt_symm' (by simp [h0]) h h'

Premises used: OpenPartialHomeomorph.analyticAt_symm'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 𝕜 F
f : 𝕜 → F
x : 𝕜
h : HasFPowerSeriesAt (𝕜 := 𝕜) f p x
⊢ HasStrictDerivAt f ((p 1 : (a : (i : Fin 1) → 𝕜) → F) fun (x : Fin 1) ↦ 1) x

Tactic:
h.hasStrictFDerivAt.hasStrictDerivAt

Premises used: cast, Fin.snoc, dite, HasStrictFDerivAt.hasStrictDerivAt, 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
p : FormalMultilinearSeries 𝕜 𝕜 F
f : 𝕜 → F
x : 𝕜
h : HasFPowerSeriesAt (𝕜 := 𝕜) f p x
⊢ HasDerivAt f ((p 1 : (a : (i : Fin 1) → 𝕜) → F) fun (x : Fin 1) ↦ 1) x

Tactic:
h.hasStrictDerivAt.hasDerivAt

Premises used: HasFPowerSeriesAt.hasStrictDerivAt, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 𝕜 F
f : 𝕜 → F
x : 𝕜
h : HasFPowerSeriesAt (𝕜 := 𝕜) f p x
⊢ deriv f x = (p 1 : (a : (i : Fin 1) → 𝕜) → F) fun (x : Fin 1) ↦ 1

Tactic:
h.hasDerivAt.deriv

Premises used: HasDerivAt.deriv, HasFPowerSeriesAt.hasDerivAt
-- 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
s : Set 𝕜
inst_3 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (deriv f) s

Tactic:
(ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOnNhd h.fderiv

Premises used: deriv, AnalyticOnNhd.fderiv, ContinuousLinearMap.apply, OfNat.ofNat, ContinuousLinearMap.comp_analyticOnNhd, DFunLike.coe
-- 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
s : Set 𝕜
h : AnalyticOnNhd 𝕜 f s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ AnalyticOnNhd 𝕜 (deriv f) s

Tactic:
(ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOnNhd (h.fderiv_of_isOpen hs)

Premises used: deriv, AnalyticOnNhd.fderiv_of_isOpen, ContinuousLinearMap.apply, OfNat.ofNat, ContinuousLinearMap.comp_analyticOnNhd, DFunLike.coe
-- 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
s : Set 𝕜
inst_3 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (deriv^[0] f) s

Tactic:
h

Premises used: Nat.iterate
-- 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
s : Set 𝕜
inst_3 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (deriv^[0] f) s

Tactic:
exact h
-- 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
s : Set 𝕜
inst_3 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (deriv^[n] f) s
⊢ AnalyticOnNhd 𝕜 (deriv^[n + 1] f) s

Tactic:
simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Premises used: Function.iterate_succ', AnalyticOnNhd.deriv, Function.comp_apply
-- 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
s : Set 𝕜
inst_3 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
zero : AnalyticOnNhd 𝕜 (deriv^[0] f) s
succ : ∀ (n : ℕ) (IH : AnalyticOnNhd 𝕜 (deriv^[n] f) s), AnalyticOnNhd 𝕜 (deriv^[n + 1] f) s
⊢ AnalyticOnNhd 𝕜 (deriv^[n] f) s

Tactic:
induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Premises used: Function.iterate_succ', Function.comp_apply
-- 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 : 𝕜
inst_3 : CompleteSpace F
h : AnalyticAt 𝕜 f x
obtain : ∀ (r : ℝ) (hr : 0 < r) (h : AnalyticOnNhd 𝕜 f (Metric.ball x r)), AnalyticAt 𝕜 (deriv f) x
⊢ AnalyticAt 𝕜 (deriv f) x

Tactic:
obtain ⟨r, hr, h⟩ := h.exists_ball_analyticOnNhd

Premises used: AnalyticAt.exists_ball_analyticOnNhd
-- 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 : 𝕜
inst_3 : CompleteSpace F
h_1 : AnalyticAt 𝕜 f x
r : ℝ
hr : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.ball x r)
⊢ x ∈ Metric.ball x r

Tactic:
simp [hr]
-- 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 : 𝕜
inst_3 : CompleteSpace F
h_1 : AnalyticAt 𝕜 f x
r : ℝ
hr : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.ball x r)
⊢ AnalyticAt 𝕜 (deriv f) x

Tactic:
exact h.deriv x (by simp [hr])

Premises used: AnalyticOnNhd.deriv
-- 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 : 𝕜
inst_3 : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (deriv^[0] f) x

Tactic:
h

Premises used: Nat.iterate
-- 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 : 𝕜
inst_3 : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (deriv^[0] f) x

Tactic:
exact h
-- 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 : 𝕜
inst_3 : CompleteSpace F
h : AnalyticAt 𝕜 f x
n : ℕ
IH : AnalyticAt 𝕜 (deriv^[n] f) x
⊢ AnalyticAt 𝕜 (deriv^[n + 1] f) x

Tactic:
simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Premises used: Function.iterate_succ', AnalyticAt.deriv, Function.comp_apply
-- 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 : 𝕜
inst_3 : CompleteSpace F
h : AnalyticAt 𝕜 f x
n : ℕ
zero : AnalyticAt 𝕜 (deriv^[0] f) x
succ : ∀ (n : ℕ) (IH : AnalyticAt 𝕜 (deriv^[n] f) x), AnalyticAt 𝕜 (deriv^[n + 1] f) x
⊢ AnalyticAt 𝕜 (deriv^[n] f) x

Tactic:
induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Premises used: Function.iterate_succ', Function.comp_apply
-- 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n r
⊢ DifferentiableOn 𝕜 f (Metric.eball x r)

Tactic:
fun _ hy ↦ (h.cpolynomialAt_of_mem hy).analyticAt.differentiableWithinAt

Premises used: HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem, CPolynomialAt.analyticAt, 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
⊢ HasStrictFDerivAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (x + y)

Tactic:
(h.changeOrigin hy).toHasFPowerSeriesOnBall.hasFPowerSeriesAt.hasStrictFDerivAt

Premises used: HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFPowerSeriesOnBall.hasFPowerSeriesAt, HasFiniteFPowerSeriesOnBall.changeOrigin, 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
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
⊢ HasFDerivAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (x + y)

Tactic:
(h.hasStrictFDerivAt hy).hasFDerivAt

Premises used: HasStrictFDerivAt.hasFDerivAt, HasFiniteFPowerSeriesOnBall.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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f (x + y))
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))

Tactic:
(h.hasFDerivAt hy).fderiv

Premises used: HasFDerivAt.fderiv, HasFiniteFPowerSeriesOnBall.hasFDerivAt
-- 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x n r

Tactic:
.congr (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    fun z hz ↦ ?_

Premises used: HasFiniteFPowerSeriesOnBall.congr
-- 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
refine_1 :
  HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F)
    (fun (z : E) ↦
      (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p.changeOrigin (z - x) 1))
    p.derivSeries x n r
refine_2 :
  ∀ (z : E) (hz : z ∈ Metric.eball x r),
    Eq (α := E →L[𝕜] F)
      ((fun (z : E) ↦
          ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
              (p.changeOrigin (z - x) 1) :
            E →L[𝕜] F))
        z)
      (fderiv 𝕜 f z)
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x n r

Tactic:
refine .congr (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    fun z hz ↦ ?_
-- 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F)
    (fun (z : E) ↦
      (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p.changeOrigin (z - x) 1))
    p.derivSeries x n r

Tactic:
continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall ?_

Premises used: ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall, FormalMultilinearSeries.derivSeries, continuousMultilinearCurryFin1, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
refine_1 :
  HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 1) ↦ E) F)
    (fun (z : E) ↦ p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) x n r
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F)
    (fun (z : E) ↦
      (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p.changeOrigin (z - x) 1))
    p.derivSeries x n r

Tactic:
refine continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall ?_

Premises used: ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall, continuousMultilinearCurryFin1, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 1) ↦ E) F)
    (fun (z : E) ↦ p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) x n r

Tactic:
simpa using
      ((p.hasFiniteFPowerSeriesOnBall_changeOrigin 1 h.finite).mono h.r_pos le_top).comp_sub x

Premises used: FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_changeOrigin, HasFiniteFPowerSeriesOnBall.mono, HasFiniteFPowerSeriesOnBall.comp_sub, HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, le_top, HasFiniteFPowerSeriesOnBall.finite, OfNat.ofNat, 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
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ Metric.eball x r
refine_2 : (↑‖z - x‖₊ : ℝ≥0∞) < r
⊢ Eq (α := E →L[𝕜] F)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p.changeOrigin (z - x) 1) :
      E →L[𝕜] F)
    (fderiv 𝕜 f z : E →L[𝕜] F)

Tactic:
rw [← h.fderiv_eq, add_sub_cancel]

Premises used: add_sub_cancel, HasFiniteFPowerSeriesOnBall.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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ Metric.eball x r
⊢ (↑‖z - x‖₊ : ℝ≥0∞) < r

Tactic:
simpa only [edist_eq_enorm_sub, Metric.mem_eball] using hz

Premises used: edist_eq_enorm_sub, Metric.mem_eball