Kadiri.zeroImagSquareTailSummable_of_dyadic_shell_source

theorem zeroImagSquareTailSummable_of_dyadic_shell_source    (hshell : zeroImagDyadicShellSummableSource) :    zeroImagSquareTailSummable := by  unfold zeroImagDyadicShellSummableSource at hshell  have hhigh : Summable      (fun rho : {rho : NontrivialZeros // 1 ≤ |(rho : ℂ).im|} =>        zeroImagSquareTail rho.1) := by    simpa [Function.comp_def, highZeroToDyadicShell] using      hshell.comp_injective highZeroToDyadicShell_injective  have hlow_set : ({rho : NontrivialZeros | ¬ 1 ≤ |(rho : ℂ).im|} :      Set NontrivialZeros).Finite := by    apply Set.Finite.subset nontrivialZeros_abs_im_lt_one_finite    intro rho hrho    rw [Set.mem_setOf_eq] at hrho ⊢    exact lt_of_not_ge hrho  haveI : Finite {rho : NontrivialZeros // ¬ 1 ≤ |(rho : ℂ).im|} :=    Set.finite_coe_iff.mpr hlow_set  have hlow : Summable      (fun rho : {rho : NontrivialZeros // ¬ 1 ≤ |(rho : ℂ).im|} =>        zeroImagSquareTail rho.1) := by    exact Summable.of_finite  unfold zeroImagSquareTailSummable  exact (summable_subtype_and_compl    (s := {rho : NontrivialZeros | 1 ≤ |(rho : ℂ).im|})).mp ⟨hhigh, hlow⟩