Kadiri.zeroImagSquareTail_shifted_le_four

lemma zeroImagSquareTail_shifted_le_four {s : ℂ} {rho : NontrivialZeros}    (hlarge : 2 * |s.im| + 2 ≤ |(rho : ℂ).im|) :    |(s - (rho : ℂ)).im|⁻¹ ^ (2 : ℕ) ≤ 4 * zeroImagSquareTail rho := by  have hs_abs : (0 : ℝ) ≤ |s.im| := abs_nonneg _  have him_pos : 0 < |(rho : ℂ).im| := by linarith  have hhalf_pos : 0 < |(rho : ℂ).im| / 2 := by linarith  have hlower : |(rho : ℂ).im| / 2 ≤ |(s - (rho : ℂ)).im| := by    have hsub_im : (s - (rho : ℂ)).im = s.im - (rho : ℂ).im := Complex.sub_im s (rho : ℂ)    have h1 : |(rho : ℂ).im| - |s.im| ≤ |s.im - (rho : ℂ).im| := by      calc |(rho : ℂ).im| - |s.im| ≤ |(rho : ℂ).im - s.im| := abs_sub_abs_le_abs_sub _ _        _ = |s.im - (rho : ℂ).im| := abs_sub_comm _ _    rw [hsub_im]    linarith  have hinv : |(s - (rho : ℂ)).im|⁻¹ ≤ (|(rho : ℂ).im| / 2)⁻¹ :=    inv_anti₀ hhalf_pos hlower  have hinv_eq : (|(rho : ℂ).im| / 2)⁻¹ = 2 * |(rho : ℂ).im|⁻¹ := by    rw [div_eq_mul_inv, mul_inv, inv_inv]    ring  have hinv' : |(s - (rho : ℂ)).im|⁻¹ ≤ 2 * |(rho : ℂ).im|⁻¹ := by    rw [← hinv_eq]    exact hinv  have hinv_nonneg : 0 ≤ |(s - (rho : ℂ)).im|⁻¹ := inv_nonneg.mpr (abs_nonneg _)  unfold zeroImagSquareTail  calc |(s - (rho : ℂ)).im|⁻¹ ^ (2 : ℕ)      ≤ (2 * |(rho : ℂ).im|⁻¹) ^ (2 : ℕ) := pow_le_pow_left₀ hinv_nonneg hinv' 2    _ = 4 * |(rho : ℂ).im|⁻¹ ^ (2 : ℕ) := by ring