-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin
    (h : HasFPowerSeriesWithinAt f p s x) (hst : s ∈ 𝓝[t] x) :
    HasFPowerSeriesWithinAt f p t x

Proof state:
case intro.intro.intro
𝕜 : 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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : EMetric.ball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (r ⊓ r')
y : E
hy : x + y ∈ insert x t
h'y : y ∈ EMetric.ball 0 (r ⊓ r')
⊢ HasSum (fun n => (p n) fun x => y) (f (x + y))

Tactic:
apply Z.hasSum ?_ h'y

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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : EMetric.ball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (r ⊓ r')
y : E
hy : x + y ∈ insert x t
h'y : y ∈ EMetric.ball 0 (r ⊓ r')
⊢ x + y ∈ insert x s

Proof state:
case inr
𝕜 : 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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : EMetric.ball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (r ⊓ r')
y : E
h'y : y ∈ EMetric.ball 0 (r ⊓ r')
hy : x + y ∈ t
⊢ x + y ∈ insert x s

Tactic:
apply mem_insert_of_mem _ (hr' ?_)

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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : EMetric.ball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (r ⊓ r')
y : E
h'y : y ∈ EMetric.ball 0 (r ⊓ r')
hy : x + y ∈ t
⊢ x + y ∈ EMetric.ball x r' ∩ t

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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : EMetric.ball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (r ⊓ r')
y : E
hy : x + y ∈ insert x t
h'y : y ∈ EMetric.ball 0 (r ⊓ r')
⊢ x + y ∈ insert x s

Tactic:
simp only [mem_insert_iff, add_right_eq_self] at hy

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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : EMetric.ball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (r ⊓ r')
y : E
h'y : y ∈ EMetric.ball 0 (r ⊓ r')
hy : y = 0 ∨ x + y ∈ t
⊢ x + y ∈ insert x s

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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : EMetric.ball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (r ⊓ r')
y : E
h'y : y ∈ EMetric.ball 0 (r ⊓ r')
hy : x + y ∈ t
⊢ x + y ∈ EMetric.ball x r' ∩ t

Tactic:
simp only [EMetric.mem_ball, edist_eq_enorm_sub, sub_zero, lt_min_iff, mem_inter_iff,
  add_sub_cancel_left, hy, and_true] at h'y ⊢

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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : EMetric.ball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (r ⊓ r')
y : E
hy : x + y ∈ t
h'y : ‖y‖ₑ < r ∧ ‖y‖ₑ < r'
⊢ ‖y‖ₑ < r'

Proof state:
case intro
𝕜 : 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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f p t x

Tactic:
rcases EMetric.mem_nhdsWithin_iff.1 hst with ⟨r', r'_pos, hr'⟩

Result:
case intro.intro.intro
𝕜 : 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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : EMetric.ball x r' ∩ t ⊆ s
⊢ HasFPowerSeriesWithinAt f p t x