-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem HasFiniteFPowerSeriesOnBall.fderiv
    (h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r) :
    HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r

Proof state:
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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ EMetric.ball x r
⊢ (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1) = fderiv 𝕜 f z

Tactic:
rw [← h.fderiv_eq, add_sub_cancel]

Result:
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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ EMetric.ball x r
⊢ ↑‖z - x‖₊ < r

Proof state:
case refine_1
𝕜 : 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (fun z => p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) x n r

Tactic:
simpa using
  ((p.hasFiniteFPowerSeriesOnBall_changeOrigin 1 h.finite).mono h.r_pos le_top).comp_sub x

Result:
no goals

Proof state:
case refine_1
𝕜 : 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries
    x n r

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

Result:
case refine_1
𝕜 : 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (fun z => p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) x n r

Proof state:
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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ EMetric.ball x r
⊢ (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) z = fderiv 𝕜 f z

Tactic:
dsimp only

Result:
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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ EMetric.ball x r
⊢ (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1) = fderiv 𝕜 f z

Proof state:
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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ EMetric.ball x r
⊢ ↑‖z - x‖₊ < r

Tactic:
simpa only [edist_eq_enorm_sub, EMetric.mem_ball] using hz

Result:
no goals

Proof state:
𝕜 : 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r

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

Result:
case refine_1
𝕜 : 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries
    x n r

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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ EMetric.ball x r
⊢ (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) z = fderiv 𝕜 f z