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 → 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)))
⊢ q.partialSum a (f (x + y) - f x) ∈ u
have 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
Tactic: apply u_closed.mem_of_tendsto this
-- 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 :
  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)))
⊢ ∀ᶠ (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
have h : ∀ (a_1 : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      x ∈ Set.Ici b₀ →
        Membership.mem (γ := Set ℕ)
          {x : ℕ |
            (fun (x : ℕ) ↦
                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)
              x}
          x}
    a_1
Tactic: filter_upwards [Ici_mem_atTop b₀] with b hb using vu (hab _ _ ha hb)
-- 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 :
  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)))
h :
  ∀ (a_1 : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        x ∈ Set.Ici b₀ →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  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)
                x}
            x}
      a_1
⊢ ∀ᶠ (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
have h₁ : ∀ a_1 ∈ Set.Ici b₀,
  q.partialSum a (HSub.hSub (β := F) (p.partialSum a_1 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)) ∈
    u
Tactic: filter_upwards [Ici_mem_atTop b₀] with b hb using vu (hab _ _ ha hb)
-- 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)
⊢ 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 L : Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
Tactic: have L : Tendsto (fun n ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y)))) := by
    apply (closed_nhds_basis (g (f (x + y)))).tendsto_right_iff.2
    rintro u ⟨hu, u_closed⟩
    simp only [id_eq, eventually_atTop, ge_iff_le]
    rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
    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)
    refine ⟨a₀, fun a ha ↦ ?_⟩
    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
    apply u_closed.mem_of_tendsto this
    filter_upwards [Ici_mem_atTop b₀] with b hb using vu (hab _ _ ha hb)
-- 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)
L : Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
⊢ CauchySeq.{u_4, 0} (α := G) fun (s : Finset ℕ) ↦
    ∑ n ∈ s, (q n : (a : (i : Fin n) → F) → G) fun (x_1 : Fin n) ↦ f (x + y) - f x
have Z : Summable (α := ℝ) fun (n : ℕ) ↦
  norm.{u_4} (E := G) ((q n : (a : (i : Fin n) → F) → G) fun (x_1 : Fin n) ↦ f (x + y) - f x : G)
Tactic: have Z := q.summable_norm_apply (x := f (x + y) - f x) h''y
-- 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)
L : Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
⊢ 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 C : CauchySeq.{u_4, 0} (α := G) fun (s : Finset ℕ) ↦
  ∑ n ∈ s, (q n : (a : (i : Fin n) → F) → G) fun (x_1 : Fin n) ↦ f (x + y) - f x
Tactic: have C : CauchySeq (fun (s : Finset ℕ) ↦ ∑ n ∈ s, q n fun _ : Fin n => (f (x + y) - f x)) := by
    have Z := q.summable_norm_apply (x := f (x + y) - f x) h''y
    exact cauchySeq_finset_of_norm_bounded Z (fun i ↦ le_rfl)
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
⊢ HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) ((p.leftInv i a).comp p) a
have rw : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) (FormalMultilinearSeries.id 𝕜 E a) a
Tactic: rw [leftInv_comp _ _ _ hp]
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
⊢ HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
have this : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) ((p.leftInv i a).comp p) a
Tactic: have : HasFPowerSeriesAt (ContinuousLinearMap.id 𝕜 E) ((p.leftInv i a).comp p) a := by
      rw [leftInv_comp _ _ _ hp]
      exact (ContinuousLinearMap.id 𝕜 E).hasFPowerSeriesAt a
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
this : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) ((p.leftInv i a).comp p) a
⊢ HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
have apply : (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) =ᶠ[𝓝 a] (↑f.symm : F → E) ∘ (↑f : E → F)
Tactic: apply this.congr
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
this : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) ((p.leftInv i a).comp p) a
⊢ (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) =ᶠ[𝓝 a] (↑f.symm : F → E) ∘ (↑f : E → F)
have h₁ : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x : E |
      x ∈ f.source →
        Membership.mem (γ := Set E)
          {x : E |
            (fun (x : E) ↦ (ContinuousLinearMap.id 𝕜 E : (a : E) → E) x = ((↑f.symm : F → E) ∘ (↑f : E → F)) x) x}
          x}
    a
Tactic: filter_upwards [f.open_source.mem_nhds h0] with x hx using by simp [hx]
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
this : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) ((p.leftInv i a).comp p) a
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        x ∈ f.source →
          Membership.mem (γ := Set E)
            {x : E |
              (fun (x : E) ↦ (ContinuousLinearMap.id 𝕜 E : (a : E) → E) x = ((↑f.symm : F → E) ∘ (↑f : E → F)) x) x}
            x}
      a
⊢ (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) =ᶠ[𝓝 a] (↑f.symm : F → E) ∘ (↑f : E → F)
have h₂ : ∀ a ∈ f.source, (ContinuousLinearMap.id 𝕜 E : (a : E) → E) a = ((↑f.symm : F → E) ∘ (↑f : E → F)) a
Tactic: filter_upwards [f.open_source.mem_nhds h0] with x hx using by simp [hx]
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
⊢ HasFPowerSeriesAt (↑f.symm : F → E) (p.leftInv i a) ((↑f : E → F) a)
have A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
Tactic: have A : HasFPowerSeriesAt (f.symm ∘ f) ((p.leftInv i a).comp p) a := by
    have : HasFPowerSeriesAt (ContinuousLinearMap.id 𝕜 E) ((p.leftInv i a).comp p) a := by
      rw [leftInv_comp _ _ _ hp]
      exact (ContinuousLinearMap.id 𝕜 E).hasFPowerSeriesAt a
    apply this.congr
    filter_upwards [f.open_source.mem_nhds h0] with x hx using by simp [hx]
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
⊢ HasFPowerSeriesAt (↑f.symm : F → E) (p.leftInv i a) ((↑f : E → F) a)
have B : ∀ᶠ (y : E) in 𝓝 0,
  HasSum
    (fun (n : ℕ) ↦
      (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
    ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
Tactic: have B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f (a + y) - f a)
      (f.symm (f (a + y))) := by
    simpa using A.eventually_hasSum_of_comp h (radius_leftInv_pos_of_radius_pos h.radius_pos hp)
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
⊢ ∀ᶠ (y : E) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) y))
have B₁ : ∀ᶠ (y : E) in 𝓝 (a - a),
  HasSum
    (fun (n : ℕ) ↦
      (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
    ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
Tactic: rw [← sub_eq_zero_of_eq (a := a) rfl] at B
Cleared hypotheses: B
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E) in 𝓝 (a - a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
⊢ ∀ᶠ (y : E) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) y))
have this : ContinuousAt (Y := E) (fun (x : E) ↦ x - a) a
Tactic: have : ContinuousAt (fun x ↦ x - a) a := by fun_prop
-- 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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f : E → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) (a + y) - (↑f : E → F) a)
      ((↑f.symm : F → E) ((↑f : E → F) (a + y)))
⊢ HasFPowerSeriesAt (↑f.symm : F → E) (p.leftInv i a) ((↑f : E → F) a)
have C : ∀ᶠ (y : E) in 𝓝 a,
  HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦ (↑f : E → F) y - (↑f : E → F) a)
    ((↑f.symm : F → E) ((↑f : E → F) y))
Tactic: have C : ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f y - f a)
      (f.symm (f y)) := by
    rw [← sub_eq_zero_of_eq (a := a) rfl] at B
    have : ContinuousAt (fun x ↦ x - a) a := by fun_prop
    simpa using this.preimage_mem_nhds B