Alices success

lemma alices_success (o : Oracle) (L : o.lipschitz t k) (e0 : 0 < e) (q0 : 0 < q) (q1 : q ≤ 1) :    (o.final t).prob true - k * e - ((1:ℝ) - (1 - q : ℝ)^(t+1)) ≤      (alices o (alice e q) (t+1)).pr (fun (p,y) => close p (o.probs y) e ∧ y.head) := by  trans (snaps o (alice e q) e (t+1)).pr (fun (_,y) => y.head) - (1 - (1 - q)^(t+1))  · apply sub_le_sub_right; trans ((snap o (alice e q) e).final t).prob true    · have lip := (abs_le.mp (L.le (snap o (alice e q) e))).2      simp only [sub_le_iff_le_add, add_comm _ (k * e)] at lip ⊢      exact le_trans lip (add_le_add_right (mul_le_mul_of_nonneg_left (snap_dist _ e0) L.k0) _)    · apply le_of_eq; simp only [←snaps_eq_snap_final, prob_map]      apply pr_congr; intro _ _; rfl  · simp only [sub_le_iff_le_add]    rw [pr_eq_add_of_cut (fun (p,y) => close p (o.probs y) e)]; apply add_le_add    · simp only [pr]; apply exp_mono'; intro (p,y)      by_cases c : close p (o.probs y) e      · simp only [c, true_and, if_false, add_zero, snaps_prob _ c, and_true, le_refl]      · simp only [c, false_and, if_false, zero_add, if_true, mul_one, and_false, mul_zero, le_refl]    · trans (snaps o (alice e q) e (t+1)).pr (fun (p,y) => ¬close p (o.probs y) e)      · apply pr_mono; intro _ _; simp only [and_imp, imp_self, implies_true]      · have ae : (snaps o (alice e q) e (t+1)).pr (fun (p,y) => close p (o.probs y) e) =            (alices o (alice e q) (t+1)).pr (fun (p,y) => close p (o.probs y) e) := by          apply exp_congr'; intro (p,y)          by_cases c : close p (o.probs y) e          · simp only [c, if_true, mul_one, snaps_prob _ c]          · simp only [c, if_false, mul_zero]        simp only [pr_neg, ae]; linarith [alices_close o e0 q0 q1 (t+1)]