-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
/-- 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

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
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

Tactic:
wlog h_le : n ≤ m generalizing m n

Result:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
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
this :
  ∀ {m n : ℤ},
    (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z) →
      (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z) → n ≤ m → m = n
h_le : ¬n ≤ m
⊢ m = n

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
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
h_le : n ≤ m
⊢ m = n

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
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
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x = (x - z₀) ^ m • g x
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x = (x - z₀) ^ n • j x
hj_ne : m ≠ n
z : 𝕜
hfz : z ∈ {z₀}ᶜ → j z = (z - z₀) ^ (m - n) • g z
hfz' : z ∈ {z₀}ᶜ → f z = (z - z₀) ^ n • j z
hz : z ∈ {z₀}ᶜ
⊢ j z = (z - z₀) ^ (m - n) • g z

Tactic:
exact hfz hz

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
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
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
⊢ j z₀ = 0

Tactic:
rw [frequently_eq_iff_eventually_eq hj_an] at this

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
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
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∀ᶠ (z : 𝕜) in 𝓝 z₀, j z = (z - z₀) ^ (m - n) • g z
⊢ j z₀ = 0

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
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
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
⊢ AnalyticAt 𝕜 (fun z => (z - z₀) ^ (m - n) • g z) z₀