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)
δ : ℝ≥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))))
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))))
D :
  HasSum
    (fun (i : (n : ℕ) × Composition 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)
    (g (f (x + y)))
n : ℕ
simp :
  HasSum.{u_4, 0} (α := G)
    (fun (c : Composition n) ↦
      (q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c fun (_j : Fin n) ↦ y))
    (∑ c : Composition n, (q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c fun (_j : Fin n) ↦ y))
⊢ HasSum.{u_4, 0} (α := G)
    (fun (c : Composition n) ↦
      ((q.compAlongComposition p
              ((Sigma.mk (β := fun (b : ℕ) ↦ Composition b) n c).snd (β := fun (n : ℕ) ↦ Composition n)) :
            (a : (i : Fin ⟨n, c⟩.fst) → E) → G)
          fun (_j : Fin ((Sigma.mk (β := fun (b : ℕ) ↦ Composition b) n c).fst (β := fun (n : ℕ) ↦ Composition n))) ↦
          y :
        G))
    ((q.comp p n : (a : (i : Fin n) → E) → G) fun (_j : Fin n) ↦ y : G)

Tactic:
simp only [compAlongComposition_apply, FormalMultilinearSeries.comp,
      ContinuousMultilinearMap.sum_apply]

Premises used: ContinuousMultilinearMap.sum_apply, FormalMultilinearSeries.compAlongComposition_apply, FormalMultilinearSeries.comp
-- 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 :
  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))))
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))))
D :
  HasSum
    (fun (i : (n : ℕ) × Composition 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)
    (g (f (x + y)))
n : ℕ
⊢ HasSum.{u_4, 0} (α := G)
    (fun (c : Composition n) ↦
      (q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c fun (_j : Fin n) ↦ y))
    (∑ c : Composition n, (q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c fun (_j : Fin n) ↦ y))

Tactic:
hasSum_fintype _

Premises used: hasSum_fintype, SummationFilter.unconditional
-- 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 :
  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))))
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))))
D :
  HasSum
    (fun (i : (n : ℕ) × Composition 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)
    (g (f (x + y)))
n : ℕ
⊢ HasSum.{u_4, 0} (α := G)
    (fun (c : Composition n) ↦
      (q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c fun (_j : Fin n) ↦ y))
    (∑ c : Composition n, (q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c fun (_j : Fin n) ↦ y))

Tactic:
exact hasSum_fintype _

Premises used: hasSum_fintype, SummationFilter.unconditional
-- 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 :
  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))))
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))))
D :
  HasSum
    (fun (i : (n : ℕ) × Composition 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)
    (g (f (x + y)))
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E) → G) fun (_j : Fin n) ↦ y) (g (f (x + y)))

Tactic:
have E : HasSum (fun n => (q.comp p) n fun _j => y) (g (f (x + y))) := by
    apply D.sigma
    intro n
    simp only [compAlongComposition_apply, FormalMultilinearSeries.comp,
      ContinuousMultilinearMap.sum_apply]
    exact hasSum_fintype _
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E_1 : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E_1 → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E_1 F
x : E_1
t : Set F
s : Set E_1
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_1}, 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_1
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E_1) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E_1) (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_1) → 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_1) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E_1) → G)
          fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    atTop (𝓝 (g (f (x + y))))
D :
  HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E_1) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (g (f (x + y)))
E : HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E_1) → G) fun (_j : Fin n) ↦ y) (g (f (x + y)))
rw : HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E_1) → G) fun (x : Fin n) ↦ y) (g (f (x + y)))
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E_1) → G) fun (x : Fin n) ↦ y) ((g ∘ f) (x + y))

Tactic:
rw [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E_1 : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E_1 → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E_1 F
x : E_1
t : Set F
s : Set E_1
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_1}, 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_1
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E_1) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E_1) (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_1) → 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_1) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E_1) → G)
          fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    atTop (𝓝 (g (f (x + y))))
D :
  HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E_1) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (g (f (x + y)))
E : HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E_1) → G) fun (_j : Fin n) ↦ y) (g (f (x + y)))
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E_1) → G) fun (x : Fin n) ↦ y) (g (f (x + y)))

Tactic:
E

Premises used: Multiset.powerset, Multiset.ofList
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E_1 : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E_1 → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E_1 F
x : E_1
t : Set F
s : Set E_1
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_1}, 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_1
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E_1) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E_1) (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_1) → 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_1) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E_1) → G)
          fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    atTop (𝓝 (g (f (x + y))))
D :
  HasSum
    (fun (i : (n : ℕ) × Composition n) ↦
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E_1) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y)
    (g (f (x + y)))
E : HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E_1) → G) fun (_j : Fin n) ↦ y) (g (f (x + y)))
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E_1) → G) fun (x : Fin n) ↦ y) (g (f (x + y)))

Tactic:
exact E
-- 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
hg : HasFPowerSeriesAt g q (f x)
hf : HasFPowerSeriesAt f p x
rw :
  ∀ (hg : HasFPowerSeriesWithinAt g q Set.univ (f x)) (hf : HasFPowerSeriesWithinAt f p Set.univ x),
    HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) Set.univ x
⊢ HasFPowerSeriesAt (g ∘ f) (q.comp p) x

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf hg ⊢

Premises used: hasFPowerSeriesWithinAt_univ
-- 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
hg : HasFPowerSeriesWithinAt g q Set.univ (f x)
hf : HasFPowerSeriesWithinAt f p Set.univ x
⊢ Set.MapsTo f Set.univ Set.univ

Tactic:
simp
-- 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
hg : HasFPowerSeriesWithinAt g q Set.univ (f x)
hf : HasFPowerSeriesWithinAt f p Set.univ x
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) Set.univ x

Tactic:
apply hg.comp hf (by simp)

Premises used: HasFPowerSeriesWithinAt.comp
-- 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
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
let : ∀ (_q : FormalMultilinearSeries 𝕜 F G) (hq : HasFPowerSeriesWithinAt g _q t (f x)), AnalyticWithinAt 𝕜 (g ∘ f) s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
let ⟨_q, hq⟩ := hg
-- 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
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
let : ∀ (_p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesWithinAt f _p s x), AnalyticWithinAt 𝕜 (g ∘ f) s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
let ⟨_p, hp⟩ := hf
-- 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
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
_p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f _p s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
(hq.comp hp h).analyticWithinAt

Premises used: HasFPowerSeriesWithinAt.analyticWithinAt, HasFPowerSeriesWithinAt.comp
-- 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
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
_p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f _p s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
exact (hq.comp hp h).analyticWithinAt

Premises used: HasFPowerSeriesWithinAt.analyticWithinAt, HasFPowerSeriesWithinAt.comp
-- 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
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t y
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
⊢ AnalyticWithinAt 𝕜 g t (f x)

Tactic:
rw [← hy] at hg
-- 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
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t y
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
hg₁ : AnalyticWithinAt 𝕜 g t (f x)
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
rw [← hy] at hg
-- 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
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t y
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
hg₁ : AnalyticWithinAt 𝕜 g t (f x)
hf₁ : AnalyticWithinAt 𝕜 f s x
⊢ Set.MapsTo f s t

Tactic:
rw [← hy] at hg
-- 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
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t y
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
hg₁ : AnalyticWithinAt 𝕜 g t (f x)
hf₁ : AnalyticWithinAt 𝕜 f s x
h₁ : Set.MapsTo f s t
⊢ f x = y

Tactic:
rw [← hy] at hg