CH2.meromorphicOrderAt_starRingEnd

lemma meromorphicOrderAt_starRingEnd {F : ℂ → ℂ} {z : ℂ}    (hF_symm : ConjSymm F ∨ ConjAntisymm F) :    meromorphicOrderAt F z = meromorphicOrderAt F (starRingEnd ℂ z) := by  rcases hF_symm with hF | hF  · have hreflect : conj_reflect F =ᶠ[nhdsWithin (starRingEnd ℂ z) {(starRingEnd ℂ z)}ᶜ] F := by      apply Filter.Eventually.of_forall      intro w      dsimp [conj_reflect]      simpa [starRingEnd_self_apply] using congrArg (starRingEnd ℂ) (hF w)    calc      meromorphicOrderAt F z = meromorphicOrderAt (conj_reflect F) (starRingEnd ℂ z) := by        symm        exact meromorphicOrderAt_conj_reflect (G := F) (a := z)      _ = meromorphicOrderAt F (starRingEnd ℂ z) := meromorphicOrderAt_congr hreflect  · have hreflect_neg : conj_reflect F =ᶠ[nhdsWithin (starRingEnd ℂ z) {(starRingEnd ℂ z)}ᶜ] -F := by      apply Filter.Eventually.of_forall      intro w      dsimp [conj_reflect]      simpa [starRingEnd_self_apply] using congrArg (starRingEnd ℂ) (hF w)    have h_neg_order :        meromorphicOrderAt (-F) (starRingEnd ℂ z) = meromorphicOrderAt F (starRingEnd ℂ z) := by      have hneg_eq : -F = (fun _ : ℂ ↦ (-1 : ℂ)) * F := by        ext w        simp      rw [hneg_eq]      exact meromorphicOrderAt_mul_of_ne_zero        (f := F) (g := fun _ : ℂ ↦ (-1 : ℂ))        (show AnalyticAt ℂ (fun _ : ℂ ↦ (-1 : ℂ)) (starRingEnd ℂ z) from analyticAt_const)        (by simp)    calc      meromorphicOrderAt F z = meromorphicOrderAt (conj_reflect F) (starRingEnd ℂ z) := by        symm        exact meromorphicOrderAt_conj_reflect (G := F) (a := z)      _ = meromorphicOrderAt (-F) (starRingEnd ℂ z) := meromorphicOrderAt_congr hreflect_neg      _ = meromorphicOrderAt F (starRingEnd ℂ z) := h_neg_order