-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesWithinAt.pi
    (hf : ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e) :
    HasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
this : ∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e

Tactic:
obtain ⟨r, hr, r_pos⟩ := (this.and self_mem_nhdsWithin).exists

Result:
case intro.intro
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
this : ∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
r : ℝ≥0∞
hr : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
r_pos : 0 < r
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e

Tactic:
have : ∀ᶠ r in 𝓝[>] 0, ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r :=
  eventually_all.mpr (fun i ↦ (hf i).eventually)

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
this : ∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e

Proof state:
case intro.intro
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
this : ∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
r : ℝ≥0∞
hr : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
r_pos : 0 < r
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e

Tactic:
exact ⟨r, HasFPowerSeriesWithinOnBall.pi hr r_pos⟩

Result:
no goals