-- Mathlib/Analysis/Meromorphic/Order.lean
/-- Compatibility of notions of `order` for analytic and meromorphic functions. -/
lemma _root_.AnalyticAt.meromorphicAt_order {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) :
    hf.meromorphicAt.order = hf.order.map (↑)

Proof state:
case inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order ≠ ⊤
n : ℕ
hn : ↑n = hf.order
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
rcases (hf.order_eq_nat_iff _).mp hn.symm with ⟨g, h1, h2, h3⟩

Result:
case inr.intro.intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order ≠ ⊤
n : ℕ
hn : ↑n = hf.order
g : 𝕜 → E
h1 : AnalyticAt 𝕜 g x
h2 : g x ≠ 0
h3 : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ n • g z
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Proof state:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order ≠ ⊤
⊢ ⋯.order = ENat.map Nat.cast hf.order

Tactic:
obtain ⟨n, hn⟩ := ENat.ne_top_iff_exists.mp ho

Result:
case inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order ≠ ⊤
n : ℕ
hn : ↑n = hf.order
⊢ ⋯.order = ENat.map Nat.cast hf.order

Proof state:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order = ⊤
⊢ ⋯.order = ENat.map Nat.cast hf.order

Tactic:
rw [ho, ENat.map_top, order_eq_top_iff]

Result:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Proof state:
case inr.intro.intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order ≠ ⊤
n : ℕ
hn : ↑n = hf.order
g : 𝕜 → E
h1 : AnalyticAt 𝕜 g x
h2 : g x ≠ 0
h3 : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ n • g z
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
exact ⟨g, h1, h2, h3.filter_mono nhdsWithin_le_nhds⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ ⋯.order = ENat.map Nat.cast hf.order

Tactic:
rcases eq_or_ne hf.order ⊤ with ho | ho

Result:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order = ⊤
⊢ ⋯.order = ENat.map Nat.cast hf.order

case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order ≠ ⊤
⊢ ⋯.order = ENat.map Nat.cast hf.order

Proof state:
case inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order ≠ ⊤
n : ℕ
hn : ↑n = hf.order
⊢ ⋯.order = ENat.map Nat.cast hf.order

Tactic:
simp_rw [← hn, ENat.map_coe, order_eq_int_iff, zpow_natCast]

Result:
case inr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order ≠ ⊤
n : ℕ
hn : ↑n = hf.order
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Proof state:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
ho : hf.order = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
exact (hf.order_eq_top_iff.mp ho).filter_mono nhdsWithin_le_nhds

Result:
no goals