Log Deriv Residue

theorem logDerivResidue' {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ}    (U_is_open : IsOpen U)    (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0)    (holc : HolomorphicOn f (U \ {p}))    (U_in_nhds : U ∈ 𝓝 p) {A : ℂ} (A_ne_zero : A ≠ 0)    (f_near_p : BddAbove (norm ∘ (f - fun s ↦ A * (s - p)⁻¹) '' (U \ {p}))) :    (deriv f * f⁻¹ + (fun s ↦ (s - p)⁻¹)) =O[𝓝[≠] p] (1 : ℂ → ℂ) := by    have simpleHolo : HolomorphicOn (fun s ↦ A / (s - p)) (U \ {p}) := by    apply DifferentiableOn.mono (t := {p}ᶜ)    · apply DifferentiableOn.div      · exact differentiableOn_const _      · exact DifferentiableOn.sub differentiableOn_id (differentiableOn_const _)      · exact fun x hx => by rw [sub_ne_zero]; exact hx    · rintro s ⟨_, hs⟩ ; exact hs   have f_minus_pole_is_holomorphic : HolomorphicOn (f - (fun s ↦ A * (s - p)⁻¹)) (U \ {p}) := by    exact (DifferentiableOn.sub_iff_right holc).mpr simpleHolo   let ⟨g, ⟨g_is_holomorphic, g_is_f_minus_pole⟩⟩ := existsDifferentiableOn_of_bddAbove    U_in_nhds f_minus_pole_is_holomorphic f_near_p       /- TODO: Assert that the derivatives match too -/   let h := (fun _ ↦ A) + g * (fun (s : ℂ) ↦ (s - p))    have linear_is_holomorphic : HolomorphicOn (fun (s : ℂ ) ↦ (s - p)) U := by    exact DifferentiableOn.sub_const differentiableOn_id p   have h_is_holomorphic : HolomorphicOn h U := by    have T := DifferentiableOn.mul g_is_holomorphic linear_is_holomorphic    exact DifferentiableOn.const_add A T   have h_continuous : ContinuousOn h U :=    by exact DifferentiableOn.continuousOn h_is_holomorphic   have deriv_h_identity : ∀x ∈ (U \ {p}), (deriv h) x = f x + (deriv f x) * (x - p) := by    intro x x_in_u_not_p    have x_in_u : x ∈ U := by exact Set.mem_of_mem_sdiff x_in_u_not_p    have x_not_p : x ≠ p := by      exact ((Set.mem_sdiff x).mp x_in_u_not_p).2     have weird : U ∈ 𝓝 x := by      exact IsOpen.mem_nhds (U_is_open) (x_in_u)     rw [derivative_const_plus_product, ← g_is_f_minus_pole x_in_u_not_p,      ← deriv_eqOn_of_eqOn_punctured _ _ U p U_is_open g_is_f_minus_pole x_in_u_not_p,      deriv_f_minus_A_inv_sub_clean]    · simp only [Pi.sub_apply]      have := sub_ne_zero_of_ne x_not_p      field_simp      ring    · apply holc.differentiableAt      exact Filter.inter_mem weird <| compl_singleton_mem_nhds x_not_p    · exact x_not_p    · exact g_is_holomorphic.differentiableAt weird  have h_identity : ∀x ∈ (U \ {p}), h x = (f x) * (x - p)  := by    intro x x_in_u_not_p    have hyp_x_not_p : x ≠ p := by      exact ((Set.mem_sdiff x).mp x_in_u_not_p).2    simp only [h, Pi.add_apply, Pi.mul_apply]    rw [← g_is_f_minus_pole x_in_u_not_p]    simp only [Pi.sub_apply]    field [sub_ne_zero.mpr hyp_x_not_p]  have log_deriv_f_plus_pole_equal_log_deriv_h :      EqOn (deriv f * f⁻¹ + fun s ↦ (s - p)⁻¹) ((deriv h) * h⁻¹) (U \ {p}) := by    simp only [Set.mem_sdiff, mem_singleton_iff, ne_eq, and_imp, Function.comp_apply, Pi.sub_apply,      DifferentiableOn.sub_iff_right, differentiableOn_const, DifferentiableOn.fun_sub_iff_left,      holc] at *    intro x hyp_x    have x_not_p : x ≠ p := by      exact ((Set.mem_sdiff x).mp hyp_x).2    have x_in_u : x ∈ U := by exact Set.mem_of_mem_sdiff hyp_x    simp only [Pi.add_apply, Pi.mul_apply, Pi.inv_apply]    rw [deriv_h_identity _ x_in_u x_not_p, h_identity _ x_in_u x_not_p]     /- This is just an identity at this point -/    field [sub_ne_zero.mpr x_not_p, non_zero x (x_in_u) x_not_p]  have h_inv_bounded :      h⁻¹ =O[𝓝[≠] p] (1 : ℂ → ℂ) := by    have : ContinuousAt h⁻¹ p := by      apply ContinuousOn.continuousAt h_continuous U_in_nhds |>.inv₀      simp [h, A_ne_zero]    exact Asymptotics.IsBigO.mono (this.norm.isBoundedUnder_le.isBigO_one ℂ) inf_le_left   have h_deriv_bounded :        (deriv h) =O[𝓝[≠] p] (1 : ℂ → ℂ) :=          analytic_deriv_bounded_near_point h U_is_open            (by exact mem_of_mem_nhds U_in_nhds) h_is_holomorphic    have h_log_deriv_bounded :    ((deriv h) * h⁻¹) =O[𝓝[≠] p] (1 : ℂ → ℂ)  := by      have T := Asymptotics.IsBigO.mul h_deriv_bounded h_inv_bounded      exact IsBigO.of_const_mul_right T   have u_not_p_in_filter : U \ {p} ∈ 𝓝[≠] p := by    exact sdiff_mem_nhdsWithin_compl U_in_nhds {p}  have T := Set.EqOn.eventuallyEq_of_mem log_deriv_f_plus_pole_equal_log_deriv_h u_not_p_in_filter  exact EventuallyEq.trans_isBigO T h_log_deriv_bounded