Chernoff estimate abs le

lemma chernoff_estimate_abs_le (f : Prob Bool) (n : ℕ) {t : ℝ} (t0 : 0 ≤ t) :    (estimate f n).pr (λ x ↦ t ≤ |x - f.prob true|) ≤ (2:ℝ) * ((-2:ℝ) * n * t^2).exp := by  by_cases n0 : (n : ℝ) = 0  · simp only [n0, mul_zero, zero_mul, Real.exp_zero]    exact le_trans pr_le_one (by norm_num)  have np : 0 < (n : ℝ) := (Ne.symm n0).lt_of_le (Nat.cast_nonneg _)  simp only [estimate, pr_map]  have b := chernoff_count_abs_le f n (mul_nonneg (Nat.cast_nonneg n) t0)  simp only [mul_pow, div_eq_inv_mul, ←mul_assoc, pow_two (n:ℝ)] at b  rw [mul_comm _ (n:ℝ)] at b; simp only [←mul_assoc, mul_inv_cancel n0, one_mul] at b  apply le_trans _ b; apply le_of_eq  apply pr_congr; intro x _; simp only [mul_comm _ t, ←le_div_iff np]  nth_rewrite 3 [←abs_of_pos np]; simp only [←abs_div, sub_div]; field_simp [n0]