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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x r
have refine_1 : HasFPowerSeriesOnBall (𝕜 := 𝕜) (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 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∞
f : E → F
x : E
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
refine_1 :
  HasFPowerSeriesOnBall (𝕜 := 𝕜) (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 r
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x 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∞
f : E → F
x : E
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (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 r
have refine_1 : HasFPowerSeriesOnBall (𝕜 := 𝕜) (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 r
Tactic: refine continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesOnBall ?_
-- 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
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x 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∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r
have refine_1 : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (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 s x 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∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
refine_1 :
  HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (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 s x r
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r
have refine_2 : ∀ (z : E) (hz : z ∈ insert x s ∩ Metric.eball x r),
  Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s) z)
    ((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)
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∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (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 s x r
have refine_1 : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 1) ↦ E) F)
  (fun (z : E) ↦ p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) s x r
Tactic: refine continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall ?_
-- 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
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 1) ↦ E) F)
    (fun (z : E) ↦ p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) s x r
have refine_1 : HasFPowerSeriesOnBall (𝕜 := 𝕜) (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 r
Tactic: apply HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall
-- 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
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s) z)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin (z - x) 1))
have rw : (↑‖z - x‖₊ : ℝ≥0∞) < r
Tactic: rw [← h.fderivWithin_eq _ _ hu, 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∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
rw : (↑‖z - x‖₊ : ℝ≥0∞) < r
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s) z)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin (z - x) 1))
have rw₁ : x + (z - x) ∈ insert x s
Tactic: rw [← h.fderivWithin_eq _ _ hu, add_sub_cancel]
-- 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
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) p.derivSeries s x r
have this : insert x s = s
Tactic: have : insert x s = s := insert_eq_of_mem 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : insert x s = s
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) p.derivSeries s x r
have hu₁ : UniqueDiffOn 𝕜 (insert x s)
Tactic: rw [← this] at hu
Cleared hypotheses: hu, hx, 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
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
hx : x ∈ s
this : insert x s = s
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) p.derivSeries s x r
have h₁ : s = insert x s
Tactic: convert! h.fderivWithin hu
-- 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
inst_5 : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (F := E →L[𝕜] F) (fderiv 𝕜 f) x
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hp : HasFPowerSeriesOnBall f p x r),
  AnalyticAt 𝕜 (F := E →L[𝕜] F) (fderiv 𝕜 f) x
Tactic: rcases h with ⟨p, r, hp⟩
Cleared hypotheses: 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
f : E → F
s : Set E
inst_5 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (n + 1) f) s
have succ : AnalyticOnNhd 𝕜 (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)
    (fderiv 𝕜 (iteratedFDeriv 𝕜 n f)))
  s
Tactic: rw [iteratedFDeriv_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
inst_5 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOnNhd 𝕜 (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)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f)))
    s
have h₁ : Eq (α :=
  (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)
  (⇑(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)
  (⇑((↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)) :
              (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) ≃L[𝕜]
                ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
          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 (i : Fin (n + 1)) ↦ E) F)
Tactic: convert! ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv
-- 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
inst_5 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) s
h₁ :
  Eq (α :=
    (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)
    (⇑(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)
    (⇑((↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)) :
                (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) ≃L[𝕜]
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
            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 (i : Fin (n + 1)) ↦ E) F)
⊢ AnalyticOnNhd 𝕜 (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)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f)))
    s
have convert! : (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
  ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F
Tactic: convert! ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv
-- 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
inst_5 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) s
have zero : AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f) s
Tactic: induction n with
  | zero =>
    rw [iteratedFDeriv_zero_eq_comp]
    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F).comp_analyticOnNhd h
  | succ n IH =>
    rw [iteratedFDeriv_succ_eq_comp_left]
    -- Porting note: for reasons that I do not understand at all, `?g` cannot be inlined.
    convert! ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv
    case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm
    simp
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
inst_5 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
zero : AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f) s
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) s
have succ : ∀ (n : ℕ)
  (IH :
    AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) s),
  AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (n + 1) f) s
Tactic: induction n with
  | zero =>
    rw [iteratedFDeriv_zero_eq_comp]
    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F).comp_analyticOnNhd h
  | succ n IH =>
    rw [iteratedFDeriv_succ_eq_comp_left]
    -- Porting note: for reasons that I do not understand at all, `?g` cannot be inlined.
    convert! ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv
    case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm
    simp
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
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 f) 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) ↦ ftaylorSeries 𝕜 f x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeries 𝕜 f 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
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f 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) ↦ ftaylorSeries 𝕜 f x m)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeries 𝕜 f x m.succ)) s x
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 f) 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) ↦ ftaylorSeries 𝕜 f 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 (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
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f 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) ↦ ftaylorSeries 𝕜 f x m)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeries 𝕜 f x m.succ)) s x
have refine_1 : HasFDerivAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
  (fun (x : E) ↦ ftaylorSeries 𝕜 f x m)
  (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (ftaylorSeries 𝕜 f x m.succ)) x
Tactic: apply HasFDerivAt.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
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
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) ↦ ftaylorSeries 𝕜 f x m) s x
have apply : DifferentiableAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
  (fun (x : E) ↦ ftaylorSeries 𝕜 f x m) x
Tactic: apply (DifferentiableAt.continuousAt (𝕜 := 𝕜) ?_).continuousWithinAt