Complex.exists_completedRiemannZeta₀_right_halfPlane

lemma exists_completedRiemannZeta₀_right_halfPlane (z : ℂ) :    ∃ w : ℂ,      completedRiemannZeta₀ w = completedRiemannZeta₀ z ∧        (2⁻¹ : ℝ) ≤ w.re ∧ ‖w‖ ≤ 1 + ‖z‖ := by  refine ⟨if z.re < (2⁻¹ : ℝ) then 1 - z else z, ?_, ?_, ?_⟩  · by_cases hzr : z.re < (2⁻¹ : ℝ)    · have hw : (if z.re < (2⁻¹ : ℝ) then 1 - z else z) = 1 - z := by        simp [hzr]      simpa [hw] using (completedRiemannZeta₀_one_sub z)    · simp [hzr]  · by_cases hzr : z.re < (2⁻¹ : ℝ)    · have : (if z.re < (2⁻¹ : ℝ) then 1 - z else z).re = 1 - z.re := by        simp [hzr]      linarith [this, hzr]    · simpa [hzr] using le_of_not_gt hzr  · by_cases hzr : z.re < (2⁻¹ : ℝ)    · have hw : (if z.re < (2⁻¹ : ℝ) then 1 - z else z) = 1 - z := by        simp [hzr]      have : ‖1 - z‖ ≤ ‖(1 : ℂ)‖ + ‖z‖ := by        simpa using (norm_sub_le (1 : ℂ) z)      simpa [hw, norm_one, add_comm, add_left_comm, add_assoc] using this    · simp [hzr]