-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinOnBall.hasSum_sub (hf : HasFPowerSeriesWithinOnBall f p s x r) {y : E}
    (hy : y ∈ (insert x s) ∩ EMetric.ball x r) :
    HasSum (fun n : ℕ => p n fun _ => y - x) (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
this✝ : y - x ∈ EMetric.ball 0 r
this : HasSum (fun n => (p n) fun x_1 => y - x) (f (x + (y - x)))
⊢ HasSum (fun n => (p n) fun x_1 => y - x) (f y)

Tactic:
simpa only [add_sub_cancel]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
this : y - x ∈ EMetric.ball 0 r
⊢ x + (y - x) ∈ insert x s

Tactic:
simpa only [add_sub_cancel] using hy.1

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
⊢ y - x ∈ EMetric.ball 0 r

Tactic:
simpa [edist_eq_enorm_sub] using hy.2

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
this : y - x ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun x_1 => y - x) (f y)

Tactic:
have := hf.hasSum (by simpa only [add_sub_cancel] using hy.1) this

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
this✝ : y - x ∈ EMetric.ball 0 r
this : HasSum (fun n => (p n) fun x_1 => y - x) (f (x + (y - x)))
⊢ HasSum (fun n => (p n) fun x_1 => y - x) (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
⊢ HasSum (fun n => (p n) fun x_1 => y - x) (f y)

Tactic:
have : y - x ∈ EMetric.ball (0 : E) r := by simpa [edist_eq_enorm_sub] using hy.2

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ EMetric.ball x r
this : y - x ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun x_1 => y - x) (f y)