awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
empty :
  ∀ (h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ ∅, f n z) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) s c
have insert : ∀ (a : α) (B : Finset α) (aB : a ∉ B)
  (hB :
    ∀ (h : ∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c),
      AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ B, f n z) s c)
  (h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c),
  AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ insert a B, f n z) s c
Tactic: induction N using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.prod_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) s c
have empty : ∀ (h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c),
  AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ ∅, f n z) s c
Tactic: classical
  induction N using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.prod_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
empty :
  ∀ (h : ∀ (n : α), Membership.mem (γ := Finset α) ∅ n → AnalyticWithinAt 𝕜 (f n) s c),
    AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ ∅, f n z) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) s c
have insert : ∀ (a : α) (B : Finset α) (aB : a ∉ B)
  (hB :
    ∀ (h : ∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c),
      AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ B, f n z) s c)
  (h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c),
  AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ insert a B, f n z) s c
Tactic: classical
  induction N using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.prod_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (∏ n ∈ N, f n) s c
have h₁ : ∀ (x : E), Eq.{u_9 + 1} (α := A) ((∏ n ∈ N, f n) x) (∏ n ∈ N, f n x)
Tactic: convert! N.analyticWithinAt_fun_prod h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
⊢ AnalyticAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) c
have simp_rw : ∀ (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) Set.univ c),
  AnalyticWithinAt.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) Set.univ c
Tactic: simp_rw [← analyticWithinAt_univ] at 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
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ n ∈ N, f n) c
have h₁ : ∀ (x : E), Eq.{u_10 + 1} (α := A) ((∏ n ∈ N, f n) x) (∏ n ∈ N, f n x)
Tactic: convert! N.analyticAt_fun_prod 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
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c
have pos : ∀ (hf : (Function.mulSupport f).Finite), AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c
Tactic: by_cases hf : (Function.mulSupport f).Finite
-- 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
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
pos : ∀ (hf : (Function.mulSupport f).Finite), AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c
have neg : ∀ (hf : ¬(Function.mulSupport f).Finite), AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c
Tactic: by_cases hf : (Function.mulSupport f).Finite
-- 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
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
hf : ¬(Function.mulSupport f).Finite
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c
have neg : AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) 1 c
Tactic: rw [finprod_of_infinite_mulSupport hf]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
⊢ r ≤ (pf.unshift z).radius
have rw : r ≤ pf.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
Tactic: rw [FormalMultilinearSeries.radius_unshift]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (pf.unshift z n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (HAdd.hAdd (β := F) z ((f (x + y) : (a : E) → F) (x + y - x) : F))
have h : HasSum.{u_4, 0} (α := F)
  (fun (n : ℕ) ↦ ((pf.unshift z (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F))
  ((f (x + y) : (a : E) → F) (x + y - x) : F)
Tactic: apply HasSum.zero_add
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦ ((pf.unshift z (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F))
    ((f (x + y) : (a : E) → F) (x + y - x) : F)
have h : HasSum.{u_4, 0} (α := F)
  (fun (n : ℕ) ↦
    ((((pf n : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F))
  ((f (x + y) : (a : E) → F) y : F)
Tactic: simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one,
      continuousMultilinearCurryRightEquiv_symm_apply', add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
⊢ r ≤ (pf.unshift z).radius
have rw : r ≤ pf.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
Tactic: rw [FormalMultilinearSeries.radius_unshift]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (pf.unshift z n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (HAdd.hAdd (β := F) z ((f (x + y) : (a : E) → F) (x + y - x) : F))
have h : HasSum.{u_4, 0} (α := F)
  (fun (n : ℕ) ↦ ((pf.unshift z (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F))
  ((f (x + y) : (a : E) → F) (x + y - x) : F)
Tactic: apply HasSum.zero_add
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦ ((pf.unshift z (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F))
    ((f (x + y) : (a : E) → F) (x + y - x) : F)
have h : HasSum.{u_4, 0} (α := F)
  (fun (n : ℕ) ↦
    ((((pf n : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F))
  ((f (x + y) : (a : E) → F) y : F)
Tactic: simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one,
      continuousMultilinearCurryRightEquiv_symm_apply', add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
⊢ r / ‖u‖ₑ ≤ pf.radius / ‖u‖ₑ
have hab : r ≤ pf.radius
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
⊢ r / ‖u‖ₑ ≤ FormalMultilinearSeries.radius (pf.compContinuousLinearMap u)
have _ : r / ‖u‖ₑ ≤ pf.radius / ‖u‖ₑ
Tactic: calc
      _ ≤ pf.radius / ‖u‖ₑ := by
        gcongr
        exact hf.r_le
      _ ≤ _ := pf.div_le_radius_compContinuousLinearMap _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
⊢ 0 < r / ‖u‖ₑ
have simp : ¬r = 0
Tactic: simp only [ENNReal.div_pos_iff, ne_eq, enorm_ne_top, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
⊢ HasSum (fun (n : ℕ) ↦ (pf.compContinuousLinearMap u n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y)
    ((f ∘ (⇑u : (a : E) → F)) (x + y))
have h : (f ∘ (⇑u : (a : E) → F)) (x + y) =
  f (HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F))
Tactic: convert! hf.hasSum _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
h :
  (f ∘ (⇑u : (a : E) → F)) (x + y) =
    f (HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F))
⊢ HasSum (fun (n : ℕ) ↦ (pf.compContinuousLinearMap u n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y)
    ((f ∘ (⇑u : (a : E) → F)) (x + y))
have convert_2 : HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈
  insert (α := F) ((u : (a : E) → F) x : F) s
Tactic: convert! hf.hasSum _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
h :
  (f ∘ (⇑u : (a : E) → F)) (x + y) =
    f (HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F))
convert_2 :
  HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈
    insert (α := F) ((u : (a : E) → F) x : F) s
⊢ HasSum (fun (n : ℕ) ↦ (pf.compContinuousLinearMap u n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y)
    ((f ∘ (⇑u : (a : E) → F)) (x + y))
have convert_3 : Membership.mem.{u_4, u_4} (α := F) (γ := Set F) (Metric.eball 0 r) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F)
Tactic: convert! hf.hasSum _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
⊢ HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈
    insert (α := F) ((u : (a : E) → F) x : F) s
have convert_2 : ∀ (hy1 : y = 0 ∨ HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) ((u : (a : E) → F) y : F) ∈ s),
  Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
    HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s
Tactic: simp only [Set.mem_insert_iff, add_eq_left, Set.mem_preimage, map_add] at hy1 ⊢
Cleared hypotheses: hy1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
hy1 : y = 0 ∨ HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) ((u : (a : E) → F) y : F) ∈ s
⊢ Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
    HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s
have convert_2 : ∀ (hy1 : y = 0),
  Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
    HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s
Tactic: rcases hy1 with (hy1 | hy1)
Cleared hypotheses: hy1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
hy1 : y = 0 ∨ HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) ((u : (a : E) → F) y : F) ∈ s
convert_2 :
  ∀ (hy1 : y = 0),
    Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
      HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s
⊢ Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
    HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s
have convert_2₁ : ∀ (hy1 : HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) ((u : (a : E) → F) y : F) ∈ s),
  Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
    HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s
Tactic: rcases hy1 with (hy1 | hy1)
Cleared hypotheses: hy1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
⊢ Membership.mem.{u_4, u_4} (α := F) (γ := Set F) (Metric.eball 0 r) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F)
have convert_3 : ∀ (hy2 : ‖y‖ₑ < r / ‖u‖ₑ), enorm.{u_4} (E := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) < r
Tactic: simp only [Metric.eball, edist_zero_right, Set.mem_setOf_eq] at hy2 ⊢
Cleared hypotheses: hy2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf ((u : (a : E) → F) x) r
⊢ HasFPowerSeriesOnBall (f ∘ (⇑u : (a : E) → F)) (pf.compContinuousLinearMap u) x (r / ‖u‖ₑ)
have rw : ∀ (hf : HasFPowerSeriesWithinOnBall f pf Set.univ ((u : (a : E) → F) x) r),
  HasFPowerSeriesWithinOnBall (f ∘ (⇑u : (a : E) → F)) (pf.compContinuousLinearMap u) Set.univ x (r / ‖u‖ₑ)
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ radius.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) (F := F) 0 = ∞
have rw : radius.{u_1, u_2, u_3} (F := F) (constFormalMultilinearSeries 𝕜 E 0) = ∞
Tactic: rw [← constFormalMultilinearSeries_zero]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
      IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x
have this : (∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
      IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
  ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
Tactic: have := (TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 4