awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
n : ℕ
hn : n ≥ 1
rw :
  (f x + ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    ∑ a ∈ Finset.range n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
⊢ (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    (∑ a ∈ Finset.range n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) - f x
have rw₁ : (f x + ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
  ∑ a ∈ Finset.Ico 0 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
Tactic: rw [eq_sub_iff_add_eq', Finset.range_eq_Ico, ← Hf.coeff_zero fun _i => y,
        Finset.sum_eq_sum_Ico_succ_bot hn]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
n : ℕ
hn : n ≥ 1
rw :
  (f x + ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    ∑ a ∈ Finset.range n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
rw₁ :
  (f x + ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    ∑ a ∈ Finset.Ico 0 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
⊢ (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    (∑ a ∈ Finset.range n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) - f x
have rw₂ : HAdd.hAdd (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (_i : Fin 0) ↦ y : F)
    (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y : F) =
  ∑ a ∈ Finset.Ico 0 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
Tactic: rw [eq_sub_iff_add_eq', Finset.range_eq_Ico, ← Hf.coeff_zero fun _i => y,
        Finset.sum_eq_sum_Ico_succ_bot hn]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
n : ℕ
hn : n ≥ 1
rw :
  (f x + ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    ∑ a ∈ Finset.range n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
rw₁ :
  (f x + ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    ∑ a ∈ Finset.Ico 0 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
rw₂ :
  HAdd.hAdd (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (_i : Fin 0) ↦ y : F)
      (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y : F) =
    ∑ a ∈ Finset.Ico 0 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
⊢ (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    (∑ a ∈ Finset.range n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) - f x
have rw₃ : HAdd.hAdd (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (_i : Fin 0) ↦ y : F)
    (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y : F) =
  HAdd.hAdd (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (_b : Fin 0) ↦ y : F)
    (∑ k ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) n, (p k : (a : (i : Fin k) → E) → F) fun (_b : Fin k) ↦ y : F)
Tactic: rw [eq_sub_iff_add_eq', Finset.range_eq_Ico, ← Hf.coeff_zero fun _i => y,
        Finset.sum_eq_sum_Ico_succ_bot hn]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
⊢ Tendsto (fun (x : ℕ) ↦ ∑ a ∈ Finset.Ico 1 x, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y) atTop
    (𝓝 (f (x + y) - f x))
have L : ∀ᶠ (n : ℕ) in atTop,
  (∑ a ∈ Finset.range n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) - f x =
    ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
Tactic: have L : ∀ᶠ n in atTop, (∑ a ∈ Finset.range n, p a fun _b ↦ y) - f x
        = ∑ a ∈ Finset.Ico 1 n, p a fun _b ↦ y := by
      rw [eventually_atTop]
      refine ⟨1, fun n hn => ?_⟩
      symm
      rw [eq_sub_iff_add_eq', Finset.range_eq_Ico, ← Hf.coeff_zero fun _i => y,
        Finset.sum_eq_sum_Ico_succ_bot hn]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
L :
  ∀ᶠ (n : ℕ) in atTop,
    (∑ a ∈ Finset.range n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) - f x =
      ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
⊢ Tendsto (fun (x : ℕ) ↦ ∑ a ∈ Finset.Ico 1 x, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y) atTop
    (𝓝 (f (x + y) - f x))
have this : Tendsto (fun (n : ℕ) ↦ (∑ a ∈ Finset.range n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) - f x) atTop
  (𝓝 (f (x + y) - f x))
Tactic: have :
      Tendsto (fun n => (∑ a ∈ Finset.range n, p a fun _b => y) - f x) atTop
        (𝓝 (f (x + y) - f x)) :=
      (Hf.hasSum h'y y_mem).tendsto_sum_nat.sub tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y) ((g ∘ f) (x + y))
have A : Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
  (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
Tactic: have A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, p a fun _ ↦ y))
      atTop (atTop ×ˢ 𝓝 (f (x + y) - f x)) := by
    apply Tendsto.prodMk tendsto_id
    have L : ∀ᶠ n in atTop, (∑ a ∈ Finset.range n, p a fun _b ↦ y) - f x
        = ∑ a ∈ Finset.Ico 1 n, p a fun _b ↦ y := by
      rw [eventually_atTop]
      refine ⟨1, fun n hn => ?_⟩
      symm
      rw [eq_sub_iff_add_eq', Finset.range_eq_Ico, ← Hf.coeff_zero fun _i => y,
        Finset.sum_eq_sum_Ico_succ_bot hn]
    have :
      Tendsto (fun n => (∑ a ∈ Finset.range n, p a fun _b => y) - f x) atTop
        (𝓝 (f (x + y) - f x)) :=
      (Hf.hasSum h'y y_mem).tendsto_sum_nat.sub tendsto_const_nhds
    exact Tendsto.congr' L this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
⊢ Tendsto (fun (z : ℕ × F) ↦ q.partialSum z.1 z.2) (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
    (𝓝 (g (f x + (f (x + y) - f x))))
have hy₁ : Membership.mem (γ := Set F) (Metric.eball 0 rg) (f (x + y) - f x)
Tactic: apply Hg.tendsto_partialSum_prod (y := f (x + y) - f x)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
hy₁ : Membership.mem (γ := Set F) (Metric.eball 0 rg) (f (x + y) - f x)
⊢ Tendsto (fun (z : ℕ × F) ↦ q.partialSum z.1 z.2) (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
    (𝓝 (g (f x + (f (x + y) - f x))))
have h'y₁ : f x + (f (x + y) - f x) ∈ insert (f x) t
Tactic: apply Hg.tendsto_partialSum_prod (y := f (x + y) - f x)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
⊢ Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
have this : Tendsto (fun (z : ℕ × F) ↦ q.partialSum z.1 z.2) (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
  (𝓝 (g (f x + (f (x + y) - f x))))
Tactic: have : Tendsto (fun (z : ℕ × F) ↦ q.partialSum z.1 z.2)
        (atTop ×ˢ 𝓝 (f (x + y) - f x)) (𝓝 (g (f x + (f (x + y) - f x)))) := by
      apply Hg.tendsto_partialSum_prod (y := f (x + y) - f x)
      · simpa [edist_eq_enorm_sub] using fy_mem.2
      · simpa using fy_mem.1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y) ((g ∘ f) (x + y))
have B : Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
  atTop (𝓝 (g (f (x + y))))
Tactic: have B : Tendsto (fun n => q.partialSum n (∑ a ∈ Finset.Ico 1 n, p a fun _b ↦ y)) atTop
      (𝓝 (g (f (x + y)))) := by
    -- we use the fact that the partial sums of `q` converge to `g (f (x + y))`, uniformly on a
    -- neighborhood of `f (x + y)`.
    have : Tendsto (fun (z : ℕ × F) ↦ q.partialSum z.1 z.2)
        (atTop ×ˢ 𝓝 (f (x + y) - f x)) (𝓝 (g (f x + (f (x + y) - f x)))) := by
      apply Hg.tendsto_partialSum_prod (y := f (x + y) - f x)
      · simpa [edist_eq_enorm_sub] using fy_mem.2
      · simpa using fy_mem.1
    simpa using this.comp A
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y) ((g ∘ f) (x + y))
have C : Tendsto
  (fun (n : ℕ) ↦
    ∑ i ∈ compPartialSumTarget 0 n n,
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
  atTop (𝓝 (g (f (x + y))))
Tactic: have C :
    Tendsto
      (fun n => ∑ i ∈ compPartialSumTarget 0 n n, q.compAlongComposition p i.2 fun _j => y)
      atTop (𝓝 (g (f (x + y)))) := by
    simpa [comp_partialSum] using B