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
x : E
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn n f p u ∧
        ∀ (i : ℕ),
          AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
have rcases : ∀ (g : E → F) (fg : EqOn f g (insert x s)) (hg : AnalyticAt 𝕜 g x),
  ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn n f p u ∧
        ∀ (i : ℕ),
          AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
Tactic: rcases h.exists_analyticAt with ⟨g, -, fg, hg⟩
-- 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
x : E
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn n f p u ∧
        ∀ (i : ℕ),
          AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
have rcases : ∀ (v : Set E) (vx : v ∈ 𝓝 x) (hv : AnalyticOnNhd 𝕜 g v),
  ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn n f p u ∧
        ∀ (i : ℕ),
          AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
Tactic: rcases hg.exists_mem_nhds_analyticOnNhd with ⟨v, vx, hv⟩
-- 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
x : E
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn n f p u ∧
        ∀ (i : ℕ),
          AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
have refine_1 : HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 g) (insert x s ∩ v)
Tactic: refine ⟨insert x s ∩ v, inter_mem_nhdsWithin _ vx, ftaylorSeries 𝕜 g, ?_, fun i ↦ ?_⟩
-- 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
x : E
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
refine_1 : HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 g) (insert x s ∩ v)
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
      HasFTaylorSeriesUpToOn n f p u ∧
        ∀ (i : ℕ),
          AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
have refine_2 : ∀ (i : ℕ),
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeries 𝕜 g x i) (insert x s ∩ v)
Tactic: refine ⟨insert x s ∩ v, inter_mem_nhdsWithin _ vx, ftaylorSeries 𝕜 g, ?_, fun i ↦ ?_⟩
-- 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
x : E
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 g) (insert x s ∩ v)
have refine_1 : HasFTaylorSeriesUpToOn n g (ftaylorSeries 𝕜 g) (insert x s ∩ v)
Tactic: suffices HasFTaylorSeriesUpToOn n g (ftaylorSeries 𝕜 g) (insert x s ∩ v) from
      this.congr (fun y hy ↦ fg hy.1)
-- 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
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
⊢ HasSum (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y) f'
have rw : HasSum (α := E →L[𝕜] F')
  (Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F') fun (n : ℕ) ↦
      (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y :
    ℕ → E →L[𝕜] F')
  ((b : (a : E →L[𝕜] F) → E →L[𝕜] F') f' : E →L[𝕜] F')
Tactic: rw [← b.isEmbedding.hasSum_iff]
-- 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
⊢ HasSum (α := E →L[𝕜] F')
    (Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F') fun (n : ℕ) ↦
        (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y :
      ℕ → E →L[𝕜] F')
    ((b : (a : E →L[𝕜] F) → E →L[𝕜] F') f' : E →L[𝕜] F')
have this : HasFPowerSeriesWithinOnBall.{u_1, u, v} (𝕜 := 𝕜) (F := F') ((⇑a : (a : F) → F') ∘ f) (a.compFormalMultilinearSeries p) s
  x r
Tactic: have : HasFPowerSeriesWithinOnBall (a ∘ f) (a.compFormalMultilinearSeries p) s x r :=
    a.comp_hasFPowerSeriesWithinOnBall 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
this :
  HasFPowerSeriesWithinOnBall.{u_1, u, v} (𝕜 := 𝕜) (F := F') ((⇑a : (a : F) → F') ∘ f) (a.compFormalMultilinearSeries p)
    s x r
⊢ HasSum (α := E →L[𝕜] F')
    (Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F') fun (n : ℕ) ↦
        (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y :
      ℕ → E →L[𝕜] F')
    ((b : (a : E →L[𝕜] F) → E →L[𝕜] F') f' : E →L[𝕜] F')
have Z : HasSum (α := E →L[𝕜] F')
  (fun (n : ℕ) ↦
    (FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
      fun (x : Fin n) ↦ y)
  (fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y))
Tactic: have Z := (this.fderivWithin hu).hasSum h'y (by simpa [edist_zero_right] using hy)
-- 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
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
this :
  HasFPowerSeriesWithinOnBall.{u_1, u, v} (𝕜 := 𝕜) (F := F') ((⇑a : (a : F) → F') ∘ f) (a.compFormalMultilinearSeries p)
    s x r
Z :
  HasSum (α := E →L[𝕜] F')
    (fun (n : ℕ) ↦
      (FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
        fun (x : Fin n) ↦ y)
    (fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y))
⊢ fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y) = a ∘SL f'
have apply : HasFDerivWithinAt ((⇑a : (a : F) → F') ∘ f) (a ∘SL f') (insert x s) (x + y)
Tactic: apply HasFDerivWithinAt.fderivWithin _ (hu _ h'y)
-- 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
this :
  HasFPowerSeriesWithinOnBall.{u_1, u, v} (𝕜 := 𝕜) (F := F') ((⇑a : (a : F) → F') ∘ f) (a.compFormalMultilinearSeries p)
    s x r
Z :
  HasSum (α := E →L[𝕜] F')
    (fun (n : ℕ) ↦
      (FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
        fun (x : Fin n) ↦ y)
    (fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y))
⊢ HasSum (α := E →L[𝕜] F')
    (Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F') fun (n : ℕ) ↦
        (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y :
      ℕ → E →L[𝕜] F')
    ((b : (a : E →L[𝕜] F) → E →L[𝕜] F') f' : E →L[𝕜] F')
have this₁ : fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y) = a ∘SL f'
Tactic: have : fderivWithin 𝕜 (a ∘ f) (insert x s) (x + y) = a ∘L f' := by
    apply HasFDerivWithinAt.fderivWithin _ (hu _ h'y)
    exact a.hasFDerivAt.comp_hasFDerivWithinAt (x + y) hf'
-- 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
this_1 :
  HasFPowerSeriesWithinOnBall.{u_1, u, v} (𝕜 := 𝕜) (F := F') ((⇑a : (a : F) → F') ∘ f) (a.compFormalMultilinearSeries p)
    s x r
Z :
  HasSum (α := E →L[𝕜] F')
    (fun (n : ℕ) ↦
      (FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
        fun (x : Fin n) ↦ y)
    (fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y))
this : fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y) = a ∘SL f'
⊢ HasSum (α := E →L[𝕜] F')
    (Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F') fun (n : ℕ) ↦
        (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y :
      ℕ → E →L[𝕜] F')
    ((b : (a : E →L[𝕜] F) → E →L[𝕜] F') f' : E →L[𝕜] F')
have Z₁ : HasSum
  (fun (n : ℕ) ↦
    (FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
      fun (x : Fin n) ↦ y)
  (a ∘SL f')
Tactic: rw [this] at Z
Cleared hypotheses: Z, 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
this_1 :
  HasFPowerSeriesWithinOnBall.{u_1, u, v} (𝕜 := 𝕜) (F := F') ((⇑a : (a : F) → F') ∘ f) (a.compFormalMultilinearSeries p)
    s x r
Z :
  HasSum
    (fun (n : ℕ) ↦
      (FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
        fun (x : Fin n) ↦ y)
    (a ∘SL f')
this : fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y) = a ∘SL f'
⊢ HasSum (α := E →L[𝕜] F')
    (Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F') fun (n : ℕ) ↦
        (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y :
      ℕ → E →L[𝕜] F')
    ((b : (a : E →L[𝕜] F) → E →L[𝕜] F') f' : E →L[𝕜] F')
have h₁ : ∀ (n : ℕ),
  Eq (α := E →L[𝕜] F')
    (Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F')
      (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y) n)
    ((FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
      fun (x : Fin n) ↦ y)
Tactic: convert! Z with 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
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
this_1 :
  HasFPowerSeriesWithinOnBall.{u_1, u, v} (𝕜 := 𝕜) (F := F') ((⇑a : (a : F) → F') ∘ f) (a.compFormalMultilinearSeries p)
    s x r
Z :
  HasSum
    (fun (n : ℕ) ↦
      (FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
        fun (x : Fin n) ↦ y)
    (a ∘SL f')
this : fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y) = a ∘SL f'
n : ℕ
⊢ Eq (α := E →L[𝕜] F')
    (Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F')
      (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y) n)
    ((FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
      fun (x : Fin n) ↦ y)
have h₁ : ∀ (v : E),
  Eq.{v + 1} (α := F')
    (((Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F')
              (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y) n :
            E →L[𝕜] F') :
          (a : E) → F')
        v :
      F')
    (((FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
            fun (x : Fin n) ↦ y :
          (a : E) → F')
        v :
      F')
Tactic: ext v
-- 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
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
this_1 :
  HasFPowerSeriesWithinOnBall.{u_1, u, v} (𝕜 := 𝕜) (F := F') ((⇑a : (a : F) → F') ∘ f) (a.compFormalMultilinearSeries p)
    s x r
Z :
  HasSum
    (fun (n : ℕ) ↦
      (FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
        fun (x : Fin n) ↦ y)
    (a ∘SL f')
this : fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y) = a ∘SL f'
n : ℕ
v : E
⊢ Eq.{v + 1} (α := F')
    (((Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F')
              (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y) n :
            E →L[𝕜] F') :
          (a : E) → F')
        v :
      F')
    (((FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
            fun (x : Fin n) ↦ y :
          (a : E) → F')
        v :
      F')
have h₁ : Eq.{v + 1} (α := F')
  (∑ c : { s : Finset (Fin (1 + n)) // s.card = n },
    ((b : (a : E →L[𝕜] F) → E →L[𝕜] F')
          ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
            ((p.changeOriginSeriesTerm 1 n (↑c : Finset (Fin (1 + n))) sorry :
                (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
              fun (x : Fin n) ↦ y)) :
        (a : E) → F')
      v)
  (∑ c : { s : Finset (Fin (1 + n)) // s.card = n },
    ((continuousMultilinearCurryFin1 𝕜 E F' : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F') → E →L[𝕜] F')
          ((FormalMultilinearSeries.changeOriginSeriesTerm (a.compFormalMultilinearSeries p) 1 n
                (↑c : Finset (Fin (1 + n))) sorry :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F')
            fun (x : Fin n) ↦ y) :
        (a : E) → F')
      v)
Tactic: simp only [FormalMultilinearSeries.derivSeries, ContinuousLinearMap.coe_sum', Finset.sum_apply,
    ContinuousLinearMap.compFormalMultilinearSeries_apply,
    FormalMultilinearSeries.changeOriginSeries,
    ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_coe, Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum]
-- 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
s : Set E
hr : HasFPowerSeriesWithinOnBall f p s x r
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) p.derivSeries s x r
have refine : ∀ {y : E} (hy : x + y ∈ insert x s) (h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y),
  HasSum (α := E →L[𝕜] F) (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y)
    (fderivWithin 𝕜 f s (x + y))
Tactic: refine ⟨hr.r_le.trans p.radius_le_radius_derivSeries, hr.r_pos, fun {y} hy h'y ↦ ?_⟩
-- 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
s : Set E
hr : HasFPowerSeriesWithinOnBall f p s x r
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum (α := E →L[𝕜] F) (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y)
    (fderivWithin 𝕜 f s (x + y))
have hf' : HasFDerivWithinAt f (fderivWithin 𝕜 f s (x + y)) (insert x s) (x + y)
Tactic: apply hr.hasSum_derivSeries_of_hasFDerivWithinAt (by simpa [edist_zero_right] using h'y) hy
-- 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
s : Set E
hr : HasFPowerSeriesWithinOnBall f p s x r
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hf' : HasFDerivWithinAt f (fderivWithin 𝕜 f s (x + y)) (insert x s) (x + y)
⊢ HasSum (α := E →L[𝕜] F) (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y)
    (fderivWithin 𝕜 f s (x + y))
have hu : UniqueDiffOn 𝕜 (insert x s)
Tactic: apply hr.hasSum_derivSeries_of_hasFDerivWithinAt (by simpa [edist_zero_right] using h'y) hy
-- 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
s : Set E
hr : HasFPowerSeriesWithinOnBall f p s x r
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f s (x + y)) (insert x s) (x + y)
have hf' : ∀ (hy : x + y ∈ s) (h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y),
  HasFDerivWithinAt f (fderivWithin 𝕜 f s (x + y)) s (x + y)
Tactic: rw [insert_eq_of_mem hx] at hy ⊢
Cleared hypotheses: hy, h'y
-- 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
s : Set E
hr : HasFPowerSeriesWithinOnBall f p s x r
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
y : E
hy : x + y ∈ s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f s (x + y)) s (x + y)
have hf' : DifferentiableWithinAt 𝕜 f s (x + y)
Tactic: apply DifferentiableWithinAt.hasFDerivWithinAt