Bobs safe

lemma bobs_safe (o : Oracle) (cs : c < s) (sb : s < b) (q0 : 0 < q) (v0 : 0 < v) (v1 : v ≤ 1)    (qv : q ≤ v) (p : Vector ℝ n) (y : Vector Bool n) :    (1 - v) * (1 - q) ^ n ≤ (bobs o (bob s b q) (vera c s v) p y).exp (vera_score v) := by  induction' n with n h  · simp only [Nat.zero_eq, pow_zero, mul_one, bobs, vera_score, exp_pure, le_refl]  · simp only [bobs, exp_bind]; specialize h p.tail y.tail    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, Nat.succ_sub_one,      Comp.prob', prob_pure, Bool.false_eq_true, ↓reduceIte, zero_mul, add_zero, prob_bind] at h ⊢    generalize hbs : bobs o (bob s b q) (vera c s v) p.tail y.tail = bs    simp only [hbs] at h    generalize hbn : (bob s b q n y.tail p.head).prob' o = bn    trans (bs.prob (some false) + bs.prob none * (1 - v)) * (1 - q)    · refine le_trans ?_ (mul_le_mul_of_nonneg_right h (by linarith))      rw [mul_assoc, ←pow_succ]    · simp only [add_mul]; apply add_le_add      · exact mul_le_of_le_one_right (prob_nonneg _) (by linarith)      · rw [mul_assoc]; refine mul_le_mul_of_nonneg_left ?_ (prob_nonneg _)        trans bn.exp (fun r ↦ ((vera c s v _ y.tail p.head).prob' o).exp (fun x ↦          (if some false = if r then none else some x then 1 else 0) +          (if none = if r then none else some x then 1 else 0) * (1 - v)))        · by_cases ps : |p.head - (o _ y.tail).prob true| ≤ s          · rw [mul_comm]            refine le_exp_of_cut (fun x ↦ x = true) (1-q) (1-v) ?_ ?_ ?_ (by linarith)            · have bc := bob_complete o BobId sb q0 ps              simp only [Nat.succ_sub_one] at bc              rw [←hbn, pr_eq_prob, bool_prob_true_of_false, bob]; linarith            · intro x _ xe              simp only [xe, if_true, if_false, zero_add, one_mul, exp_const, le_refl]            · intro _ _ _; apply exp_nonneg; intro _ _; apply add_nonneg ite_one_zero_nonneg              apply mul_nonneg ite_one_zero_nonneg; linarith          · apply le_exp_of_forall_le; intro r _; induction r            · trans 1 - v; apply mul_le_of_le_one_right; linarith; linarith              have vs := bob_sound o VeraId cs v0 (le_of_lt (not_le.mp ps))              simp only [if_false, Option.some_inj, zero_mul, add_zero, @eq_comm _ false,                exp_eq_prob, Nat.succ_sub_one, vera, bool_prob_false_of_true] at vs ⊢              linarith            · simp only [if_true, one_mul, if_false, zero_add, exp_const]              apply mul_le_of_le_one_right; linarith; linarith        · simp only [exp_add, exp_mul_const, Nat.succ_sub_one, ← hbn]          convert le_refl _