awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ AnalyticWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f p s x r),
  AnalyticWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
Tactic: rcases h x hx with ⟨p, r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
hu : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s) s
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f s) s
have succ : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
  (Function.comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F)
    (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
      (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
        ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s))
  s
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
hu : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s) s
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (Function.comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s))
    s
have apply : AnalyticOnNhd 𝕜 (E := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (F :=
  ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
  (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
          ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (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)
  univ
Tactic: apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
hu : UniqueDiffOn 𝕜 s
n : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s) s
have zero : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 f s) s
Tactic: induction n with
  | zero =>
    rw [iteratedFDerivWithin_zero_eq_comp]
    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F)
      |>.comp_analyticOn h
  | succ n IH =>
    rw [iteratedFDerivWithin_succ_eq_comp_left]
    apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)
    apply LinearIsometryEquiv.analyticOnNhd
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
hu : UniqueDiffOn 𝕜 s
n : ℕ
zero :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 f s) s
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s) s
have succ : ∀ (n : ℕ)
  (IH :
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s)
      s),
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f s) s
Tactic: induction n with
  | zero =>
    rw [iteratedFDerivWithin_zero_eq_comp]
    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F)
      |>.comp_analyticOn h
  | succ n IH =>
    rw [iteratedFDerivWithin_succ_eq_comp_left]
    apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)
    apply LinearIsometryEquiv.analyticOnNhd
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s
have refine_1 : ∀ (m : ℕ) (_hm : (↑m : WithTop ℕ∞) < n) (x : E) (hx : x ∈ s),
  HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
Tactic: refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
refine_1 :
  ∀ (m : ℕ) (_hm : (↑m : WithTop ℕ∞) < n) (x : E) (hx : x ∈ s),
    HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
      (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s
have refine_2 : ∀ (m : ℕ) (_hm : (↑m : WithTop ℕ∞) ≤ n) (x : E) (hx : x ∈ s),
  ContinuousWithinAt (Y := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m) s x
Tactic: refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : (↑m : WithTop ℕ∞) < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
have this : HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
  (iteratedFDerivWithin 𝕜 m f s) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 m f s) (insert x s) x) (insert x s) x
Tactic: have := (h.iteratedFDerivWithin hu m x hx).differentiableWithinAt.hasFDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : (↑m : WithTop ℕ∞) < n
x : E
hx : x ∈ s
this :
  HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (iteratedFDerivWithin 𝕜 m f s) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 m f s) (insert x s) x) (insert x s) x
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
have refine_1 : ∀
  (this :
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
      (iteratedFDerivWithin 𝕜 m f s) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x) s x),
  HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeriesWithin 𝕜 f s x m.succ)) s x
Tactic: rwa [insert_eq_of_mem hx] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ AnalyticOnNhd 𝕜 (F := E →L[𝕜] F) (fderiv 𝕜 f) s
have rw : ∀ (h : AnalyticOn 𝕜 f s) (hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
  AnalyticOn 𝕜 (F := E →L[𝕜] F) (fderiv 𝕜 f) s
Tactic: rw [← hs.analyticOn_iff_analyticOnNhd] at h ⊢
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) s
have rw : ∀ (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: rw [← hs.analyticOn_iff_analyticOnNhd] at h ⊢
Cleared hypotheses: h, hs, n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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)
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) a)
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesAt (↑f : E → F) p a),
  AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) a)
Tactic: rcases h with ⟨p, hp⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
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
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) a)
have 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))
Tactic: have : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i := by simp [← h', hp.fderiv_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
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)
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) a
have this : a = (↑f : E → F) ((↑f.symm : F → E) a)
Tactic: have : a = f (f.symm a) := by simp [h0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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) a
have rw : AnalyticAt 𝕜 (↑f.symm : F → E) ((↑f : E → F) ((↑f.symm : F → E) a))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 : ℕ
⊢ AnalyticOnNhd 𝕜 (deriv^[n] f) s
have zero : AnalyticOnNhd 𝕜 (deriv^[0] f) s
Tactic: induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ AnalyticOnNhd 𝕜 (deriv^[n] f) s
have succ : ∀ (n : ℕ) (IH : AnalyticOnNhd 𝕜 (deriv^[n] f) s), AnalyticOnNhd 𝕜 (deriv^[n + 1] f) s
Tactic: induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 f) x
have obtain : ∀ (r : ℝ) (hr : 0 < r) (h : AnalyticOnNhd 𝕜 f (Metric.ball x r)), AnalyticAt 𝕜 (deriv f) x
Tactic: obtain ⟨r, hr, h⟩ := h.exists_ball_analyticOnNhd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 : ℕ
⊢ AnalyticAt 𝕜 (deriv^[n] f) x
have zero : AnalyticAt 𝕜 (deriv^[0] f) x
Tactic: induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ AnalyticAt 𝕜 (deriv^[n] f) x
have succ : ∀ (n : ℕ) (IH : AnalyticAt 𝕜 (deriv^[n] f) x), AnalyticAt 𝕜 (deriv^[n + 1] f) x
Tactic: induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
have 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
Tactic: refine .congr (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    fun z hz ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x n r
have 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)
Tactic: refine .congr (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    fun z hz ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
have 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
Tactic: refine continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ 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)
have refine_2 : (↑‖z - x‖₊ : ℝ≥0∞) < r
Tactic: rw [← h.fderiv_eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (n - 1) r
have inl : ∀ (h : HasFiniteFPowerSeriesOnBall f p x 0 r),
  HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (HSub.hSub (α := ℕ) 0 1) r
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
inl :
  ∀ (h : HasFiniteFPowerSeriesOnBall f p x 0 r),
    HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (HSub.hSub (α := ℕ) 0 1) r
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (n - 1) r
have inr : ∀ (hn : n ≠ 0), HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (n - 1) r
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
h : HasFiniteFPowerSeriesOnBall f p x 0 r
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x 0 r
have inl : ∀ (y : E) (hy : y ∈ Metric.eball x r), Eq (α := E →L[𝕜] F) (fderiv 𝕜 f y) 0
Tactic: refine HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (fun y hy ↦ ?_) h.r_pos fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
h : HasFiniteFPowerSeriesOnBall f p x 0 r
inl : ∀ (y : E) (hy : y ∈ Metric.eball x r), Eq (α := E →L[𝕜] F) (fderiv 𝕜 f y) 0
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x 0 r
have inl₁ : ∀ (n : ℕ), p.derivSeries n = 0
Tactic: refine HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (fun y hy ↦ ?_) h.r_pos fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
h : HasFiniteFPowerSeriesOnBall f p x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f y) 0
have inl : Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ 0) y) 0
Tactic: rw [Filter.EventuallyEq.fderiv_eq (f := fun _ ↦ 0)]