awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 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)
have h : ∀ (i : Fin 0), 0 = y
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
have apply : ContinuousAt.{u_2, u_3} (Y := F) (fun (x_1 : E) ↦ f (x + x_1)) 0
Tactic: apply ContinuousAt.sub _ continuousAt_const
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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)
have A : 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)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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
⊢ ∀ᶠ (y : E) in 𝓝 0, Membership.mem (γ := Set F) (Metric.eball 0 q.radius) (f (x + y) - f x)
have B : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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,
    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)))
have this : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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) 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)))
have 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)))
Tactic: filter_upwards [hgf.tendsto_partialSum_prod_of_comp hq (hf.radius_pos),
    hf.tendsto_partialSum, this] with y hy h'y h''y
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
⊢ Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
have 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
Tactic: apply (closed_nhds_basis (g (f (x + y)))).tendsto_right_iff.2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ ∀ᶠ (x_1 : ℕ) in atTop, q.partialSum x_1 (f (x + y) - f x) ∈ _root_.id u
have simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → q.partialSum b (f (x + y) - f x) ∈ u
Tactic: simp only [id_eq, eventually_atTop, ge_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → q.partialSum b (f (x + y) - f x) ∈ u
have 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
Tactic: rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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 → q.partialSum b (f (x + y) - f x) ∈ u
have 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
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)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
have refine : ∀ (a : ℕ) (ha : a₀ ≤ a), q.partialSum a (f (x + y) - f x) ∈ u
Tactic: refine ⟨a₀, fun a ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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)))
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
    (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)))
have 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))
Tactic: apply this.tendsto.comp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
    (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))
have apply : Tendsto (fun (x : ℕ) ↦ (p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0) atTop (𝓝 (f x))
Tactic: apply Tendsto.sub h'y
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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 (fun (x : ℕ) ↦ (p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0) atTop (𝓝 (f x))
have h : f x = (p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0
Tactic: convert! tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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
⊢ q.partialSum a (f (x + y) - f x) ∈ u
have 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)))
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