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

Tactic:
simp [hx]

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

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)

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

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

Tactic:
have : y + f a ∈ EMetric.ball (f a) r := by
  simp only [EMetric.mem_ball, edist_eq_enorm_sub, sub_zero, lt_min_iff,
    add_sub_cancel_right] at hy ⊢
  exact hy.1

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

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
⊢ HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((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

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

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

Result:
case h
𝕜 : 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))
x : E
hx : HasSum (fun n => (p.leftInv i a n) fun x_1 => ↑f x - ↑f a) (↑f.symm (↑f x))
h'x : x ∈ f.source
⊢ HasSum (fun n => (p.leftInv i a n) fun x_1 => ↑f x - ↑f a) x