Kadiri.zeroImagDyadicAbsToPositiveCountWithZeroHeightSource_of_conj

theorem zeroImagDyadicAbsToPositiveCountWithZeroHeightSource_of_conj    (hconj : riemannZetaConjZeroSource) :    zeroImagDyadicAbsToPositiveCountWithZeroHeightSource := by  classical  refine ⟨2, (Nat.card ZeroHeightNontrivialZeros : ℝ), by norm_num, ?_, ?_⟩  · exact_mod_cast Nat.zero_le (Nat.card ZeroHeightNontrivialZeros)  intro k  let T : ℝ := (2 : ℝ) ^ (k + 1)  have hT_pos : 0 < T := by    exact pow_pos (by norm_num) _  let Abs := {rho : NontrivialZeros // |(rho : ℂ).im| < T}  let Pos := {rho : NontrivialZeros // 0 < (rho : ℂ).im ∧ (rho : ℂ).im < T}  let Z := ZeroHeightNontrivialZeros  haveI : Finite Pos := by    haveI : Finite (riemannZeta.zeroes_rect (.Ioo (0 : ℝ) 1) (.Ioo 0 T)) :=      Set.finite_coe_iff.mpr (zeroes_rect_Ioo_critical_positive_height_finite T)    exact Finite.of_equiv _ (positiveHeightNontrivialZeroEquivZeroesRect T).symm  haveI : Finite Z := zeroHeightNontrivialZeros_finite  let toBucket : Abs → ((Pos ⊕ Pos) ⊕ Z) := fun rho =>    if hpos : 0 < (rho.1 : ℂ).im then      Sum.inl (Sum.inl        ⟨rho.1,          by            constructor            · exact hpos            · have hlt := rho.2              rwa [abs_of_pos hpos] at hlt⟩)    else if hzero : (rho.1 : ℂ).im = 0 then      Sum.inr ⟨rho.1, hzero⟩    else      have hle : (rho.1 : ℂ).im ≤ 0 := le_of_not_gt hpos      have hneg : (rho.1 : ℂ).im < 0 := lt_of_le_of_ne hle hzero      Sum.inl (Sum.inr        ⟨⟨((starRingEnd ℂ) (rho.1 : ℂ)),            by simpa [Complex.conj_re] using rho.1.property.1,            Set.mem_univ _,            by exact hconj (rho.1 : ℂ) rho.1.property.2.2⟩,          by            constructor            · rw [Complex.conj_im]              exact neg_pos.mpr hneg            · rw [Complex.conj_im]              simpa [abs_of_neg hneg] using rho.2⟩)  let recover : ((Pos ⊕ Pos) ⊕ Z) → NontrivialZeros := fun bucket =>    match bucket with    | Sum.inl (Sum.inl rho) => rho.1    | Sum.inl (Sum.inr rho) =>        ⟨((starRingEnd ℂ) (rho.1 : ℂ)),          by simpa [Complex.conj_re] using rho.1.property.1,          Set.mem_univ _,          by exact hconj (rho.1 : ℂ) rho.1.property.2.2⟩    | Sum.inr rho => rho.1  have hrecover : ∀ rho : Abs, recover (toBucket rho) = rho.1 := by    intro rho    by_cases hpos : 0 < (rho.1 : ℂ).im    · simp [toBucket, recover, hpos]    · by_cases hzero : (rho.1 : ℂ).im = 0      · simp [toBucket, recover, hzero]      · simp [toBucket, recover, hpos, hzero]  have hinj : Function.Injective toBucket := by    intro rho eta h    apply Subtype.ext    calc      rho.1 = recover (toBucket rho) := (hrecover rho).symm      _ = recover (toBucket eta) := by rw [h]      _ = eta.1 := hrecover eta  have hcard_nat :      Nat.card Abs ≤ Nat.card ((Pos ⊕ Pos) ⊕ Z) :=    Nat.card_le_card_of_injective toBucket hinj  have hcard_real :      (Nat.card Abs : ℝ) ≤ (Nat.card ((Pos ⊕ Pos) ⊕ Z) : ℝ) := by    exact_mod_cast hcard_nat  have htarget :      (Nat.card ((Pos ⊕ Pos) ⊕ Z) : ℝ) =        2 * (Nat.card Pos : ℝ) + (Nat.card Z : ℝ) := by    rw [Nat.card_sum, Nat.card_sum]    norm_num [Nat.cast_add]    ring  calc    (Nat.card {rho : NontrivialZeros // |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} : ℝ)        = (Nat.card Abs : ℝ) := by rfl    _ ≤ (Nat.card ((Pos ⊕ Pos) ⊕ Z) : ℝ) := hcard_real    _ = 2 * (Nat.card Pos : ℝ) + (Nat.card Z : ℝ) := htarget    _ = 2 * (Nat.card {rho : NontrivialZeros //          0 < (rho : ℂ).im ∧ (rho : ℂ).im < (2 : ℝ) ^ (k + 1)} : ℝ) +        (Nat.card ZeroHeightNontrivialZeros : ℝ) := by          rfl