-- Mathlib/Analysis/Meromorphic/Basic.lean
theorem eventually_analyticAt [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜}
    (h : MeromorphicAt f x) : ∀ᶠ y in 𝓝[≠] x, AnalyticAt 𝕜 f y

Proof state:
case intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Tactic:
refine (h.filter_mono ?_).mp ?_

Result:
case intro.refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ 𝓝[≠] x ≤ 𝓝 x

case intro.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Proof state:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ ∀ x_1 ∈ {x}ᶜ, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Tactic:
intro y hy hf

Result:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : y ∈ {x}ᶜ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y

Proof state:
case intro.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Tactic:
rw [eventually_nhdsWithin_iff]

Result:
case intro.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Proof state:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 (fun x_1 => (_root_.id - fun x_2 => x) x_1 ^ n)⁻¹ y
z : 𝕜
hz : z ≠ x
⊢ ((fun x_1 => (_root_.id - fun x_2 => x) x_1 ^ n)⁻¹ • fun z => (z - x) ^ n • f z) z = f z

Tactic:
simp [smul_smul, hz, sub_eq_zero]

Result:
no goals

Proof state:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 (fun x_1 => (_root_.id - fun x_2 => x) x_1 ^ n)⁻¹ y
⊢ AnalyticAt 𝕜 f y

Tactic:
apply (this.smul hf).congr ∘ (eventually_ne_nhds hy).mono

Result:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 (fun x_1 => (_root_.id - fun x_2 => x) x_1 ^ n)⁻¹ y
⊢ ∀ (x_1 : 𝕜), x_1 ≠ x → ((fun x_2 => (_root_.id - fun x_3 => x) x_2 ^ n)⁻¹ • fun z => (z - x) ^ n • f z) x_1 = f x_1

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : ∃ n, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Tactic:
obtain ⟨n, h⟩ := h

Result:
case intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Proof state:
case intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Tactic:
apply AnalyticAt.eventually_analyticAt at h

Result:
case intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Proof state:
case intro.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Tactic:
apply Filter.Eventually.of_forall

Result:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ ∀ x_1 ∈ {x}ᶜ, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Tactic:
rw [MeromorphicAt] at h

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : ∃ n, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Proof state:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 (fun x_1 => (_root_.id - fun x_2 => x) x_1 ^ n)⁻¹ y
⊢ ∀ (x_1 : 𝕜), x_1 ≠ x → ((fun x_2 => (_root_.id - fun x_3 => x) x_2 ^ n)⁻¹ • fun z => (z - x) ^ n • f z) x_1 = f x_1

Tactic:
intro z hz

Result:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 (fun x_1 => (_root_.id - fun x_2 => x) x_1 ^ n)⁻¹ y
z : 𝕜
hz : z ≠ x
⊢ ((fun x_1 => (_root_.id - fun x_2 => x) x_1 ^ n)⁻¹ • fun z => (z - x) ^ n • f z) z = f z