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 → 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
obtain :
  ∀ (a₀ b₀ : ℕ)
    (hab :
      ∀ (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),
    ∃ (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:
obtain ⟨a₀, b₀, hab⟩ : ∃ a₀ b₀, ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b →
        q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0) ∈ v := by
      simpa using hy (v_open.mem_nhds hv)
-- 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₀ : ℕ
hab :
  ∀ (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
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → q.partialSum b (f (x + y) - f x) ∈ u

Tactic:
⟨a₀, fun a ha ↦ ?_⟩

Premises used: Exists.intro
-- 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₀ : ℕ
hab :
  ∀ (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
refine : ∀ (a : ℕ) (ha : a₀ ≤ a), q.partialSum a (f (x + y) - f x) ∈ u
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → q.partialSum b (f (x + y) - f x) ∈ u

Tactic:
refine ⟨a₀, fun a ha ↦ ?_⟩
-- 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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
⊢ ContinuousAt (q.partialSum a) (f (x + y) - f x)

Tactic:
have : ContinuousAt (q.partialSum a) (f (x + y) - f x) :=
        (partialSum_continuous q a).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
this_1 : ∀ᶠ (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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
apply :
  Tendsto
    (fun (b : ℕ) ↦ HSub.hSub (β := F) (p.partialSum b y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F))
    atTop (𝓝 (f (x + y) - f x))
⊢ Tendsto
    (fun (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)))
    atTop (𝓝 (q.partialSum a (f (x + y) - f x)))

Tactic:
apply this.tendsto.comp

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp
-- 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_1 : ∀ᶠ (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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
apply : Tendsto (fun (x : ℕ) ↦ (p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0) atTop (𝓝 (f x))
⊢ Tendsto
    (fun (b : ℕ) ↦ HSub.hSub (β := F) (p.partialSum b y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F))
    atTop (𝓝 (f (x + y) - f x))

Tactic:
apply Tendsto.sub h'y

Premises used: Filter.Tendsto.sub
-- 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_1 : ∀ᶠ (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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ Tendsto.{0, u_3} (β := F) (fun (x : ℕ) ↦ ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)) atTop
    (𝓝 ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0) : Filter F)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_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
this_1 : ∀ᶠ (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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
h : f x = (p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0
⊢ Tendsto (fun (x : ℕ) ↦ (p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0) atTop (𝓝 (f x))

Tactic:
convert! tendsto_const_nhds

Premises used: tendsto_const_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
this_1 : ∀ᶠ (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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ f x = (p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0

Tactic:
(HasFPowerSeriesAt.coeff_zero hf fun _ ↦ 0).symm

Premises used: HasFPowerSeriesAt.coeff_zero, OfNat.ofNat, Eq.symm
-- 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_1 : ∀ᶠ (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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ f x = (p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0

Tactic:
exact (HasFPowerSeriesAt.coeff_zero hf fun _ ↦ 0).symm

Premises used: HasFPowerSeriesAt.coeff_zero, OfNat.ofNat, Eq.symm
-- 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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
⊢ Tendsto
    (fun (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)))
    atTop (𝓝 (q.partialSum a (f (x + y) - f x)))

Tactic:
have : Tendsto (fun b ↦ q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0)) atTop
        (𝓝 (q.partialSum a (f (x + y) - f x))) := by
      have : ContinuousAt (q.partialSum a) (f (x + y) - f x) :=
        (partialSum_continuous q a).continuousAt
      apply this.tendsto.comp
      apply Tendsto.sub h'y
      convert! tendsto_const_nhds
      exact (HasFPowerSeriesAt.coeff_zero hf fun _ ↦ 0).symm
-- 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_1 : ∀ᶠ (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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
this :
  Tendsto
    (fun (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)))
    atTop (𝓝 (q.partialSum a (f (x + y) - f x)))
apply :
  ∀ᶠ (x : ℕ) in atTop,
    q.partialSum a (HSub.hSub (β := F) (p.partialSum x y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)) ∈
      u
⊢ q.partialSum a (f (x + y) - f x) ∈ u

Tactic:
apply u_closed.mem_of_tendsto this

Premises used: IsClosed.mem_of_tendsto
-- 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_1 : ∀ᶠ (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₀ : ℕ
hab :
  ∀ (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
a : ℕ
ha : a₀ ≤ a
this :
  Tendsto
    (fun (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)))
    atTop (𝓝 (q.partialSum a (f (x + y) - f x)))
b : ℕ
hb : b ∈ Set.Ici 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)) ∈ u

Tactic:
vu (hab _ _ ha hb)