Alice pr le

lemma alice_pr_le (o : Oracle) (i : OracleId) (e0 : 0 < e) (q0 : 0 < q) (y : Vector Bool n) :    ((alice' e q i _ y).prob' o).pr (λ p ↦ e ≤ |p - (o _ y).prob true|) ≤ q := by  simp only [alice', Comp.prob', Comp.prob_estimate, Comp.prob_query]  refine le_trans (chernoff_estimate_abs_le (o _ y) (samples e q) (le_of_lt e0)) ?_  have le : -2 * ↑(samples e q) * e^2 ≤ -2 * samples' e q * e^2 :=    mul_le_mul_of_nonneg_right (mul_le_mul_of_nonpos_left (le_samples _ _) (by norm_num))      (sq_nonneg _)  refine le_trans (mul_le_mul_of_nonneg_left (Real.exp_le_exp.mpr le) (by norm_num)) ?_; clear le  simp only [samples', div_eq_inv_mul, ←mul_assoc, mul_inv]; norm_num  simp only [mul_comm _ (e^2), ←mul_assoc, mul_inv_cancel (pow_ne_zero _ (ne_of_gt e0)), one_mul]  rw [Real.exp_log]; ring_nf; rfl; positivity