Kadiri.zeroSquareTail_shift_le_four_zero

lemma zeroSquareTail_shift_le_four_zero {s : ℂ} {rho : NontrivialZeros}    (hlarge : 2 * ‖s‖ ≤ ‖(rho : ℂ)‖) :    zeroSquareTail s rho ≤ 4 * zeroSquareTail 0 rho := by  have hrho : (rho : ℂ) ≠ 0 := nontrivialZero_ne_zero rho  have hrho_norm_pos : 0 < ‖(rho : ℂ)‖ := norm_pos_iff.mpr hrho  have hhalf_pos : 0 < ‖(rho : ℂ)‖ / 2 := half_pos hrho_norm_pos  have hs_le_half : ‖s‖ ≤ ‖(rho : ℂ)‖ / 2 := by nlinarith  have hhalf_le_sub : ‖(rho : ℂ)‖ / 2 ≤ ‖(rho : ℂ)‖ - ‖s‖ := by    nlinarith  have hrev : ‖(rho : ℂ)‖ - ‖s‖ ≤ ‖(rho : ℂ) - s‖ :=    norm_sub_norm_le (rho : ℂ) s  have hhalf_le_w : ‖(rho : ℂ)‖ / 2 ≤ ‖s - (rho : ℂ)‖ := by    exact le_trans hhalf_le_sub (by simpa [norm_sub_rev] using hrev)  have hinv : ‖s - (rho : ℂ)‖⁻¹ ≤ (‖(rho : ℂ)‖ / 2)⁻¹ :=    inv_anti₀ hhalf_pos hhalf_le_w  have hinv_eq : (‖(rho : ℂ)‖ / 2)⁻¹ = 2 * ‖(rho : ℂ)‖⁻¹ := by    field_simp [norm_ne_zero_iff.mpr hrho]  have hinv_bound : ‖s - (rho : ℂ)‖⁻¹ ≤ 2 * ‖(rho : ℂ)‖⁻¹ := by    simpa [hinv_eq] using hinv  have hinv_nonneg : 0 ≤ ‖s - (rho : ℂ)‖⁻¹ :=    inv_nonneg.mpr (norm_nonneg _)  have hpow :      ‖s - (rho : ℂ)‖⁻¹ ^ (2 : ℕ) ≤        (2 * ‖(rho : ℂ)‖⁻¹) ^ (2 : ℕ) :=    pow_le_pow_left₀ hinv_nonneg hinv_bound 2  have hpow_eq :      (2 * ‖(rho : ℂ)‖⁻¹) ^ (2 : ℕ) =        4 * ‖(rho : ℂ)‖⁻¹ ^ (2 : ℕ) := by    ring  unfold zeroSquareTail  rw [zero_sub, norm_neg]  exact le_trans hpow (by rw [hpow_eq])