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
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)
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)
⊢ ∃ 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:
refine ⟨insert x s ∩ v, inter_mem_nhdsWithin _ vx, ftaylorSeries 𝕜 g, ?_, fun i ↦ ?_⟩
-- 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
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 g (ftaylorSeries 𝕜 g) (insert x s ∩ v)
⊢ HasFTaylorSeriesUpToOn n f (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)
-- 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
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 g (ftaylorSeries 𝕜 g) (insert x s ∩ v)

Tactic:
AnalyticOnNhd.hasFTaylorSeriesUpToOn _ (hv.mono Set.inter_subset_right)

Premises used: AnalyticOnNhd.mono, AnalyticOnNhd.hasFTaylorSeriesUpToOn, Set.inter_subset_right
-- 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
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 g (ftaylorSeries 𝕜 g) (insert x s ∩ v)

Tactic:
exact AnalyticOnNhd.hasFTaylorSeriesUpToOn _ (hv.mono Set.inter_subset_right)

Premises used: AnalyticOnNhd.mono, AnalyticOnNhd.hasFTaylorSeriesUpToOn, Set.inter_subset_right
-- 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
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
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:
(hv.iteratedFDeriv i).analyticOn.mono Set.inter_subset_right

Premises used: AnalyticOnNhd.iteratedFDeriv, ftaylorSeries, AnalyticOnNhd.analyticOn, Set.inter_subset_right, AnalyticOn.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
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
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:
exact (hv.iteratedFDeriv i).analyticOn.mono Set.inter_subset_right

Premises used: AnalyticOnNhd.iteratedFDeriv, AnalyticOnNhd.analyticOn, Set.inter_subset_right, AnalyticOn.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
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ₗᵢ
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')
⊢ HasSum (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y) f'

Tactic:
rw [← b.isEmbedding.hasSum_iff]

Premises used: LinearIsometry.isEmbedding, Topology.IsEmbedding.toIsInducing, Topology.IsInducing.hasSum_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
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ₗᵢ
⊢ 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
-- 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
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
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) y

Tactic:
simpa [edist_zero_right] using hy

Premises used: edist_zero_right
-- 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
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')
    (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)
-- 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
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))
apply : HasFDerivWithinAt ((⇑a : (a : F) → F') ∘ f) (a ∘SL f') (insert x s) (x + y)
⊢ fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y) = a ∘SL f'

Tactic:
apply HasFDerivWithinAt.fderivWithin _ (hu _ h'y)

Premises used: HasFDerivWithinAt.fderivWithin
-- 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
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))
⊢ HasFDerivWithinAt ((⇑a : (a : F) → F') ∘ f) (a ∘SL f') (insert x s) (x + y)

Tactic:
a.hasFDerivAt.comp_hasFDerivWithinAt (x + y) hf'

Premises used: ContinuousLinearMap.hasFDerivAt, HasFDerivAt.comp_hasFDerivWithinAt, HAdd.hAdd
-- 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
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))
⊢ HasFDerivWithinAt ((⇑a : (a : F) → F') ∘ f) (a ∘SL f') (insert x s) (x + y)

Tactic:
exact a.hasFDerivAt.comp_hasFDerivWithinAt (x + y) hf'

Premises used: ContinuousLinearMap.hasFDerivAt, HasFDerivAt.comp_hasFDerivWithinAt, HAdd.hAdd
-- 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
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'

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'
-- 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
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
    (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
-- 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
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'
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')
⊢ fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y) = a ∘SL f'

Tactic:
rw [this] at Z
-- 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
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
    (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:
Z
-- 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
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'
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)
⊢ 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:
convert! Z with n
-- 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
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 : ℕ
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')
⊢ 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:
ext v
-- 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
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')
    (∑ 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))) ⋯ :
                  (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))) ⋯ :
                (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F')
              fun (x : Fin n) ↦ y) :
          (a : E) → F')
        v)

Tactic:
rfl