Soundness

theorem soundness' (o : Oracle) (L : o.lipschitz t k) (eve : Alice)    (c0 : 0 < c) (cs : c < s) (sb : s < b) (q0 : 0 < q) (v0 : 0 < v) (v1 : v ≤ 1) (qv : q ≤ v) :    (1 - v) * (1 - q) ^ (t+1) * ((o.final t).prob false - k * b) ≤      ((debate eve (bob s b q) (vera c s v) t).prob' o).prob false := by  simp only [debate_eq_transposed, transposed, trace, map_bind, ge_iff_le,    ← pr_eq_prob (alices _ _ _ >>= _)]  have lies := evil_alices_lies o L eve (lt_trans c0 (lt_trans cs sb))  rw [pr_neg', sub_le_iff_le_add, add_comm, ←sub_le_iff_le_add, bool_prob_true_of_false] at lies  simp only [not_and_or, Bool.not_eq_true] at lies; ring_nf at lies  rw [mul_comm]; refine le_pr_bind_of_cut _ ?_ lies ?_ ?_  · intro (p,y) _ h; simp only [pr_map]; cases' h with h h    · refine le_trans (bobs_catches o cs sb q0 v0 v1 qv h) ?_      apply pr_mono; intro r _ e; simp only [e, extract]    · simp only at h; simp only [pr]      have safe := bobs_safe o cs sb q0 v0 v1 qv p y      generalize hbs : bobs o (bob s b q) (vera c s v) p y = bs; simp only [hbs] at safe      simp only [@exp_fintype (Option Bool), option_bool_univ, vera_score, Finset.mem_insert,        some.injEq, Bool.true_eq_false, Finset.mem_singleton, or_self, not_false_eq_true,        Finset.sum_insert, mul_zero, mul_one, Finset.sum_singleton, zero_add, extract, h, mul_ite,        ↓reduceIte, ge_iff_le] at safe ⊢      exact le_trans safe (add_le_add_left (mul_le_of_le_one_right (prob_nonneg _) (by linarith)) _)  · apply mul_nonneg; linarith; apply pow_nonneg; linarith