mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
IH : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) ⊆ tsupport f

Tactic:
]

Goal state after:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
IH : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) ⊆ tsupport f
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[s] y

Tactic:
]

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ s ∈ 𝓝[s] y
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ ‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDeriv 𝕜 m f x

Tactic:
rw [← iteratedFDerivWithin_univ]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (insert (x + y) s) (x + y)
⊢ s ∈ 𝓝[s] (x + y)

pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (insert (x + y) s) (x + y)
⊢ x + y ≠ x

Tactic:
]

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (insert (x + y) s) (x + y)
⊢ s ∈ 𝓝[s] (x + y)

case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (insert (x + y) s) (x + y)
⊢ x + y ≠ x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f univ x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f univ x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x

Tactic:
rw [← iteratedFDerivWithin_univ]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f univ x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ iteratedFDeriv 𝕜 n f x = iteratedFDeriv 𝕜 n f x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f univ x) m =
    ((iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f univ y) univ x) (init m)) (m (last n))

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f univ x) m =
    ((iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f univ y) univ x) (init m)) (m (last n))
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
z : E
hz : z ∈ Metric.eball x r
⊢ fderiv 𝕜 f z = fderiv 𝕜 f z

pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
z : E
hz : z ∈ Metric.eball x r
⊢ ↑‖z - x‖₊ < r

Tactic:
]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
z : E
hz : z ∈ Metric.eball x r
⊢ ↑‖z - x‖₊ < r
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ ((iteratedFDeriv 𝕜 n (fun y ↦ fderiv 𝕜 f y) x) (init m)) (m (last n)) =
    ((iteratedFDeriv 𝕜 n (fun y ↦ fderiv 𝕜 f y) x) (init m)) (m (last n))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ ‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 n (fun y ↦ fderiv 𝕜 f y) x‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
m : Fin 1 → E
⊢ (fderiv 𝕜 f x) (m 0) = (fderiv 𝕜 f x) (m 0)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
inst✝ : CompleteSpace F
h : ‖x‖ₑ < p.radius
⊢ HasFDerivAt p.sum (fderiv 𝕜 p.sum x) x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
inst✝ : CompleteSpace F
h : ‖x‖ₑ < p.radius
⊢ HasFDerivAt p.sum (fderiv 𝕜 p.sum x) x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
f : E → F
⊢ ‖iteratedFDerivWithin 𝕜 1 f univ x‖ = ‖fderivWithin 𝕜 f univ x‖

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
f : E → F
⊢ ‖iteratedFDerivWithin 𝕜 1 f univ x‖ = ‖fderivWithin 𝕜 f univ x‖
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a b : 𝕜
⊢ (((-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-b)) fun x ↦ 1) =
    ((-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-b)) fun x ↦ 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : 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
⊢ fderivWithin 𝕜 f (insert x s) z = fderivWithin 𝕜 f (insert x s) z

pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : 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‖₊ < r

pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : 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:
]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : 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‖₊ < r

𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : 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
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
hx : x ∈ s
this : insert x s = s
⊢ HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
hx : x ∈ s
this : insert x s = s
⊢ HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s

Tactic:
]

Goal state after:
case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOnNhd 𝕜 (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) s

Tactic:
]

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOnNhd 𝕜 (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a : 𝕜
ih' : iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s = fun a ↦ (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
g : 𝕜 → 𝕜 [×n]→L[𝕜] F := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) a
⊢ (-1) ^ (n + 1) • (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm (fderivWithin 𝕜 g (-s) (-a)) =
    (-1) ^ (n + 1) •
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ 𝕜) F).symm
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (-s)) (-s) (-a))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c a : 𝕜
this : (fun z ↦ f (c - z)) = fun z ↦ (fun w ↦ f (c + w)) (-z)
⊢ (((-1) ^ n • iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c + -a)) fun x ↦ 1) =
    ((-1) ^ n • iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) fun x ↦ 1

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c a : 𝕜
this : (fun z ↦ f (c - z)) = fun z ↦ (fun w ↦ f (c + w)) (-z)
⊢ (((-1) ^ n • iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c + -a)) fun x ↦ 1) =
    ((-1) ^ n • iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) fun x ↦ 1
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ ((n + 1).pred - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ ((n + 1 + 1).pred - x_1) •> f' <• f x ^ x_1 +
      f x ^ ((n + 1 + 1).pred - (n + 1)) •> f' <• f x ^ (n + 1)

Tactic:
]

Goal state after:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ ((n + 1).pred - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ ((n + 1 + 1).pred - x_1) •> f' <• f x ^ x_1 +
      f x ^ ((n + 1 + 1).pred - (n + 1)) •> f' <• f x ^ (n + 1)
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: case a
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x✝ : E
n x : ℕ
hx : x ≤ n
⊢ n + 1 - x = n + 1 - x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hf : HasDerivWithinAt f f' univ x
⊢ HasDerivWithinAt (c • f) (c x • f' + c' • f x) univ x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hf : HasDerivWithinAt f f' univ x
⊢ HasDerivWithinAt (c • f) (c x • f' + c' • f x) univ x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : 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‖₊ < 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' := UniformSpace.Completion.toComplₗᵢ.postcomp
⊢ HasSum (⇑b ∘ fun n ↦ (p.derivSeries n) fun x ↦ y) (b f')

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : 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‖₊ < 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' := UniformSpace.Completion.toComplₗᵢ.postcomp
⊢ HasSum (⇑b ∘ fun n ↦ (p.derivSeries n) fun x ↦ y) (b f')