Evil bobs lies

lemma evil_bobs_lies' (o : Oracle) (eve : Bob) (cs : c < s) (v0 : 0 < v)    {p : Vector ℝ n} {y : Vector Bool n} (py : close p (o.probs y) c) :    (bobs o eve (vera c s v) p y).cond (λ r ↦ r = some false) (λ r ↦ r.isSome) ≤ v := by  have v0' := le_of_lt v0  induction' n with n h  · simp only [bobs, cond_pure, Option.isSome_none, Bool.false_eq_true, and_self, ↓reduceIte, v0']  · simp only [close_succ, Vector.eq_cons_iff] at py    apply le_trans (cond_bind_le_of_cut (λ r ↦ r.isSome)); apply max_le    · refine le_trans (cond_bind_le_first (λ r ↦ r = some false)        (λ r ↦ r.isSome) (λ r ↦ r = some false) (λ r ↦ r.isSome) ?_ ?_) ?_;      · intro r s pr ps r0 s0 _; match r with        | none => simp only [Option.isSome_none, Bool.false_eq_true] at r0        | some false => rfl        | some true =>          simp only [s0, prob_pure, some.injEq, Bool.false_eq_true, ↓reduceIte, ne_eq,            not_true_eq_false] at ps      · intro r s pr ps ri; match r with        | none => simp only [Option.isSome_none, Bool.false_eq_true] at ri        | some r => simp only [prob_pure, ite_one_zero_ne_zero] at ps; simp only [ps, Option.isSome]      · exact h py.2    · refine cond_bind_le_second (λ r ↦ r = some false) (λ r ↦ r.isSome)        (λ r : Option Bool ↦ ¬r.isSome) v0' ?_      intro r pr ri; match r with      | some _ => simp only [Option.isSome, not_true_eq_false] at ri      | none =>          simp only; apply cond_bind_le_of_forall_le v0'          intro b _; match b with          | true => simp [cond_pure, v0']          | false =>            simp only [if_false]; rw [cond_eq_pr]            · refine le_trans ?_ (bob_complete o VeraId cs v0 py.1)              simp only [pr_bind, pr_pure, Option.some_inj, exp_eq_prob]; rfl            · simp only [pr_eq_one, prob_bind]              intro r h; match r with              | some _ => simp only [Option.isSome]              | none =>                contrapose h; clear h; simp only [not_not]; apply exp_eq_zero                intro x _; simp only [prob_pure, if_false]