-- 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
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)
⊢ HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)

Tactic:
have F : ∀ᶠ z in 𝓝 (f a), HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ z - f a) (f.symm z) := by
  filter_upwards [f.open_target.mem_nhds (f.map_source h0), E] with z hz h'z
  simpa [hz] using h'z

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
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)
⊢ 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
this : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E)) ((p.leftInv i a).comp p) a
⊢ HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a

Tactic:
apply this.congr

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
this : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E)) ((p.leftInv i a).comp p) a
⊢ ⇑(ContinuousLinearMap.id 𝕜 E) =ᶠ[𝓝 a] ↑f.symm ∘ ↑f

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}
⊢ HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)

Tactic:
refine ⟨min r (p.leftInv i a).radius, min_le_right _ _,
  lt_min r_pos (radius_leftInv_pos_of_radius_pos h.radius_pos hp), fun {y} hy ↦ ?_⟩

Result:
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)
⊢ HasSum (fun n => (p.leftInv i a n) fun x => y) (↑f.symm (↑f a + y))

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))
⊢ ∀ᶠ (y : E) in 𝓝 (↑f.symm (↑f a)), HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) y

Tactic:
simp only [h0, PartialHomeomorph.left_inv]

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))
⊢ ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n => (p.leftInv i a n) fun x => ↑f y - ↑f a) y