Evil bobs lies

lemma evil_bobs_lies (o : Oracle) (eve : Bob) (cs : c < s) (v0 : 0 < v)    {p : Vector ℝ (t+1)} {y : Vector Bool (t+1)} (py : close p (o.probs y) c) (yt : y.head) :    (bobs o eve (vera c s v) p y).pr (λ r ↦ extract ((p,y),r) = false) ≤ v := by  rw [pr_eq_cond_add_cond (λ r : Option Bool ↦ r.isSome)]  have b1 : (bobs o eve (vera c s v) p y).cond (λ r ↦ extract ((p,y),r) = false)      (λ r ↦ ¬r.isSome) = 0 := by    apply cond_eq_zero; intro r _ ri    simp only [Option.not_isSome_iff_eq_none] at ri    simp [ri, extract, yt]  simp only [b1, zero_mul, add_zero]  refine le_trans (mul_le_of_le_one_right cond_nonneg pr_le_one) ?_  refine le_trans (le_of_eq ?_) (evil_bobs_lies' o eve cs v0 py)  apply cond_congr; intro r _ ri; match r with  | some r => simp only [extract, Option.some_inj]  | none => simp at ri