-- Mathlib/Analysis/Analytic/Within.lean
/-- `f` has power series `p` at `x` iff some local extension of `f` has that series -/
lemma hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpace F] {f : E → F}
    {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ℝ≥0∞} :
    HasFPowerSeriesWithinOnBall f p s x r ↔
      ∃ g, EqOn f g (insert x s ∩ EMetric.ball x r) ∧
        HasFPowerSeriesOnBall g p x r

Proof state:
case mp.refine_1.refine_2.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n => (p n) fun x_1 => y - x) (p.sum (y - x))
⊢ x + (y - x) ∈ insert x s

Tactic:
simpa only [add_sub_cancel]

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ ∃ g, EqOn f g (insert x s ∩ EMetric.ball x r) ∧ HasFPowerSeriesOnBall g p x r

Tactic:
refine ⟨fun y ↦ p.sum (y - x), ?_, ?_⟩

Result:
case mp.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ EqOn f (fun y => p.sum (y - x)) (insert x s ∩ EMetric.ball x r)

case mp.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesOnBall (fun y => p.sum (y - x)) p x r

Proof state:
case mp.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : y ∈ EMetric.ball x r
⊢ f y = (fun y => p.sum (y - x)) y

Tactic:
simp only [EMetric.mem_ball, edist_eq_enorm_sub] at yb

Result:
case mp.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
⊢ f y = (fun y => p.sum (y - x)) y

Proof state:
case mp.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
⊢ f y = (fun y => p.sum (y - x)) y

Tactic:
have e0 := p.hasSum (x := y - x) ?_

Result:
case mp.refine_1.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n => (p n) fun x_1 => y - x) (p.sum (y - x))
⊢ f y = (fun y => p.sum (y - x)) y

case mp.refine_1.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
⊢ y - x ∈ EMetric.ball 0 p.radius