Evil alices lies

lemma evil_alices_lies (o : Oracle) (L : o.lipschitz t k) (eve : Alice) (e0 : 0 < e) :    (alices o eve (t+1)).pr (λ (p,y) ↦ close p (o.probs y) e ∧ y.head) ≤      (o.final t).prob true + k * e := by  trans (snaps o eve e (t+1)).pr (λ (p,y) ↦ close p (o.probs y) e ∧ y.head)  · apply le_of_eq; apply exp_congr'; intro (p,y); by_cases c : close p (o.probs y) e    · simp only [c, true_and, snaps_prob _ c]    · simp only [c, false_and, if_false, mul_zero]  · trans ((snap o eve e).final t).prob true    · simp only [←snaps_eq_snap_final, prob_map]      apply pr_mono; intro (p,y) _; simp only [final, and_imp, imp_self, implies_true]    · have lip := (abs_le.mp (L.le (snap o eve e))).1      rw [le_sub_iff_add_le, add_comm, ←sub_eq_add_neg, sub_le_iff_le_add] at lip      exact le_trans lip (add_le_add_left (mul_le_mul_of_nonneg_left (snap_dist _ e0) L.k0) _)