awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  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)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (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 (𝓝 (f (x + y)))
C :
  Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (f (x + y)))
fst n : ℕ
hn : 1 ≤ n
h :
  (∑ a ∈ Ico 1 (fst, n).2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    HSub.hSub (β := F) (p.partialSum (fst, n).2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)
⊢ q.partialSum (fst, n).1 (∑ a ∈ Ico 1 (fst, n).2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    q.partialSum (fst, n).1
      (HSub.hSub (β := F) (p.partialSum (fst, n).2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F))

Tactic:
congr
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  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)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (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 (𝓝 (f (x + y)))
C :
  Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (f (x + y)))
fst n : ℕ
hn : 1 ≤ n
h :
  HAdd.hAdd (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)
      (∑ a ∈ Ico 1 (fst, n).2, (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 (x : Fin 0) ↦ y : F)
      (∑ k ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) n, (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F)
⊢ (∑ a ∈ Ico 1 (fst, n).2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y) =
    HSub.hSub (β := F) (p.partialSum (fst, n).2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)

Tactic:
rw [partialSum, eq_sub_iff_add_eq', Finset.range_eq_Ico,
        Finset.sum_eq_sum_Ico_succ_bot hn]

Premises used: eq_sub_iff_add_eq', FormalMultilinearSeries.partialSum, Finset.sum_eq_sum_Ico_succ_bot, Finset.range_eq_Ico
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  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)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (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 (𝓝 (f (x + y)))
C :
  Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (f (x + y)))
fst n : ℕ
hn : 1 ≤ n
h : ∀ (i : Fin 0), 0 = y
⊢ HAdd.hAdd (α := F) (β := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)
      (∑ a ∈ Ico 1 (fst, n).2, (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 (x : Fin 0) ↦ y : F)
      (∑ k ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) n, (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F)

Tactic:
congr with i
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  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)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (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 (𝓝 (f (x + y)))
C :
  Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (f (x + y)))
fst n : ℕ
hn : 1 ≤ n
i : Fin 0
⊢ 0 = y

Tactic:
i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
A :
  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)
    (f (x + y))
B :
  Tendsto
    (fun (n : ℕ × ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
        (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 (𝓝 (f (x + y)))
C :
  Tendsto (fun (n : ℕ × ℕ) ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (f (x + y)))
fst n : ℕ
hn : 1 ≤ n
i : Fin 0
⊢ 0 = y

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
apply : ContinuousAt.{u_2, u_3} (Y := F) (fun (x_1 : E) ↦ f (x + x_1)) 0
⊢ ContinuousAt.{u_2, u_3} (Y := F) (fun (y : E) ↦ f (x + y) - f x) 0

Tactic:
apply ContinuousAt.sub _ continuousAt_const

Premises used: ContinuousAt.sub, continuousAt_const
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
⊢ ContinuousAt (X := E) (HAdd.hAdd x) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
⊢ x + 0 = x

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
⊢ ContinuousAt.{u_2, u_3} (Y := F) (fun (x_1 : E) ↦ f (x + x_1)) 0

Tactic:
exact hf.continuousAt.comp_of_eq (by fun_prop) (by simp)

Premises used: ContinuousAt.comp_of_eq, HasFPowerSeriesAt.continuousAt
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
⊢ ContinuousAt.{u_2, u_3} (Y := F) (fun (y : E) ↦ f (x + y) - f x) 0

Tactic:
have A : ContinuousAt (fun y ↦ f (x + y) - f x) 0 := by
      apply ContinuousAt.sub _ continuousAt_const
      exact hf.continuousAt.comp_of_eq (by fun_prop) (by simp)
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
A : ContinuousAt.{u_2, u_3} (Y := F) (fun (y : E) ↦ f (x + y) - f x) 0
⊢ Metric.eball 0 q.radius ∈ 𝓝 (f (x + 0) - f x)

Tactic:
simpa using Metric.eball_mem_nhds _ hq

Premises used: Metric.eball_mem_nhds
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
A : ContinuousAt.{u_2, u_3} (Y := F) (fun (y : E) ↦ f (x + y) - f x) 0
⊢ Metric.eball 0 q.radius ∈ 𝓝 (f (x + 0) - f x)

Tactic:
have B : Metric.eball 0 q.radius ∈ 𝓝 (f (x + 0) - f x) := by
      simpa using Metric.eball_mem_nhds _ hq
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
A : ContinuousAt.{u_2, u_3} (Y := F) (fun (y : E) ↦ f (x + y) - f x) 0
B : Metric.eball 0 q.radius ∈ 𝓝 (f (x + 0) - f x)
⊢ ∀ᶠ (y : E) in 𝓝 0, Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)

Tactic:
A.preimage_mem_nhds B

Premises used: Set.Mem, Filter.Eventually, setOf, ContinuousAt.preimage_mem_nhds, Set.preimage
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
A : ContinuousAt.{u_2, u_3} (Y := F) (fun (y : E) ↦ f (x + y) - f x) 0
B : Metric.eball 0 q.radius ∈ 𝓝 (f (x + 0) - f x)
⊢ ∀ᶠ (y : E) in 𝓝 0, Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)

Tactic:
exact A.preimage_mem_nhds B

Premises used: ContinuousAt.preimage_mem_nhds
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
⊢ ∀ᶠ (y : E) in 𝓝 0, Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)

Tactic:
have : ∀ᶠ y in 𝓝 (0 : E), f (x + y) - f x ∈ Metric.eball 0 q.radius := by
    have A : ContinuousAt (fun y ↦ f (x + y) - f x) 0 := by
      apply ContinuousAt.sub _ continuousAt_const
      exact hf.continuousAt.comp_of_eq (by fun_prop) (by simp)
    have B : Metric.eball 0 q.radius ∈ 𝓝 (f (x + 0) - f x) := by
      simpa using Metric.eball_mem_nhds _ hq
    exact A.preimage_mem_nhds B
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
h :
  ∀ (y : E)
    (hy :
      Tendsto
        (fun (a : ℕ × ℕ) ↦
          q.partialSum a.1
            (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
        atTop (𝓝 ((g ∘ f) (x + y))))
    (h'y : Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y))))
    (h''y : Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)),
    HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → F) → G) fun (x_1 : Fin n) ↦ f (x + y) - f x) (g (f (x + y)))
⊢ ∀ᶠ (y : E) in 𝓝 0,
    HasSum (fun (n : ℕ) ↦ (q n : (a : (i : Fin n) → F) → G) fun (x_1 : Fin n) ↦ f (x + y) - f x) (g (f (x + y)))

Tactic:
filter_upwards [hgf.tendsto_partialSum_prod_of_comp hq (hf.radius_pos),
    hf.tendsto_partialSum, this] with y hy h'y h''y

Premises used: HasFPowerSeriesAt.radius_pos, HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp, HasFPowerSeriesAt.tendsto_partialSum
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
y : E
hy :
  Tendsto
    (fun (a : ℕ × ℕ) ↦
      q.partialSum a.1
        (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
    atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
apply :
  ∀ (i : Set G),
    i ∈ 𝓝 (g (f (x + y))) ∧ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] i →
      ∀ᶠ (x_1 : ℕ) in atTop, q.partialSum x_1 (f (x + y) - f x) ∈ _root_.id i
⊢ Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))

Tactic:
apply (closed_nhds_basis (g (f (x + y)))).tendsto_right_iff.2

Premises used: Iff.mpr, closed_nhds_basis, HAdd.hAdd, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
y : E
hy :
  Tendsto
    (fun (a : ℕ × ℕ) ↦
      q.partialSum a.1
        (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
    atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → q.partialSum b (f (x + y) - f x) ∈ u
⊢ ∀ᶠ (x_1 : ℕ) in atTop, q.partialSum x_1 (f (x + y) - f x) ∈ _root_.id u

Tactic:
simp only [id_eq, eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.eventually_atTop, id_eq
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
y : E
hy :
  Tendsto
    (fun (a : ℕ × ℕ) ↦
      q.partialSum a.1
        (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
    atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
rcases :
  ∀ (v : Set G) (vu : v ⊆ u) (v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v)
    (hv : g (f (x + y)) ∈ v), ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → q.partialSum b (f (x + y) - f x) ∈ u
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → q.partialSum b (f (x + y) - f x) ∈ u

Tactic:
rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
y : E
hy :
  Tendsto
    (fun (a : ℕ × ℕ) ↦
      q.partialSum a.1
        (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
    atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
v : Set G
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
hv : g (f (x + y)) ∈ v
⊢ ∃ (a₀ : ℕ) (b₀ : ℕ),
    ∀ (a b : ℕ),
      a₀ ≤ a →
        b₀ ≤ b →
          q.partialSum a
              (HSub.hSub (β := F) (p.partialSum b y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)) ∈
            v

Tactic:
simpa using hy (v_open.mem_nhds hv)

Premises used: IsOpen.mem_nhds