awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
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)
obtain :
  ∀ (δ : ℝ≥0∞) (δpos : 0 < δ)
    (hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg),
    HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x

Tactic:
obtain ⟨δ, δpos, hδ⟩ :
    ∃ δ : ℝ≥0∞, 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ
      → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg := by
    have : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] (f x) := by
      apply inter_mem_nhdsWithin
      exact Metric.eball_mem_nhds _ Hg.r_pos
    have := Hf.analyticWithinAt.continuousWithinAt_insert.tendsto_nhdsWithin (hs.insert x) this
    rcases EMetric.mem_nhdsWithin_iff.1 this with ⟨δ, δpos, Hδ⟩
    exact ⟨δ, δpos, fun {z} hz => Hδ (by rwa [Set.inter_comm])⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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 δ
⊢ 0 < min rf' (↑r : ℝ≥0∞)

Tactic:
simp only [rf', r_pos, Hf.r_pos, δpos, lt_min_iff, ENNReal.coe_pos, and_self_iff]

Premises used: ENNReal.coe_pos, HasFPowerSeriesWithinOnBall.r_pos, and_self_iff, lt_min_iff
-- Module: Mathlib.Analysis.Analytic.Composition
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 δ
⊢ 0 < min rf' (↑r : ℝ≥0∞)

Tactic:
have min_pos : 0 < min rf' r := by
    simp only [rf', r_pos, Hf.r_pos, δpos, lt_min_iff, ENNReal.coe_pos, and_self_iff]
-- Module: Mathlib.Analysis.Analytic.Composition
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∞)
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x

Tactic:
⟨min rf' r, ?_⟩

Premises used: ENNReal.ofNNReal, HasFPowerSeriesWithinAt, Exists.intro, Min.min
-- Module: Mathlib.Analysis.Analytic.Composition
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∞)
refine : HasFPowerSeriesWithinOnBall (g ∘ f) (q.comp p) s x (min rf' (↑r : ℝ≥0∞))
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x

Tactic:
refine ⟨min rf' r, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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∞)
⊢ HasFPowerSeriesWithinOnBall (g ∘ f) (q.comp p) s x (min rf' (↑r : ℝ≥0∞))

Tactic:
⟨le_trans (min_le_right rf' r) (FormalMultilinearSeries.le_comp_radius_of_summable q p r hr),
      min_pos, fun {y} h'y hy ↦ ?_⟩

Premises used: ENNReal.ofNNReal, HasFPowerSeriesWithinOnBall.mk, FormalMultilinearSeries.le_comp_radius_of_summable, min_le_right, le_trans
-- Module: Mathlib.Analysis.Analytic.Composition
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∞)
rf'₁ :
  ∀ {y : E} (h'y : x + y ∈ insert x s) (hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y),
    HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y) ((g ∘ f) (x + y))
⊢ HasFPowerSeriesWithinOnBall (g ∘ f) (q.comp p) s x (min rf' (↑r : ℝ≥0∞))

Tactic:
refine
    ⟨le_trans (min_le_right rf' r) (FormalMultilinearSeries.le_comp_radius_of_summable q p r hr),
      min_pos, fun {y} h'y hy ↦ ?_⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ Membership.mem (γ := Set E) (Metric.eball 0 rf) y

Tactic:
have y_mem : y ∈ Metric.eball (0 : E) rf :=
    (Metric.eball_subset_eball (le_trans (min_le_left _ _) (min_le_left _ _))) hy
-- Module: Mathlib.Analysis.Analytic.Composition
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
a : x + y ∈ insert x s ∩ Metric.eball x δ
⊢ f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg

Tactic:
apply hδ
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ Membership.mem (γ := Set E) (Metric.eball 0 δ) y

Tactic:
have : y ∈ Metric.eball (0 : E) δ :=
      (Metric.eball_subset_eball (le_trans (min_le_left _ _) (min_le_right _ _))) hy
-- Module: Mathlib.Analysis.Analytic.Composition
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
this : Membership.mem (γ := Set E) (Metric.eball 0 δ) y
⊢ x + y ∈ insert x s ∩ Metric.eball x δ

Tactic:
simpa [-Set.mem_insert_iff, edist_eq_enorm_sub, h'y]

Premises used: edist_eq_enorm_sub, Set.mem_insert_iff
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg

Tactic:
have fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg := by
    apply hδ
    have : y ∈ Metric.eball (0 : E) δ :=
      (Metric.eball_subset_eball (le_trans (min_le_left _ _) (min_le_right _ _))) hy
    simpa [-Set.mem_insert_iff, edist_eq_enorm_sub, h'y]
-- Module: Mathlib.Analysis.Analytic.Composition
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
apply :
  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))
⊢ 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:
apply Tendsto.prodMk tendsto_id

Premises used: Filter.tendsto_id, Filter.Tendsto.prodMk
-- Module: Mathlib.Analysis.Analytic.Composition
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
rw :
  ∃ (a : ℕ),
    ∀ b ≥ a,
      (∑ a ∈ Finset.range b, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) - f x =
        ∑ a ∈ Finset.Ico 1 b, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y
⊢ ∀ᶠ (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:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ),
    ∀ b ≥ a,
      (∑ a ∈ Finset.range b, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) - f x =
        ∑ a ∈ Finset.Ico 1 b, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y

Tactic:
⟨1, fun n hn => ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Composition
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
refine :
  ∀ (n : ℕ) (hn : n ≥ 1),
    (∑ 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
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      (∑ a ∈ Finset.range b, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) - f x =
        ∑ a ∈ Finset.Ico 1 b, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y

Tactic:
refine ⟨1, fun n hn => ?_⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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
symm :
  (∑ 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
⊢ (∑ 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:
symm