diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index 50876c0aad50f..246ecea1729a2 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -148,11 +148,13 @@ theorem frequently_eq_iff_eventually_eq (hf : AnalyticAt 𝕜 f z₀) (hg : Anal
   simpa [sub_eq_zero] using frequently_zero_iff_eventually_zero (hf.sub hg)
 #align analytic_at.frequently_eq_iff_eventually_eq AnalyticAt.frequently_eq_iff_eventually_eq
 
-/-- There exists at most one `n` such that locally around `z₀` we have `f z = (z - z₀) ^ n • g z`,
-with `g` analytic and nonvanishing at `z₀`. -/
-lemma unique_eventuallyEq_pow_smul_nonzero {m n : ℕ}
-    (hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ m • g z)
-    (hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ n • g z) :
+/-- For a function `f` on `𝕜`, and `z₀ ∈ 𝕜`, there exists at most one `n` such that on a punctured
+neighbourhood of `z₀` we have `f z = (z - z₀) ^ n • g z`, with `g` analytic and nonvanishing at
+`z₀`. We formulate this with `n : ℤ`, and deduce the case `n : ℕ` later, for applications to
+meromorphic functions. -/
+lemma unique_eventuallyEq_zpow_smul_nonzero {m n : ℤ}
+    (hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z)
+    (hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z) :
     m = n := by
   wlog h_le : n ≤ m generalizing m n
   · exact ((this hn hm) (not_le.mp h_le).le).symm
@@ -160,14 +162,28 @@ lemma unique_eventuallyEq_pow_smul_nonzero {m n : ℕ}
   let ⟨j, hj_an, hj_ne, hj_eq⟩ := hn
   contrapose! hj_ne
   have : ∃ᶠ z in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
-  · refine (eventually_nhdsWithin_iff.mpr ?_).frequently
+  · apply Filter.Eventually.frequently
+    rw [eventually_nhdsWithin_iff] at hg_eq hj_eq ⊢
     filter_upwards [hg_eq, hj_eq] with z hfz hfz' hz
-    rwa [← Nat.add_sub_cancel' h_le, pow_add, mul_smul, hfz', smul_right_inj] at hfz
-    exact pow_ne_zero _ <| sub_ne_zero.mpr hz
+    rw [← add_sub_cancel' n m, add_sub_assoc, zpow_add₀ <| sub_ne_zero.mpr hz, mul_smul,
+      hfz' hz, smul_right_inj <| zpow_ne_zero _ <| sub_ne_zero.mpr hz] at hfz
+    exact hfz hz
   rw [frequently_eq_iff_eventually_eq hj_an] at this
-  rw [EventuallyEq.eq_of_nhds this, sub_self, zero_pow, zero_smul]
-  · apply Nat.sub_ne_zero_of_lt (h_le.lt_of_ne' hj_ne)
-  · exact (((analyticAt_id 𝕜 _).sub analyticAt_const).pow _).smul hg_an
+  rw [EventuallyEq.eq_of_nhds this, sub_self, zero_zpow _ (sub_ne_zero.mpr hj_ne), zero_smul]
+  conv => enter [2, z, 1]; rw [← Int.toNat_sub_of_le h_le, zpow_ofNat]
+  exact (((analyticAt_id _ _).sub analyticAt_const).pow _).smul hg_an
+
+/-- For a function `f` on `𝕜`, and `z₀ ∈ 𝕜`, there exists at most one `n` such that on a
+neighbourhood of `z₀` we have `f z = (z - z₀) ^ n • g z`, with `g` analytic and nonvanishing at
+`z₀`. -/
+lemma unique_eventuallyEq_pow_smul_nonzero {m n : ℕ}
+    (hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ m • g z)
+    (hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ n • g z) :
+    m = n := by
+  simp_rw [← zpow_ofNat] at hm hn
+  exact Int.ofNat_inj.mp <| unique_eventuallyEq_zpow_smul_nonzero
+    (let ⟨g, h₁, h₂, h₃⟩ := hm; ⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)
+    (let ⟨g, h₁, h₂, h₃⟩ := hn; ⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)
 
 /-- If `f` is analytic at `z₀`, then exactly one of the following two possibilities occurs: either
 `f` vanishes identically near `z₀`, or locally around `z₀` it has the form `z ↦ (z - z₀) ^ n • g z`
diff --git a/Mathlib/Analysis/Analytic/Meromorphic.lean b/Mathlib/Analysis/Analytic/Meromorphic.lean
index dc33af45cce31..a81ee1665f3e9 100644
--- a/Mathlib/Analysis/Analytic/Meromorphic.lean
+++ b/Mathlib/Analysis/Analytic/Meromorphic.lean
@@ -7,8 +7,17 @@ import Mathlib.Analysis.Analytic.IsolatedZeros
 
 /-!
 # Meromorphic functions
+
+Main statements:
+
+* `MeromorphicAt`: definition of meromorphy at a point
+* `MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt`: `f` is meromorphic at `z₀` iff we have
+  `f z = (z - z₀) ^ n • g z` on a punctured nhd of `z₀`, for some `n : ℤ` and `g` analytic at z₀.
+* `MeromorphicAt.order`: order of vanishing at `z₀`, as an element of `ℤ ∪ {∞}`
 -/
 
+open Filter
+
 open scoped Topology
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
@@ -23,12 +32,12 @@ lemma AnalyticAt.meromorphicAt {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜
     MeromorphicAt f x :=
   ⟨0, by simpa only [pow_zero, one_smul]⟩
 
-lemma meromorphicAt_id (x : 𝕜) : MeromorphicAt id x := (analyticAt_id 𝕜 x).meromorphicAt
+namespace MeromorphicAt
 
-lemma meromorphicAt_const (e : E) (x : 𝕜) : MeromorphicAt (fun _ ↦ e) x :=
-  analyticAt_const.meromorphicAt
+lemma id (x : 𝕜) : MeromorphicAt id x := (analyticAt_id 𝕜 x).meromorphicAt
 
-namespace MeromorphicAt
+lemma const (e : E) (x : 𝕜) : MeromorphicAt (fun _ ↦ e) x :=
+  analyticAt_const.meromorphicAt
 
 lemma add {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (f + g) x := by
@@ -57,7 +66,7 @@ lemma mul {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : Meromo
   hf.smul hg
 
 lemma neg {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt (-f) x := by
-  convert (meromorphicAt_const (-1 : 𝕜) x).smul hf using 1
+  convert (MeromorphicAt.const (-1 : 𝕜) x).smul hf using 1
   ext1 z
   simp only [Pi.neg_apply, Pi.smul_apply', neg_smul, one_smul]
 
@@ -90,7 +99,7 @@ lemma inv {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicA
   rcases hf with ⟨m, hf⟩
   by_cases h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
   · -- silly case: f locally 0 near x
-    apply (meromorphicAt_const 0 x).congr
+    refine (MeromorphicAt.const 0 x).congr ?_
     rw [eventuallyEq_nhdsWithin_iff]
     filter_upwards [h_eq] with z hfz hz
     rw [Pi.inv_apply, (smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz,
@@ -122,4 +131,140 @@ lemma div {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : Meromo
     MeromorphicAt (f / g) x :=
   (div_eq_mul_inv f g).symm ▸ (hf.mul hg.inv)
 
+lemma pow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℕ) : MeromorphicAt (f ^ n) x := by
+  induction' n with m hm
+  · simpa only [Nat.zero_eq, pow_zero] using MeromorphicAt.const 1 x
+  · simpa only [pow_succ'] using hm.mul hf
+
+lemma zpow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : MeromorphicAt (f ^ n) x := by
+  induction' n with m m
+  · simpa only [Int.ofNat_eq_coe, zpow_ofNat] using hf.pow m
+  · simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)
+
+/-- The order of vanishing of a meromorphic function, as an element of `ℤ ∪ ∞` (to include the
+case of functions identically 0 near `x`). -/
+noncomputable def order {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : WithTop ℤ :=
+  (hf.choose_spec.order.map (↑· : ℕ → ℤ)) - hf.choose
+
+lemma order_eq_top_iff {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) :
+    hf.order = ⊤ ↔ ∀ᶠ z in 𝓝[≠] x, f z = 0 := by
+  unfold order
+  by_cases h : hf.choose_spec.order = ⊤
+  · rw [h, WithTop.map_top, ← WithTop.coe_nat,
+      WithTop.top_sub_coe, eq_self, true_iff, eventually_nhdsWithin_iff]
+    rw [AnalyticAt.order_eq_top_iff] at h
+    filter_upwards [h] with z hf hz
+    rwa [smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)] at hf
+  · obtain ⟨m, hm⟩ := WithTop.ne_top_iff_exists.mp h
+    rw [← hm, WithTop.map_coe, WithTop.sub_eq_top_iff, eq_false_intro WithTop.coe_ne_top,
+      false_and, false_iff, eventually_nhdsWithin_iff]
+    contrapose! h
+    rw [AnalyticAt.order_eq_top_iff]
+    rw [← hf.choose_spec.frequently_eq_iff_eventually_eq analyticAt_const]
+    apply Eventually.frequently
+    rw [eventually_nhdsWithin_iff]
+    filter_upwards [h] with z hfz hz
+    rw [hfz hz, smul_zero]
+
+lemma order_eq_int_iff {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : hf.order = n ↔
+    ∃ g : 𝕜 → E, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ z in 𝓝[≠] x, f z = (z - x) ^ n • g z := by
+  unfold order
+  by_cases h : hf.choose_spec.order = ⊤
+  · rw [h, WithTop.map_top, ← WithTop.coe_nat, WithTop.top_sub_coe,
+      eq_false_intro WithTop.top_ne_coe, false_iff]
+    rw [AnalyticAt.order_eq_top_iff] at h
+    refine fun ⟨g, hg_an, hg_ne, hg_eq⟩ ↦ hg_ne ?_
+    apply EventuallyEq.eq_of_nhds
+    rw [EventuallyEq, ← AnalyticAt.frequently_eq_iff_eventually_eq hg_an analyticAt_const]
+    apply Eventually.frequently
+    rw [eventually_nhdsWithin_iff] at hg_eq ⊢
+    filter_upwards [h, hg_eq] with z hfz hfz_eq hz
+    rwa [hfz_eq hz, ← mul_smul, smul_eq_zero_iff_right] at hfz
+    exact mul_ne_zero (pow_ne_zero _ (sub_ne_zero.mpr hz)) (zpow_ne_zero _ (sub_ne_zero.mpr hz))
+  · obtain ⟨m, h⟩ := WithTop.ne_top_iff_exists.mp h
+    rw [← h, WithTop.map_coe, ← WithTop.coe_nat, ← WithTop.coe_sub, WithTop.coe_inj]
+    obtain ⟨g, hg_an, hg_ne, hg_eq⟩ := (AnalyticAt.order_eq_nat_iff _ _).mp h.symm
+    replace hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ (↑m - ↑hf.choose : ℤ) • g z
+    · rw [eventually_nhdsWithin_iff]
+      filter_upwards [hg_eq] with z hg_eq hz
+      rwa [← smul_right_inj <| zpow_ne_zero _ (sub_ne_zero.mpr hz), ← mul_smul,
+      ← zpow_add₀ (sub_ne_zero.mpr hz), ← add_sub_assoc, add_sub_cancel', zpow_ofNat, zpow_ofNat]
+    exact ⟨fun h ↦ ⟨g, hg_an, hg_ne, h ▸ hg_eq⟩,
+      AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero ⟨g, hg_an, hg_ne, hg_eq⟩⟩
+
+/-- 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 (↑) := by
+  rcases eq_or_ne hf.order ⊤ with ho | ho
+  · rw [ho, WithTop.map_top, order_eq_top_iff]
+    exact (hf.order_eq_top_iff.mp ho).filter_mono nhdsWithin_le_nhds
+  · obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp ho
+    simp_rw [← hn, WithTop.map_coe, order_eq_int_iff, zpow_ofNat]
+    rcases (hf.order_eq_nat_iff _).mp hn.symm with ⟨g, h1, h2, h3⟩
+    exact ⟨g, h1, h2, h3.filter_mono nhdsWithin_le_nhds⟩
+
+lemma iff_eventuallyEq_zpow_smul_analyticAt {f : 𝕜 → E} {x : 𝕜} : MeromorphicAt f x ↔
+    ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ z in 𝓝[≠] x, f z = (z - x) ^ n • g z := by
+  refine ⟨fun ⟨n, hn⟩ ↦ ⟨-n, _, ⟨hn, eventually_nhdsWithin_iff.mpr ?_⟩⟩, ?_⟩
+  · filter_upwards with z hz
+    rw [← mul_smul, ← zpow_ofNat, ← zpow_add₀ (sub_ne_zero.mpr hz), add_left_neg,
+      zpow_zero, one_smul]
+  · refine fun ⟨n, g, hg_an, hg_eq⟩ ↦ MeromorphicAt.congr ?_ (EventuallyEq.symm hg_eq)
+    exact (((MeromorphicAt.id x).sub (.const _ x)).zpow _).smul hg_an.meromorphicAt
+
 end MeromorphicAt
+
+/-- Meromorphy of a function on a set. -/
+def MeromorphicOn (f : 𝕜 → E) (U : Set 𝕜) : Prop := ∀ x ∈ U, MeromorphicAt f x
+
+lemma AnalyticOn.meromorphicOn {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOn 𝕜 f U) :
+    MeromorphicOn f U :=
+  fun x hx ↦ (hf x hx).meromorphicAt
+
+
+namespace MeromorphicOn
+
+variable {s t : 𝕜 → 𝕜} {f g : 𝕜 → E} {U : Set 𝕜}
+  (hs : MeromorphicOn s U) (ht : MeromorphicOn t U)
+  (hf : MeromorphicOn f U) (hg : MeromorphicOn g U)
+
+lemma id {U : Set 𝕜} : MeromorphicOn id U := fun x _ ↦ .id x
+
+lemma const (e : E) {U : Set 𝕜} : MeromorphicOn (fun _ ↦ e) U :=
+  fun x _ ↦ .const e x
+
+section arithmetic
+
+lemma mono_set {V : Set 𝕜} (hv : V ⊆ U) : MeromorphicOn f V := fun x hx ↦ hf x (hv hx)
+
+lemma add : MeromorphicOn (f + g) U := fun x hx ↦ (hf x hx).add (hg x hx)
+
+lemma sub : MeromorphicOn (f - g) U := fun x hx ↦ (hf x hx).sub (hg x hx)
+
+lemma neg : MeromorphicOn (-f) U := fun x hx ↦ (hf x hx).neg
+
+@[simp] lemma neg_iff : MeromorphicOn (-f) U ↔ MeromorphicOn f U :=
+  ⟨fun h ↦ by simpa only [neg_neg] using h.neg, neg⟩
+
+lemma smul : MeromorphicOn (s • f) U := fun x hx ↦ (hs x hx).smul (hf x hx)
+
+lemma mul : MeromorphicOn (s * t) U := fun x hx ↦ (hs x hx).mul (ht x hx)
+
+lemma inv : MeromorphicOn s⁻¹ U := fun x hx ↦ (hs x hx).inv
+
+@[simp] lemma inv_iff : MeromorphicOn s⁻¹ U ↔ MeromorphicOn s U :=
+  ⟨fun h ↦ by simpa only [inv_inv] using h.inv, inv⟩
+
+lemma div : MeromorphicOn (s / t) U := fun x hx ↦ (hs x hx).div (ht x hx)
+
+lemma pow (n : ℕ) : MeromorphicOn (s ^ n) U := fun x hx ↦ (hs x hx).pow _
+
+lemma zpow (n : ℤ) : MeromorphicOn (s ^ n) U := fun x hx ↦ (hs x hx).zpow _
+
+end arithmetic
+
+lemma congr (h_eq : Set.EqOn f g U) (hu : IsOpen U) : MeromorphicOn g U := by
+  refine fun x hx ↦ (hf x hx).congr (EventuallyEq.filter_mono ?_ nhdsWithin_le_nhds)
+  exact eventually_of_mem (hu.mem_nhds hx) h_eq
+
+end MeromorphicOn