awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hr : 0 < r
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e r

Tactic:
HasFPowerSeriesWithinOnBall.pi hf hr

Premises used: HasFPowerSeriesWithinOnBall.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hr : 0 < r
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e r

Tactic:
exact HasFPowerSeriesWithinOnBall.pi hf hr

Premises used: HasFPowerSeriesWithinOnBall.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hr : 0 < r
simp_rw :
  HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e r ↔
    ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) e r ↔
    ∀ (i : ι), HasFPowerSeriesOnBall (f i) (p i) e r

Tactic:
simp_rw [← hasFPowerSeriesWithinOnBall_univ]

Premises used: hasFPowerSeriesWithinOnBall_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hr : 0 < r
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e r ↔
    ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r

Tactic:
hasFPowerSeriesWithinOnBall_pi_iff hr

Premises used: hasFPowerSeriesWithinOnBall_pi_iff
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hr : 0 < r
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e r ↔
    ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r

Tactic:
exact hasFPowerSeriesWithinOnBall_pi_iff hr

Premises used: hasFPowerSeriesWithinOnBall_pi_iff
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
⊢ ∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r

Tactic:
have : ∀ᶠ r in 𝓝[>] 0, ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r :=
    eventually_all.mpr (fun i ↦ (hf i).eventually)
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 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
obtain :
  ∀ (r : ℝ≥0∞) (hr : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r) (r_pos : 0 < r),
    HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) s e
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) s e

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

Premises used: Filter.Eventually.and, Filter.Eventually.exists, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 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 (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) s e

Tactic:
⟨r, HasFPowerSeriesWithinOnBall.pi hr r_pos⟩

Premises used: HasFPowerSeriesWithinAt, Exists.intro, HasFPowerSeriesWithinOnBall.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 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 (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) s e

Tactic:
exact ⟨r, HasFPowerSeriesWithinOnBall.pi hr r_pos⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) s e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
⟨fun h i ↦ ?_, fun h ↦ .pi h⟩

Premises used: HasFPowerSeriesWithinAt.pi, Iff.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
refine :
  ∀
    (h :
      HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
        (FormalMultilinearSeries.pi (F := Fm) p) s e)
    (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) s e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h :
  HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) s e
i : ι
obtain :
  ∀ (r : ℝ≥0∞)
    (hr :
      HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
        (FormalMultilinearSeries.pi (F := Fm) p) s e r),
    HasFPowerSeriesWithinAt (f i) (p i) s e
⊢ HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
obtain ⟨r, hr⟩ := h
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r : ℝ≥0∞
hr :
  HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) s e r
⊢ HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
⟨r, (hasFPowerSeriesWithinOnBall_pi_iff hr.r_pos).1 hr i⟩

Premises used: HasFPowerSeriesWithinAt, hasFPowerSeriesWithinOnBall_pi_iff, Exists.intro, Iff.mp, HasFPowerSeriesWithinOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r : ℝ≥0∞
hr :
  HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) s e r
⊢ HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
exact ⟨r, (hasFPowerSeriesWithinOnBall_pi_iff hr.r_pos).1 hr i⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e
simp_rw :
  ∀ (hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e),
    HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) e

Tactic:
simp_rw [← hasFPowerSeriesWithinAt_univ] at hf ⊢

Premises used: hasFPowerSeriesWithinAt_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e

Tactic:
HasFPowerSeriesWithinAt.pi hf

Premises used: HasFPowerSeriesWithinAt.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e

Tactic:
exact HasFPowerSeriesWithinAt.pi hf

Premises used: HasFPowerSeriesWithinAt.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
simp_rw :
  HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) e ↔
    ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e

Tactic:
simp_rw [← hasFPowerSeriesWithinAt_univ]

Premises used: hasFPowerSeriesWithinAt_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e

Tactic:
hasFPowerSeriesWithinAt_pi_iff

Premises used: hasFPowerSeriesWithinAt_pi_iff
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e

Tactic:
exact hasFPowerSeriesWithinAt_pi_iff

Premises used: hasFPowerSeriesWithinAt_pi_iff
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
hf : ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e
choose :
  ∀ (p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i))
    (hp : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e),
    AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e

Tactic:
choose p hp using hf
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hp : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e

Tactic:
⟨FormalMultilinearSeries.pi p, HasFPowerSeriesWithinAt.pi hp⟩

Premises used: AnalyticWithinAt, HasFPowerSeriesWithinAt.pi, FormalMultilinearSeries.pi, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hp : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e

Tactic:
exact ⟨FormalMultilinearSeries.pi p, HasFPowerSeriesWithinAt.pi hp⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e ↔
    ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e

Tactic:
⟨fun h i ↦ ?_, fun h ↦ .pi h⟩

Premises used: AnalyticWithinAt.pi, Iff.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
refine :
  ∀ (h : AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e) (i : ι),
    AnalyticWithinAt 𝕜 (f i) s e
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e ↔
    ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e

Tactic:
refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
h : AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e
i : ι
⊢ AnalyticWithinAt 𝕜 (f i) s e

Tactic:
((ContinuousLinearMap.proj (R := 𝕜) i).analyticAt _).comp_analyticWithinAt h

Premises used: AnalyticAt.comp_analyticWithinAt, ContinuousLinearMap.analyticAt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
h : AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e
i : ι
⊢ AnalyticWithinAt 𝕜 (f i) s e

Tactic:
exact ((ContinuousLinearMap.proj (R := 𝕜) i).analyticAt _).comp_analyticWithinAt h

Premises used: AnalyticAt.comp_analyticWithinAt, ContinuousLinearMap.analyticAt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
hf : ∀ (i : ι), AnalyticAt 𝕜 (f i) e
simp_rw :
  ∀ (hf : ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e),
    AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) Set.univ e
⊢ AnalyticAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) e

Tactic:
simp_rw [← analyticWithinAt_univ] at hf ⊢

Premises used: analyticWithinAt_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
hf : ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) Set.univ e

Tactic:
AnalyticWithinAt.pi hf

Premises used: AnalyticWithinAt.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
hf : ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) Set.univ e

Tactic:
exact AnalyticWithinAt.pi hf

Premises used: AnalyticWithinAt.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
simp_rw :
  AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) Set.univ e ↔
    ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e
⊢ AnalyticAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) e ↔ ∀ (i : ι), AnalyticAt 𝕜 (f i) e

Tactic:
simp_rw [← analyticWithinAt_univ]

Premises used: analyticWithinAt_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) Set.univ e ↔
    ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e

Tactic:
analyticWithinAt_pi_iff

Premises used: analyticWithinAt_pi_iff