Chernoff le count

lemma chernoff_le_count (f : Prob Bool) (n : ℕ) {t : ℝ} (t0 : 0 ≤ t) :    (count f n).pr (λ x ↦ x ≤ n * f.prob true - t) ≤ (-2 * t^2 / n).exp := by  have h := chernoff_count_le (not <$> f) n t0  simp only [count_not, pr_map] at h  have e : ∀ k, (count f n).prob k ≠ 0 →      (↑n * (not <$> f).prob true + t ≤ ↑(n - k) ↔ ↑k ≤ ↑n * f.prob true - t) := by    intro k m    simp only [not_bool_prob, Bool.not_true, bool_prob_false_of_true, Nat.cast_sub (count_le' _ m),      mul_sub, mul_one, sub_add, sub_le_sub_iff_left]  rw [pr_congr e] at h; exact h