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

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
⊢ MeromorphicAt f⁻¹ x

Tactic:
refine ⟨n + 1, (this.smul' <| hg_an.inv hg_ne).congr ?_⟩

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

Proof state:
𝕜 : 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
this : (z - x) ^ n * g z ≠ 0
⊢ f z ≠ 0

Tactic:
rw [← hfg, mul_ne_zero_iff] at this

Result:
𝕜 : 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
this : (z - x) ^ m ≠ 0 ∧ f z ≠ 0
⊢ f z ≠ 0

Proof state:
𝕜 : 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
⊢ f z ≠ 0

Tactic:
have : (z - x) ^ n * g z ≠ 0 := mul_ne_zero (pow_ne_zero _ (sub_ne_zero.mpr hz_ne)) hg_ne'

Result:
𝕜 : 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
this : (z - x) ^ n * g z ≠ 0
⊢ f z ≠ 0

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
aux1 : f z ≠ 0
⊢ (z - x) * ((z - x) ^ n * g z) = (z - x) ^ (n + 1) * g z

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : 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
this : (z - x) ^ m ≠ 0 ∧ f z ≠ 0
⊢ f z ≠ 0

Tactic:
exact this.2

Result:
no goals

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
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → 0 = f⁻¹ x_1

Tactic:
filter_upwards [h_eq] with z hfz hz

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
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : z ∈ {x}ᶜ
⊢ 0 = 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
aux1 : f z ≠ 0
⊢ (z - x) ^ (m + 1) * g⁻¹ z = (z - x) ^ (n + 1) * f⁻¹ z

Tactic:
field_simp [sub_ne_zero.mpr hz_ne]

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) * f z = (z - x) ^ (n + 1) * g z

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
⊢ MeromorphicAt f⁻¹ x

Tactic:
have : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + 1)) x :=
  (analyticAt_id.sub analyticAt_const).pow _

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
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
⊢ MeromorphicAt f⁻¹ x

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

Tactic:
by_cases h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0

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
⊢ MeromorphicAt f⁻¹ x

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

Proof state:
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

Tactic:
simp only [sub_self, pow_succ, mul_zero, zero_smul]

Result:
no goals