awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
h : Monotone (β := Finset ((n : ℕ) × Composition n)) fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2
h' : ∀ (x : (n : ℕ) × Composition n), ∃ (n : ℕ × ℕ), x ∈ compPartialSumTarget 0 n.1 n.2
⊢ Tendsto (β := Finset ((n : ℕ) × Composition n)) (fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) atTop atTop

Tactic:
apply Monotone.tendsto_atTop_finset

Premises used: Monotone.tendsto_atTop_finset
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : Membership.mem (γ := Finset ((n : ℕ) × Composition n)) ((fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) m) a
⊢ ∀ i < m.1, i < n.1

Tactic:
have : ∀ i, i < m.1 → i < n.1 := fun i hi => lt_of_lt_of_le hi hmn.1
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : Membership.mem (γ := Finset ((n : ℕ) × Composition n)) ((fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) m) a
this : ∀ i < m.1, i < n.1
⊢ ∀ i < m.2, i < n.2

Tactic:
have : ∀ i, i < m.2 → i < n.2 := fun i hi => lt_of_lt_of_le hi hmn.2
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : Membership.mem (γ := Finset ((n : ℕ) × Composition n)) ((fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) m) a
this_1 : ∀ i < m.1, i < n.1
this : ∀ i < m.2, i < n.2
⊢ Membership.mem (γ := Finset ((n : ℕ) × Composition n)) ((fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) n) a

Tactic:
simp_all
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
c : Composition n
h' : ∃ (n_1 : ℕ × ℕ), 0 ≤ c.length ∧ c.length < n_1.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n_1.2
⊢ ∃ (n_1 : ℕ × ℕ), Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTarget 0 n_1.1 n_1.2

Tactic:
simp only [mem_compPartialSumTarget_iff]

Premises used: FormalMultilinearSeries.mem_compPartialSumTarget_iff
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
c : Composition n
⊢ BddAbove (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)

Tactic:
Finset.bddAbove _

Premises used: Finset.bddAbove
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
c : Composition n
h' :
  ∀ (n_1 : ℕ) (hn : n_1 ∈ upperBounds (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)),
    ∃ (n_2 : ℕ × ℕ), 0 ≤ c.length ∧ c.length < n_2.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n_2.2
⊢ ∃ (n_1 : ℕ × ℕ), 0 ≤ c.length ∧ c.length < n_1.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n_1.2

Tactic:
obtain ⟨n, hn⟩ : BddAbove ((Finset.univ.image fun i : Fin c.length => c.blocksFun i) : Set ℕ) :=
      Finset.bddAbove _

Premises used: Finset.univ, Finset.bddAbove, Composition.blocksFun, BddAbove, SetLike.coe, Finset.image
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n_1 : ℕ
c : Composition n_1
n : ℕ
hn : n ∈ upperBounds (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)
⊢ ∃ (n : ℕ × ℕ), 0 ≤ c.length ∧ c.length < n.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n.2

Tactic:
⟨max n c.length + 1, bot_le, lt_of_le_of_lt (le_max_right n c.length) (lt_add_one _), fun j =>
        lt_of_le_of_lt (le_trans ?_ (le_max_left _ _)) (lt_add_one _)⟩

Premises used: le_max_right, lt_of_le_of_lt, Composition.length, lt_add_one, Nat.cast, HAdd.hAdd, Max.max, And.intro, Exists.intro, OfNat.ofNat, le_max_left, bot_le, le_trans
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n_1 : ℕ
c : Composition n_1
n : ℕ
hn : n ∈ upperBounds (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)
h' : ∀ (j : Fin c.length), c.blocksFun j ≤ n
⊢ ∃ (n : ℕ × ℕ), 0 ≤ c.length ∧ c.length < n.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n.2

Tactic:
refine
      ⟨max n c.length + 1, bot_le, lt_of_le_of_lt (le_max_right n c.length) (lt_add_one _), fun j =>
        lt_of_le_of_lt (le_trans ?_ (le_max_left _ _)) (lt_add_one _)⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n_1 : ℕ
c : Composition n_1
n : ℕ
hn : n ∈ upperBounds (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)
j : Fin c.length
h' : c.blocksFun j ∈ (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)
⊢ c.blocksFun j ≤ n

Tactic:
apply hn
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n_1 : ℕ
c : Composition n_1
n : ℕ
hn : n ∈ upperBounds (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)
j : Fin c.length
⊢ c.blocksFun j ∈ (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)

Tactic:
simp only [Finset.mem_image_of_mem, Finset.mem_coe, Finset.mem_univ]

Premises used: Finset.mem_univ, Finset.mem_image_of_mem, Finset.mem_coe
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
⊢ Tendsto (β := Finset ((n : ℕ) × Composition n)) (fun (N : ℕ) ↦ compPartialSumTarget 0 N N) atTop atTop

Tactic:
apply Tendsto.comp compPartialSumTarget_tendsto_prod_atTop tendsto_atTop_diagonal

Premises used: Filter.tendsto_atTop_diagonal, Filter.Tendsto.comp, FormalMultilinearSeries.compPartialSumTarget_tendsto_prod_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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
H :
  Eq.{u_4 + 1} (α := G)
    (∑ n ∈ Finset.range M,
      ∑ r ∈ Fintype.piFinset (δ := fun (i : Fin n) ↦ ℕ) fun (i : Fin n) ↦ Finset.Ico 1 N,
        (q n : (a : (i : Fin n) → F) → G) fun (i : Fin n) ↦
          (p (r i) : (a : (i : Fin (r i)) → E) → F) fun (_j : Fin (r i)) ↦ z)
    (∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z)
⊢ q.partialSum M (∑ i ∈ Finset.Ico 1 N, (p i : (a : (i : Fin i) → E) → F) fun (_j : Fin i) ↦ z) =
    ∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z

Tactic:
simpa only [FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset] using H

Premises used: FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset
-- 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
suffices :
  Eq.{u_4 + 1} (α := G)
    (∑ n ∈ Finset.range M,
      ∑ r ∈ Fintype.piFinset (δ := fun (i : Fin n) ↦ ℕ) fun (i : Fin n) ↦ Finset.Ico 1 N,
        (q n : (a : (i : Fin n) → F) → G) fun (i : Fin n) ↦
          (p (r i) : (a : (i : Fin (r i)) → E) → F) fun (_j : Fin (r i)) ↦ z)
    (∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z)
⊢ q.partialSum M (∑ i ∈ Finset.Ico 1 N, (p i : (a : (i : Fin i) → E) → F) fun (_j : Fin i) ↦ z) =
    ∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z

Tactic:
suffices H :
    (∑ n ∈ Finset.range M,
        ∑ r ∈ Fintype.piFinset fun i : Fin n => Finset.Ico 1 N,
          q n fun i : Fin n => p (r i) fun _j => z) =
      ∑ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z by
    simpa only [FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset] using 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
rw :
  Eq.{u_4 + 1} (α := G)
    (∑
      x ∈
        (Finset.Ico 0 M).sigma (α := fun (a : ℕ) ↦ (a : Fin a) → ℕ) fun (n : ℕ) ↦
          Fintype.piFinset (δ := fun (i : Fin n) ↦ ℕ) fun (i : Fin n) ↦ Finset.Ico 1 N,
      (q (x.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ)) : (a : (i : Fin x.fst) → F) → G)
        fun (i : Fin (x.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ))) ↦
        (p (x.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i) : (a : (i : Fin (x.snd i)) → E) → F)
          fun (_j : Fin (x.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i)) ↦ z)
    (∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z)
⊢ Eq.{u_4 + 1} (α := G)
    (∑ n ∈ Finset.range M,
      ∑ r ∈ Fintype.piFinset (δ := fun (i : Fin n) ↦ ℕ) fun (i : Fin n) ↦ Finset.Ico 1 N,
        (q n : (a : (i : Fin n) → F) → G) fun (i : Fin n) ↦
          (p (r i) : (a : (i : Fin (r i)) → E) → F) fun (_j : Fin (r i)) ↦ z)
    (∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z)

Tactic:
rw [Finset.range_eq_Ico, Finset.sum_sigma']

Premises used: Finset.sum_sigma', Finset.range_eq_Ico
-- 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
h :
  ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource 0 M N),
    Eq.{u_4 + 1} (α := G)
      ((q (e.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ)) : (a : (i : Fin e.fst) → F) → G)
          fun (i : Fin (e.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ))) ↦
          (p (e.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i) : (a : (i : Fin (e.snd i)) → E) → F)
            fun (_j : Fin (e.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i)) ↦ z :
        G)
      ((q.compAlongComposition p ((compChangeOfVariables 0 M N e he).snd (β := fun (n : ℕ) ↦ Composition n)) :
            (a : (i : Fin (compChangeOfVariables 0 M N e he).fst) → E) → G)
          fun (_j : Fin ((compChangeOfVariables 0 M N e he).fst (β := fun (n : ℕ) ↦ Composition n))) ↦ z :
        G)
⊢ Eq.{u_4 + 1} (α := G)
    (∑
      x ∈
        (Finset.Ico 0 M).sigma (α := fun (a : ℕ) ↦ (a : Fin a) → ℕ) fun (n : ℕ) ↦
          Fintype.piFinset (δ := fun (i : Fin n) ↦ ℕ) fun (i : Fin n) ↦ Finset.Ico 1 N,
      (q (x.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ)) : (a : (i : Fin x.fst) → F) → G)
        fun (i : Fin (x.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ))) ↦
        (p (x.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i) : (a : (i : Fin (x.snd i)) → E) → F)
          fun (_j : Fin (x.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i)) ↦ z)
    (∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z)

Tactic:
apply compChangeOfVariables_sum 0 M N

Premises used: OfNat.ofNat, FormalMultilinearSeries.compChangeOfVariables_sum
-- 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
hg : HasFPowerSeriesWithinAt g q t (f x)
hf : HasFPowerSeriesWithinAt f p s x
hs : Set.MapsTo f s t
rcases : ∀ (rg : ℝ≥0∞) (Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg), HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x

Tactic:
rcases hg with ⟨rg, 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hf : HasFPowerSeriesWithinAt f p s x
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rcases : ∀ (rf : ℝ≥0∞) (Hf : HasFPowerSeriesWithinOnBall f p s x rf), HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x

Tactic:
rcases hf with ⟨rf, 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
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
rcases :
  ∀ (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)),
    HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x

Tactic:
rcases q.comp_summable_nnreal p Hg.radius_pos Hf.radius_pos with ⟨r, r_pos : 0 < r, hr⟩

Premises used: HasFPowerSeriesWithinOnBall.radius_pos, FormalMultilinearSeries.comp_summable_nnreal
-- 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)
h : Metric.eball (f x) rg ∈ 𝓝 (f x)
⊢ insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x

Tactic:
apply inter_mem_nhdsWithin

Premises used: inter_mem_nhdsWithin
-- 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)
⊢ Metric.eball (f x) rg ∈ 𝓝 (f x)

Tactic:
Metric.eball_mem_nhds _ Hg.r_pos

Premises used: Set.Mem, Metric.eball_mem_nhds, HasFPowerSeriesWithinOnBall.r_pos
-- 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)
⊢ Metric.eball (f x) rg ∈ 𝓝 (f x)

Tactic:
exact Metric.eball_mem_nhds _ Hg.r_pos

Premises used: Metric.eball_mem_nhds, HasFPowerSeriesWithinOnBall.r_pos
-- 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)
⊢ insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x

Tactic:
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
-- 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)
this : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x
⊢ insert (f x) t ∩ Metric.eball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)

Tactic:
have := Hf.analyticWithinAt.continuousWithinAt_insert.tendsto_nhdsWithin (hs.insert x) this
-- 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)
this_1 : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ Metric.eball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
rcases :
  ∀ (δ : ℝ≥0∞) (δpos : δ > 0) (Hδ : Metric.eball x δ ∩ insert x s ⊆ f ⁻¹' (insert (f x) t ∩ Metric.eball (f x) rg)),
    ∃ (δ : ℝ≥0∞), 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
⊢ ∃ (δ : ℝ≥0∞), 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg

Tactic:
rcases EMetric.mem_nhdsWithin_iff.1 this with ⟨δ, δpos, Hδ⟩

Premises used: Iff.mp, EMetric.mem_nhdsWithin_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)
this_1 : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ Metric.eball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
δ : ℝ≥0∞
δpos : δ > 0
Hδ : Metric.eball x δ ∩ insert x s ⊆ f ⁻¹' (insert (f x) t ∩ Metric.eball (f x) rg)
z : E
hz : z ∈ insert x s ∩ Metric.eball x δ
rwa rwa₁ rwa₂ rwa₃ : z ∈ insert x s ∩ Metric.eball x δ
⊢ z ∈ Metric.eball x δ ∩ insert x s

Tactic:
rwa [Set.inter_comm]

Premises used: 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)
this_1 : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ Metric.eball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
δ : ℝ≥0∞
δpos : δ > 0
Hδ : Metric.eball x δ ∩ insert x s ⊆ f ⁻¹' (insert (f x) t ∩ Metric.eball (f x) rg)
⊢ ∃ (δ : ℝ≥0∞), 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg

Tactic:
exact ⟨δ, δpos, fun {z} hz => Hδ (by rwa [Set.inter_comm])⟩