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_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
h₁ h₂ :
  ∀ (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
⊢ ∀ᶠ (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:
filter_upwards [Ici_mem_atTop b₀] with b hb using vu (hab _ _ ha hb)

Premises used: Filter.Ici_mem_atTop
-- 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)
⊢ 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)
-- 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)
L : Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
⊢ 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
-- 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)
L : Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
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)
⊢ 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:
cauchySeq_finset_of_norm_bounded Z (fun i ↦ le_rfl)

Premises used: le_rfl, cauchySeq_finset_of_norm_bounded
-- 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)
L : Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
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)
⊢ 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:
exact cauchySeq_finset_of_norm_bounded Z (fun i ↦ le_rfl)

Premises used: le_rfl, cauchySeq_finset_of_norm_bounded
-- 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)
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

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)
-- 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)
L : Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
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
⊢ 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:
tendsto_nhds_of_cauchySeq_of_subseq C tendsto_finset_range L

Premises used: iInf, tendsto_nhds_of_cauchySeq_of_subseq, Filter.atTop, Filter.tendsto_finset_range, HasSum
-- 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)
L : Tendsto (fun (n : ℕ) ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y))))
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
⊢ 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:
exact tendsto_nhds_of_cauchySeq_of_subseq C tendsto_finset_range L

Premises used: tendsto_nhds_of_cauchySeq_of_subseq, Filter.tendsto_finset_range
-- 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
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))
rw : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) (FormalMultilinearSeries.id 𝕜 E a) a
⊢ HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) ((p.leftInv i a).comp p) a

Tactic:
rw [leftInv_comp _ _ _ hp]

Premises used: FormalMultilinearSeries.leftInv_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
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) (FormalMultilinearSeries.id 𝕜 E a) a

Tactic:
(ContinuousLinearMap.id 𝕜 E).hasFPowerSeriesAt a

Premises used: ContinuousLinearMap.hasFPowerSeriesAt, ContinuousLinearMap.id, FormalMultilinearSeries.id
-- 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
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) (FormalMultilinearSeries.id 𝕜 E a) a

Tactic:
exact (ContinuousLinearMap.id 𝕜 E).hasFPowerSeriesAt a

Premises used: ContinuousLinearMap.hasFPowerSeriesAt, ContinuousLinearMap.id
-- 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
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

Tactic:
have : HasFPowerSeriesAt (ContinuousLinearMap.id 𝕜 E) ((p.leftInv i a).comp p) a := by
      rw [leftInv_comp _ _ _ hp]
      exact (ContinuousLinearMap.id 𝕜 E).hasFPowerSeriesAt a
-- 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
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
apply : (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) =ᶠ[𝓝 a] (↑f.symm : F → E) ∘ (↑f : E → F)
⊢ HasFPowerSeriesAt ((↑f.symm : F → E) ∘ (↑f : E → F)) ((p.leftInv i a).comp p) a

Tactic:
apply this.congr

Premises used: HasFPowerSeriesAt.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
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
x : E
hx : x ∈ f.source
⊢ (ContinuousLinearMap.id 𝕜 E : (a : E) → E) x = ((↑f.symm : F → E) ∘ (↑f : E → F)) x

Tactic:
simp [hx]
-- 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
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
h₂ h₃ :
  ∀ (x : E) (hx : x ∈ f.source), (ContinuousLinearMap.id 𝕜 E : (a : E) → E) x = ((↑f.symm : F → E) ∘ (↑f : E → F)) x
⊢ (⇑(ContinuousLinearMap.id 𝕜 E) : (a : E) → E) =ᶠ[𝓝 a] (↑f.symm : F → E) ∘ (↑f : E → F)

Tactic:
filter_upwards [f.open_source.mem_nhds h0] with x hx using by simp [hx]

Premises used: OpenPartialHomeomorph.open_source, IsOpen.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
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

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]
-- 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
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
⊢ ∀ᶠ (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:
simpa using A.eventually_hasSum_of_comp h (radius_leftInv_pos_of_radius_pos h.radius_pos hp)

Premises used: HasFPowerSeriesAt.radius_pos, HasFPowerSeriesAt.eventually_hasSum_of_comp, FormalMultilinearSeries.radius_leftInv_pos_of_radius_pos
-- 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
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
⊢ ∀ᶠ (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)