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

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, PartialHomeomorph.left_inv]
  filter_upwards [C, f.open_source.mem_nhds h0] with x hx h'x
  simpa [h'x] using hx

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

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

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)
⊢ 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)
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‖ₑ < r ∧ ‖y‖ₑ < (p.leftInv i a).radius
⊢ ‖y‖ₑ < r

Tactic:
exact hy.1

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

Tactic:
have : ContinuousAt (fun x ↦ x - a) a := by fun_prop

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)))
this : ContinuousAt (fun x => x - a) a
⊢ ∀ᶠ (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 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

Tactic:
simpa [h'x] using hx

Result:
no goals