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
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z :
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert (x + y) s) (x + y)
inr : s ∈ 𝓝[insert x s] (x + y)
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert x s) (x + y)

Tactic:
apply (Z.mono (subset_insert _ _)).mono_of_mem_nhdsWithin

Premises used: HasFDerivWithinAt.mono_of_mem_nhdsWithin, HasFDerivWithinAt.mono, Set.subset_insert
-- 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
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z :
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert (x + y) s) (x + y)
inr : s ∈ 𝓝[s] (x + y)
inr₁ : x + y ≠ x
⊢ s ∈ 𝓝[insert x s] (x + y)

Tactic:
rw [nhdsWithin_insert_of_ne]

Premises used: nhdsWithin_insert_of_ne
-- 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
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z :
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert (x + y) s) (x + y)
⊢ s ∈ 𝓝[s] (x + y)

Tactic:
self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin
-- 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
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z :
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert (x + y) s) (x + y)
⊢ s ∈ 𝓝[s] (x + y)

Tactic:
exact self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin
-- 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
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z :
  HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (insert (x + y) s) (x + y)
⊢ x + y ≠ x

Tactic:
simpa using h''y
-- 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
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
⊢ HasFDerivAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))
    (x + y)

Tactic:
(h.changeOrigin hy).hasFPowerSeriesAt.hasFDerivAt

Premises used: HasFPowerSeriesAt.hasFDerivAt, HasFPowerSeriesOnBall.changeOrigin, HasFPowerSeriesOnBall.hasFPowerSeriesAt
-- 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
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hu : UniqueDiffOn 𝕜 (insert x s)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s) (x + y))
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))

Tactic:
(h.hasFDerivWithinAt hy h'y).fderivWithin (hu _ h'y)

Premises used: HasFDerivWithinAt.fderivWithin, HasFPowerSeriesWithinOnBall.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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f (x + y))
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p.changeOrigin y 1))

Tactic:
(h.hasFDerivAt hy).fderiv

Premises used: HasFDerivAt.fderiv, HasFPowerSeriesOnBall.hasFDerivAt
-- 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
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x r

Tactic:
.congr (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    fun z hz ↦ ?_

Premises used: HasFPowerSeriesOnBall.congr
-- 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
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
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)
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x r

Tactic:
refine .congr (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    fun z hz ↦ ?_
-- 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
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

Tactic:
continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesOnBall ?_

Premises used: FormalMultilinearSeries.derivSeries, continuousMultilinearCurryFin1, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, LinearIsometryEquiv.toContinuousLinearEquiv, 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
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 := 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
⊢ 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 continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesOnBall ?_

Premises used: continuousMultilinearCurryFin1, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, LinearIsometryEquiv.toContinuousLinearEquiv, 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ 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:
simpa using ((p.hasFPowerSeriesOnBall_changeOrigin 1
      (h.r_pos.trans_le h.r_le)).mono h.r_pos h.r_le).comp_sub x

Premises used: HasFPowerSeriesOnBall.comp_sub, HasFPowerSeriesOnBall.r_le, LT.lt.trans_le, OfNat.ofNat, HasFPowerSeriesOnBall.mono, HasFPowerSeriesOnBall.r_pos, FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin
-- 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
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
z : E
hz : z ∈ Metric.eball x r
refine_2 : (↑‖z - x‖₊ : ℝ≥0∞) < 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)

Tactic:
rw [← h.fderiv_eq, add_sub_cancel]

Premises used: HasFPowerSeriesOnBall.fderiv_eq, add_sub_cancel
-- 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
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
z : E
hz : z ∈ Metric.eball x r
⊢ (↑‖z - x‖₊ : ℝ≥0∞) < r

Tactic:
simpa only [edist_eq_enorm_sub, Metric.mem_eball] using hz

Premises used: edist_eq_enorm_sub, Metric.mem_eball
-- 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)
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r

Tactic:
.congr' (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    (fun z hz ↦ ?_)

Premises used: HasFPowerSeriesWithinOnBall.congr'
-- 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)
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
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)
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r

Tactic:
refine .congr' (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
    (fun z hz ↦ ?_)
-- 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)
⊢ 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:
continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall ?_

Premises used: FormalMultilinearSeries.derivSeries, continuousMultilinearCurryFin1, ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall, LinearIsometryEquiv.toContinuousLinearEquiv, 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
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 := 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
⊢ 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 continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall ?_

Premises used: continuousMultilinearCurryFin1, ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall, LinearIsometryEquiv.toContinuousLinearEquiv, 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
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 :
  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
⊢ 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:
apply HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall

Premises used: HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall
-- 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)
⊢ 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:
simpa using ((p.hasFPowerSeriesOnBall_changeOrigin 1
      (h.r_pos.trans_le h.r_le)).mono h.r_pos h.r_le).comp_sub x

Premises used: HasFPowerSeriesOnBall.comp_sub, HasFPowerSeriesWithinOnBall.r_le, LT.lt.trans_le, HasFPowerSeriesWithinOnBall.r_pos, OfNat.ofNat, HasFPowerSeriesOnBall.mono, FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin
-- 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)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
rw : (↑‖z - x‖₊ : ℝ≥0∞) < r
rw₁ : x + (z - x) ∈ insert x s
⊢ 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))

Tactic:
rw [← h.fderivWithin_eq _ _ hu, add_sub_cancel]

Premises used: add_sub_cancel, HasFPowerSeriesWithinOnBall.fderivWithin_eq
-- 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)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ (↑‖z - x‖₊ : ℝ≥0∞) < r

Tactic:
simpa only [edist_eq_enorm_sub, Metric.mem_eball] using hz.2

Premises used: edist_eq_enorm_sub, And.right, Metric.mem_eball
-- 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)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ x + (z - x) ∈ insert x s

Tactic:
simpa using hz.1

Premises used: And.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
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
⊢ insert x s = s

Tactic:
have : insert x s = s := insert_eq_of_mem 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
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
⊢ UniqueDiffOn 𝕜 (insert x s)

Tactic:
rw [← this] at hu
-- 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 𝕜 s
hx : x ∈ s
this : insert x s = s
hu₁ : UniqueDiffOn 𝕜 (insert x s)
⊢ x ∈ s

Tactic:
rw [← this] at hu
-- 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 𝕜 s
hx : x ∈ s
this : insert x s = s
hu₁ : UniqueDiffOn 𝕜 (insert x s)
hx₁ : x ∈ s
⊢ insert x s = s

Tactic:
rw [← this] at hu
-- 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
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r

Tactic:
h.fderivWithin hu

Premises used: HasFPowerSeriesWithinOnBall.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
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
hx : x ∈ s
this : insert x s = s
h₁ : s = insert x s
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) p.derivSeries s x r

Tactic:
convert! h.fderivWithin hu

Premises used: HasFPowerSeriesWithinOnBall.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
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:
this.symm

Premises used: Eq.symm