-- Mathlib/Analysis/Analytic/Inverse.lean
theorem PartialHomeomorph.hasFPowerSeriesAt_symm (f : PartialHomeomorph E F) {a : E}
    {i : E ≃L[𝕜] F} (h0 : a ∈ f.source) {p : FormalMultilinearSeries 𝕜 E F}
    (h : HasFPowerSeriesAt f p a) (hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
    HasFPowerSeriesAt f.symm (p.leftInv i a) (f a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n => (p.leftInv i a n) fun x => ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
C : ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) (↑f.symm (↑f y))
D : ∀ᶠ (y : E) in 𝓝 (↑f.symm (↑f a)), HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) y
⊢ ∀ᶠ (z : F) in 𝓝 (↑f a), HasSum (fun n => (p.leftInv i a n) fun x => ↑f (↑f.symm z) - ↑f a) (↑f.symm z)

Tactic:
have : ContinuousAt f.symm (f a) := f.continuousAt_symm (f.map_source h0)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n => (p.leftInv i a n) fun x => ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
C : ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) (↑f.symm (↑f y))
D : ∀ᶠ (y : E) in 𝓝 (↑f.symm (↑f a)), HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) y
this : ContinuousAt (↑f.symm) (↑f a)
⊢ ∀ᶠ (z : F) in 𝓝 (↑f a), HasSum (fun n => (p.leftInv i a n) fun x => ↑f (↑f.symm z) - ↑f a) (↑f.symm z)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n => (p.leftInv i a n) fun x => ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
⊢ ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) (↑f.symm (↑f y))

Tactic:
rw [← sub_eq_zero_of_eq (a := a) rfl] at B

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 (a - a), HasSum (fun n => (p.leftInv i a n) fun x => ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
⊢ ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) (↑f.symm (↑f y))

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace 𝕜 E✝
F✝ : Type u_3
inst✝¹ : NormedAddCommGroup F✝
inst✝ : NormedSpace 𝕜 F✝
f : PartialHomeomorph E✝ F✝
a : E✝
i : E✝ ≃L[𝕜] F✝
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E✝ F✝
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E✝ F✝).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E✝) in 𝓝 0, HasSum (fun n => (p.leftInv i a n) fun x => ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
C : ∀ᶠ (y : E✝) in 𝓝 a, HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) (↑f.symm (↑f y))
D : ∀ᶠ (y : E✝) in 𝓝 (↑f.symm (↑f a)), HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) y
E : ∀ᶠ (z : F✝) in 𝓝 (↑f a), HasSum (fun n => (p.leftInv i a n) fun x => ↑f (↑f.symm z) - ↑f a) (↑f.symm z)
F : ∀ᶠ (z : F✝) in 𝓝 (↑f a), HasSum (fun n => (p.leftInv i a n) fun x => z - ↑f a) (↑f.symm z)
r : ℝ≥0∞
r_pos : r > 0
hr : EMetric.ball (↑f a) r ⊆ {x | (fun z => HasSum (fun n => (p.leftInv i a n) fun x => z - ↑f a) (↑f.symm z)) x}
y : F✝
hy : y ∈ EMetric.ball 0 (r ⊓ (p.leftInv i a).radius)
this : y + ↑f a ∈ EMetric.ball (↑f a) r
⊢ HasSum (fun n => (p.leftInv i a n) fun x => y) (↑f.symm (↑f a + y))

Tactic:
simpa [add_comm] using hr this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n => (p.leftInv i a n) fun x => ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
⊢ HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)

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

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n => (p.leftInv i a n) fun x => ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
C : ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) (↑f.symm (↑f y))
⊢ HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)