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
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
⊢ s = insert x s

Tactic:
exact this.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
inst_5 : CompleteSpace F
h : AnalyticAt 𝕜 f x
rcases :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hp : HasFPowerSeriesOnBall f p x r),
    AnalyticAt 𝕜 (F := E →L[𝕜] F) (fderiv 𝕜 f) x
⊢ AnalyticAt 𝕜 (F := E →L[𝕜] F) (fderiv 𝕜 f) x

Tactic:
rcases h with ⟨p, r, hp⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 (F := E →L[𝕜] F) (fderiv 𝕜 f) x

Tactic:
hp.fderiv.analyticAt

Premises used: HasFPowerSeriesOnBall.fderiv, HasFPowerSeriesOnBall.analyticAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 (F := E →L[𝕜] F) (fderiv 𝕜 f) x

Tactic:
exact hp.fderiv.analyticAt

Premises used: HasFPowerSeriesOnBall.fderiv, HasFPowerSeriesOnBall.analyticAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (F := E →L[𝕜] F) (fderiv 𝕜 f) s

Tactic:
fun y hy ↦ AnalyticAt.fderiv (h y hy)

Premises used: AnalyticOnNhd, AnalyticAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
      f)
    s

Tactic:
((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F).comp_analyticOnNhd h

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearMap.comp_analyticOnNhd, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
      f)
    s

Tactic:
exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F).comp_analyticOnNhd h

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearMap.comp_analyticOnNhd, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
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
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
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (n + 1) f) s

Tactic:
rw [iteratedFDeriv_succ_eq_comp_left]

Premises used: iteratedFDeriv_succ_eq_comp_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
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 𝕜 (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)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f)))
    s

Tactic:
ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv

Premises used: AnalyticOnNhd.fderiv, ContinuousLinearMap.comp_analyticOnNhd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
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)
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
⊢ 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:
convert! ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv

Premises used: AnalyticOnNhd.fderiv, ContinuousLinearMap.comp_analyticOnNhd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
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
⊢ (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:
exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryLeftEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
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
⊢ (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:
case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryLeftEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
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
⊢ 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:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
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
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
⊢ AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n 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

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, iteratedFDeriv_zero_eq_comp, LinearIsometryEquiv.toContinuousLinearEquiv, continuousMultilinearCurryLeftEquiv, iteratedFDeriv_succ_eq_comp_left, ContinuousLinearMap.comp_analyticOnNhd, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 f) s

Tactic:
⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩

Premises used: HasFTaylorSeriesUpToOn.mk, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
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
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
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 f) s

Tactic:
refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : (↑m : WithTop ℕ∞) < n
x : E
hx : x ∈ s
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
⊢ 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:
apply HasFDerivAt.hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : (↑m : WithTop ℕ∞) < n
x : E
hx : x ∈ s
⊢ 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:
((h.iteratedFDeriv m x hx).differentiableAt).hasFDerivAt

Premises used: Eq.mpr, AnalyticOnNhd.iteratedFDeriv, ftaylorSeries, Fin.cons, Fin.induction.go, ContinuousMultilinearMap.curryLeft, MultilinearMap.mkContinuous, DifferentiableAt.hasFDerivAt, Fin.induction, MultilinearMap.mk', AnalyticAt.differentiableAt, Fin.cases, iteratedFDeriv, MultilinearMap.mkContinuousLinear, Fin.tail, LinearMap.mkContinuous
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : (↑m : WithTop ℕ∞) < n
x : E
hx : x ∈ s
⊢ 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:
exact ((h.iteratedFDeriv m x hx).differentiableAt).hasFDerivAt

Premises used: AnalyticOnNhd.iteratedFDeriv, DifferentiableAt.hasFDerivAt, AnalyticAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : (↑m : WithTop ℕ∞) ≤ n
x : E
hx : x ∈ s
apply :
  DifferentiableAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeries 𝕜 f x m) x
⊢ ContinuousWithinAt (Y := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeries 𝕜 f x m) s x

Tactic:
apply (DifferentiableAt.continuousAt (𝕜 := 𝕜) ?_).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, DifferentiableAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : (↑m : WithTop ℕ∞) ≤ n
x : E
hx : x ∈ s
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeries 𝕜 f x m) x

Tactic:
(h.iteratedFDeriv m x hx).differentiableAt

Premises used: AnalyticOnNhd.iteratedFDeriv, ftaylorSeries, AnalyticAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
inst_5 : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : (↑m : WithTop ℕ∞) ≤ n
x : E
hx : x ∈ s
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin m) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeries 𝕜 f x m) x

Tactic:
exact (h.iteratedFDeriv m x hx).differentiableAt

Premises used: AnalyticOnNhd.iteratedFDeriv, AnalyticAt.differentiableAt
-- 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
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
⊢ ∃ 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⟩

Premises used: AnalyticWithinAt.exists_analyticAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : 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
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
⊢ ∃ 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⟩

Premises used: AnalyticAt.exists_mem_nhds_analyticOnNhd
-- 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
⊢ ∃ 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:
⟨insert x s ∩ v, inter_mem_nhdsWithin _ vx, ftaylorSeries 𝕜 g, ?_, fun i ↦ ?_⟩

Premises used: inter_mem_nhdsWithin, ftaylorSeries, Insert.insert, Inter.inter, And.intro, Exists.intro