awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
⊢ (↑r' : ℝ≥0∞) ≤ (p i).radius
have obtain : ∀ (C : ℝ) (hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C), (↑r' : ℝ≥0∞) ≤ (p i).radius
Tactic: obtain ⟨C, -, hC⟩ : ∃ C > 0, ∀ n, ‖pi p n‖ * ↑r' ^ n ≤ C := norm_mul_pow_le_of_lt_radius _ hr'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
⊢ (↑r' : ℝ≥0∞) ≤ (p i).radius
have apply : ∀ (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C
Tactic: apply le_radius_of_bound _ C (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C
have apply : ‖p i n‖ * (↑r' : ℝ) ^ n ≤ ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n
Tactic: apply le_trans _ (hC n)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p i n‖ * (↑r' : ℝ) ^ n ≤ ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n
have hbc : ‖p i n‖ ≤ ‖pi (F := Fm) p n‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p i n‖ ≤ ‖pi (F := Fm) p n‖
have hbc : ‖p i n‖ ≤
  norm (E := (i' : ι) → ContinuousMultilinearMap.{u_2, 0, u_3, u_10} 𝕜 (fun (i : Fin n) ↦ E) (Fm i')) fun (i : ι) ↦
    p i n
Tactic: rw [pi, ContinuousMultilinearMap.opNorm_pi]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
⊢ r ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
have apply : ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < r), (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
Tactic: apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
⊢ (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
have I : ∀ (i : ι), ∃ C > 0, ∀ (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C
Tactic: have I i : ∃ C > 0, ∀ n, ‖p i n‖ * (r' : ℝ) ^ n ≤ C :=
    norm_mul_pow_le_of_lt_radius _ (hr'.trans_le (h i))
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
I : ∀ (i : ι), ∃ C > 0, ∀ (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C
⊢ (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
have choose : ∀ (C : (i : ι) → ℝ) (C_pos : ∀ (i : ι), C i > 0) (hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i),
  (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
Tactic: choose C C_pos hC using I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
⊢ (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
have obtain : ∀ (D : ℝ) (D_nonneg : D ≥ 0) (hD : ∀ (i : ι), C i ≤ D),
  (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
Tactic: obtain ⟨D, D_nonneg, hD⟩ : ∃ D ≥ 0, ∀ i, C i ≤ D :=
    ⟨∑ i, C i, Finset.sum_nonneg (fun i _ ↦ (C_pos i).le),
      fun i ↦ Finset.single_le_sum (fun j _ ↦ (C_pos j).le) (Finset.mem_univ _)⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
⊢ (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
have apply : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D
Tactic: apply le_radius_of_bound _ D (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
⊢ ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D
have inl : ∀ (hr' : (↑r' : ℝ) ^ n ≤ 0), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D
Tactic: rcases le_or_gt ((r' : ℝ) ^ n) 0 with hr' | hr'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
inl : ∀ (hr' : (↑r' : ℝ) ^ n ≤ 0), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D
⊢ ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D
have inr : ∀ (hr' : 0 < (↑r' : ℝ) ^ n), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D
Tactic: rcases le_or_gt ((r' : ℝ) ^ n) 0 with hr' | hr'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr'_1 : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : 0 < (↑r' : ℝ) ^ n
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) ((i : ι) → Fm i))
        (ContinuousMultilinearMap.pi (M₁ := fun (i : Fin n) ↦ E) (M' := Fm) fun (i : ι) ↦ p i n :
          ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) ((i : ι) → Fm i)) *
      (↑r' : ℝ) ^ n ≤
    D
have inr : ∀ (i : ι), ‖p i n‖ ≤ D / (↑r' : ℝ) ^ n
Tactic: rw [← le_div_iff₀ hr', ContinuousMultilinearMap.opNorm_pi,
      pi_norm_le_iff_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
⊢ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p) = ⨅ (i : ι), (p i).radius
have refine : ⨅ (i : ι), (p i).radius ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
Tactic: refine le_antisymm (by simp [radius_pi_le]) ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
⊢ ⨅ (i : ι), (p i).radius ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
have apply : ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < ⨅ (i : ι), (p i).radius),
  (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
Tactic: apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
⊢ r ≤ FormalMultilinearSeries.radius (𝕜 := 𝕜) (E := E) (F := (x : ι) → Fm x) (FormalMultilinearSeries.pi (F := Fm) p)
have apply : ∀ (i : ι), r ≤ (p i).radius
Tactic: apply FormalMultilinearSeries.le_radius_pi (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
hf : ∀ (i : ι), HasFPowerSeriesOnBall (f i) (p i) e r
hr : 0 < r
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) e r
have simp_rw : ∀ (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: simp_rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ 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
have 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
Tactic: simp_rw [← hasFPowerSeriesWithinOnBall_univ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
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
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) s e
have this : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) s e
have 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
Tactic: obtain ⟨r, hr, r_pos⟩ := (this.and self_mem_nhdsWithin).exists
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
have 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
Tactic: refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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 : ι
⊢ HasFPowerSeriesWithinAt (f i) (p i) s e
have 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
Tactic: obtain ⟨r, hr⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) e
have 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
Tactic: simp_rw [← hasFPowerSeriesWithinAt_univ] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
⊢ 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
have 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
Tactic: simp_rw [← hasFPowerSeriesWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ AnalyticWithinAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) s e
have 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
Tactic: choose p hp using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
have refine : ∀ (h : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ AnalyticAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) e
have 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
Tactic: simp_rw [← analyticWithinAt_univ] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ AnalyticAt 𝕜 (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x) e ↔ ∀ (i : ι), AnalyticAt 𝕜 (f i) e
have 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
Tactic: simp_rw [← analyticWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
⊢ AnalyticWithinAt 𝕜 (HPow.hPow (β := ℕ) f 0) s z
have zero : AnalyticWithinAt.{u_2, u_3, u_7} 𝕜 (F := A) 1 s z
Tactic: simp only [pow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (f ^ m) s z
⊢ AnalyticWithinAt 𝕜 (f ^ (m + 1)) s z
have succ : AnalyticWithinAt 𝕜 (f ^ m * f) s z
Tactic: simp only [pow_succ]