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
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 - 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

Premises used: sub_eq_zero_of_eq, 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
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)))
⊢ ContinuousAt (Y := E) (fun (x : E) ↦ x - a) a

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
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)))
⊢ ContinuousAt (Y := E) (fun (x : E) ↦ x - a) a

Tactic:
have : ContinuousAt (fun x ↦ x - a) a := by fun_prop
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
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)))
this : ContinuousAt (Y := E) (fun (x : E) ↦ x - a) a
⊢ ∀ᶠ (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:
simpa using this.preimage_mem_nhds B

Premises used: ContinuousAt.preimage_mem_nhds
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
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))

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
-- 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
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)))
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))
simp :
  ∀ᶠ (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) y
⊢ ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) 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) y

Tactic:
simp only [h0, OpenPartialHomeomorph.left_inv]

Premises used: OpenPartialHomeomorph.left_inv
-- 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
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)))
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))
h₁ :
  ∀ (x : E)
    (hx :
      HasSum
        (fun (n : ℕ) ↦
          (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x_1 : Fin n) ↦ (↑f : E → F) x - (↑f : E → F) a)
        ((↑f.symm : F → E) ((↑f : E → F) x)))
    (h'x : x ∈ f.source),
    HasSum
      (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x_1 : Fin n) ↦ (↑f : E → F) x - (↑f : E → F) a)
      x
⊢ ∀ᶠ (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) y

Tactic:
filter_upwards [C, f.open_source.mem_nhds h0] with x hx h'x

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))
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)))
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))
x : E
hx :
  HasSum
    (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x_1 : Fin n) ↦ (↑f : E → F) x - (↑f : E → F) a)
    ((↑f.symm : F → E) ((↑f : E → F) x))
h'x : x ∈ f.source
⊢ HasSum
    (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x_1 : Fin n) ↦ (↑f : E → F) x - (↑f : E → F) a) x

Tactic:
simpa [h'x] using 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
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)))
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))
⊢ ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) 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) y

Tactic:
have D : ∀ᶠ (y : E) in 𝓝 (f.symm (f a)),
      HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f y - f a) y := by
    simp only [h0, OpenPartialHomeomorph.left_inv]
    filter_upwards [C, f.open_source.mem_nhds h0] with x hx h'x
    simpa [h'x] using 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
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)))
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))
D :
  ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) 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) y
⊢ ContinuousAt (↑f.symm : F → E) ((↑f : E → F) a)

Tactic:
have : ContinuousAt f.symm (f a) := f.continuousAt_symm (f.map_source h0)
-- 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
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)))
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))
D :
  ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) 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) y
this : ContinuousAt (↑f.symm : F → E) ((↑f : E → F) a)
⊢ ∀ᶠ (z : F) in 𝓝 ((↑f : E → F) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦
          (↑f : E → F) ((↑f.symm : F → E) z) - (↑f : E → F) a)
      ((↑f.symm : F → E) z)

Tactic:
this D

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, Filter.Tendsto, 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
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)))
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))
D :
  ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) 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) y
this : ContinuousAt (↑f.symm : F → E) ((↑f : E → F) a)
⊢ ∀ᶠ (z : F) in 𝓝 ((↑f : E → F) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦
          (↑f : E → F) ((↑f.symm : F → E) z) - (↑f : E → F) a)
      ((↑f.symm : F → E) z)

Tactic:
exact this D
-- 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
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)))
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))
D :
  ∀ᶠ (y : E) in 𝓝 ((↑f.symm : F → E) ((↑f : E → F) 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) y
⊢ ∀ᶠ (z : F) in 𝓝 ((↑f : E → F) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E) fun (x : Fin n) ↦
          (↑f : E → F) ((↑f.symm : F → E) z) - (↑f : E → F) a)
      ((↑f.symm : F → E) z)

Tactic:
have E : ∀ᶠ z in 𝓝 (f a), HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f (f.symm z) - f a)
      (f.symm z) := by
    have : ContinuousAt f.symm (f a) := f.continuousAt_symm (f.map_source h0)
    exact this D
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E_1 F
a : E_1
i : E_1 ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F
h : HasFPowerSeriesAt (↑f : E_1 → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F) :
        (a : E_1 →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F)
      (↑i : E_1 →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E_1) ∘ (↑f : E_1 → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F) (a + y) - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) ((↑f : E_1 → F) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F) y - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) ((↑f : E_1 → F) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F → E_1) ((↑f : E_1 → F) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F) y - (↑f : E_1 → F) a)
      y
E :
  ∀ᶠ (z : F) in 𝓝 ((↑f : E_1 → F) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F) ((↑f.symm : F → E_1) z) - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) z)
h₁ :
  ∀ (z : F) (hz : z ∈ f.target)
    (h'z :
      HasSum
        (fun (n : ℕ) ↦
          (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦
            (↑f : E_1 → F) ((↑f.symm : F → E_1) z) - (↑f : E_1 → F) a)
        ((↑f.symm : F → E_1) z)),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) z)
⊢ ∀ᶠ (z : F) in 𝓝 ((↑f : E_1 → F) a),
    HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) z)

Tactic:
filter_upwards [f.open_target.mem_nhds (f.map_source h0), E] with z hz h'z

Premises used: OpenPartialHomeomorph.map_source, IsOpen.mem_nhds, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E_1 F
a : E_1
i : E_1 ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E_1 F
h : HasFPowerSeriesAt (↑f : E_1 → F) p a
hp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E_1) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E_1 F) :
        (a : E_1 →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E_1) F)
      (↑i : E_1 →L[𝕜] F))
A : HasFPowerSeriesAt ((↑f.symm : F → E_1) ∘ (↑f : E_1 → F)) ((p.leftInv i a).comp p) a
B :
  ∀ᶠ (y : E_1) in 𝓝 0,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F) (a + y) - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) ((↑f : E_1 → F) (a + y)))
C :
  ∀ᶠ (y : E_1) in 𝓝 a,
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F) y - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) ((↑f : E_1 → F) y))
D :
  ∀ᶠ (y : E_1) in 𝓝 ((↑f.symm : F → E_1) ((↑f : E_1 → F) a)),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ (↑f : E_1 → F) y - (↑f : E_1 → F) a)
      y
E :
  ∀ᶠ (z : F) in 𝓝 ((↑f : E_1 → F) a),
    HasSum
      (fun (n : ℕ) ↦
        (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦
          (↑f : E_1 → F) ((↑f.symm : F → E_1) z) - (↑f : E_1 → F) a)
      ((↑f.symm : F → E_1) z)
z : F
hz : z ∈ f.target
h'z :
  HasSum
    (fun (n : ℕ) ↦
      (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦
        (↑f : E_1 → F) ((↑f.symm : F → E_1) z) - (↑f : E_1 → F) a)
    ((↑f.symm : F → E_1) z)
⊢ HasSum (fun (n : ℕ) ↦ (p.leftInv i a n : (a : (i : Fin n) → F) → E_1) fun (x : Fin n) ↦ z - (↑f : E_1 → F) a)
    ((↑f.symm : F → E_1) z)

Tactic:
simpa [hz] using h'z