-- Mathlib/Analysis/Meromorphic/Basic.lean
@[fun_prop]
lemma inv {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt f⁻¹ x

Proof state:
case h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z

Tactic:
rcases eq_or_ne z x with rfl | hz_ne

Result:
case h.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
m n : ℕ
g : 𝕜 → 𝕜
z : 𝕜
hg_ne' : g z ≠ 0
hf : AnalyticAt 𝕜 (fun z_1 => (z_1 - z) ^ m • f z_1) z
h_eq : ¬(fun z_1 => (z_1 - z) ^ m • f z_1) =ᶠ[𝓝 z] 0
hg_an : AnalyticAt 𝕜 g z
hg_ne : g z ≠ 0
hg_eq : ∀ᶠ (z_1 : 𝕜) in 𝓝 z, (z_1 - z) ^ m • f z_1 = (z_1 - z) ^ n • g z_1
this : AnalyticAt 𝕜 (fun z_1 => (z_1 - z) ^ (m + 1)) z
hfg : (z - z) ^ m • f z = (z - z) ^ n • g z
⊢ (z - z) ^ (m + 1) • g⁻¹ z = (z - z) ^ (n + 1) • f⁻¹ z

case h.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z

Proof state:
case h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : (fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : z ∈ {x}ᶜ
⊢ 0 = f⁻¹ z

Tactic:
rw [Pi.inv_apply, (smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz,
  inv_zero]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
⊢ MeromorphicAt f⁻¹ x

Tactic:
obtain ⟨n, g, hg_an, hg_ne, hg_eq⟩ := hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h_eq

Result:
case neg.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
⊢ MeromorphicAt f⁻¹ x

Proof state:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : (fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
⊢ (fun x => 0) =ᶠ[𝓝[≠] x] f⁻¹

Tactic:
rw [eventuallyEq_nhdsWithin_iff]

Result:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : (fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → 0 = f⁻¹ x_1

Proof state:
case neg.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
⊢ (fun x_1 => (x_1 - x) ^ (m + 1) • g⁻¹ x_1) =ᶠ[𝓝 x] fun z => (z - x) ^ (n + 1) • f⁻¹ z

Tactic:
filter_upwards [hg_eq, hg_an.continuousAt.eventually_ne hg_ne] with z hfg hg_ne'

Result:
case h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z

Proof state:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : (fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
⊢ MeromorphicAt f⁻¹ x

Tactic:
refine (MeromorphicAt.const 0 x).congr ?_

Result:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : (fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
⊢ (fun x => 0) =ᶠ[𝓝[≠] x] f⁻¹

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
⊢ MeromorphicAt f⁻¹ x

Tactic:
rcases hf with ⟨m, hf⟩

Result:
case intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
⊢ MeromorphicAt f⁻¹ x

Proof state:
case h.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m * f z = (z - x) ^ n * g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
⊢ (z - x) ^ (m + 1) * g⁻¹ z = (z - x) ^ (n + 1) * f⁻¹ z

Tactic:
have aux1 : f z ≠ 0 := by
  have : (z - x) ^ n * g z ≠ 0 := mul_ne_zero (pow_ne_zero _ (sub_ne_zero.mpr hz_ne)) hg_ne'
  rw [← hfg, mul_ne_zero_iff] at this
  exact this.2

Result:
case h.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m * f z = (z - x) ^ n * g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
aux1 : f z ≠ 0
⊢ (z - x) ^ (m + 1) * g⁻¹ z = (z - x) ^ (n + 1) * f⁻¹ z

Proof state:
case h.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z

Tactic:
simp_rw [smul_eq_mul] at hfg ⊢

Result:
case h.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m * f z = (z - x) ^ n * g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
⊢ (z - x) ^ (m + 1) * g⁻¹ z = (z - x) ^ (n + 1) * f⁻¹ z