Kadiri.meromorphicOrderAt_eq_neg_one_of_sub_principal_isBigO_one

lemma meromorphicOrderAt_eq_neg_one_of_sub_principal_isBigO_one    {f : ℂ → ℂ} {p c : ℂ}    (hf : MeromorphicAt f p) (hc : c ≠ 0)    (h : (f - fun z : ℂ => c / (z - p)) =O[𝓝[≠] p] (1 : ℂ → ℂ)) :    meromorphicOrderAt f p = (-1 : ℤ) := by  let principal : ℂ → ℂ := fun z => c / (z - p)  let rem : ℂ → ℂ := f - principal  have hconst_mero : MeromorphicAt (fun _ : ℂ => c) p := MeromorphicAt.const c p  have hlin_mero : MeromorphicAt (fun z : ℂ => z - p) p := by fun_prop  have hprincipal_mero : MeromorphicAt principal p := hconst_mero.div hlin_mero  have hrem_mero : MeromorphicAt rem p := hf.sub hprincipal_mero  have hrem_nonneg : 0 ≤ meromorphicOrderAt rem p :=    meromorphicOrderAt_nonneg_of_isBigO_one hrem_mero (by simpa [rem, principal] using h)  have hprincipal_order : meromorphicOrderAt principal p = (-1 : ℤ) := by    dsimp [principal]    change meromorphicOrderAt ((fun _ : ℂ => c) / fun z : ℂ => z - p) p = (-1 : ℤ)    rw [meromorphicOrderAt_div hconst_mero hlin_mero, meromorphicOrderAt_const,      if_neg hc, meromorphicOrderAt_id_sub_const]    norm_num  have hlt : meromorphicOrderAt principal p < meromorphicOrderAt rem p := by    rw [hprincipal_order]    exact lt_of_lt_of_le (WithTop.coe_lt_coe.2 (by norm_num : (-1 : ℤ) < 0)) hrem_nonneg  have hsum_order :      meromorphicOrderAt (principal + rem) p = meromorphicOrderAt principal p :=    meromorphicOrderAt_add_eq_left_of_lt hrem_mero hlt  have hcongr : f =ᶠ[𝓝[≠] p] principal + rem := by    filter_upwards with z    dsimp [principal, rem]    ring  calc    meromorphicOrderAt f p = meromorphicOrderAt (principal + rem) p :=      meromorphicOrderAt_congr hcongr    _ = meromorphicOrderAt principal p := hsum_order    _ = (-1 : ℤ) := hprincipal_order