-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F]
    (h : HasFPowerSeriesOnBall f p x r) :
    HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x 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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x 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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x 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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x 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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x 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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries x 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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
z : E
hz : z ∈ EMetric.ball x r
⊢ (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) z = fderiv 𝕜 f z

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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (fun z => 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

Result:
no goals

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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x 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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x 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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries x r

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

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∞
f : E → F
x : E
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (fun z => p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) x r