Bobs catches

lemma bobs_catches (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} (pb : ¬close p (o.probs y) b) :    (1 - v) * (1 - q) ^ n ≤ (bobs o (bob s b q) (vera c s v) p y).pr (λ r ↦ r = some false) := by  induction' n with n h  · simp only [Vector.eq_nil, close_nil, not_true_eq_false] at pb  · by_cases pbn : close p.tail (o.probs y.tail) b    · have safe := bobs_safe o cs sb q0 v0 v1 qv p.tail y.tail      simp only [bobs, Nat.succ_sub_one, pr_bind, @exp_fintype (Option Bool), option_bool_univ,        Finset.mem_singleton, Finset.mem_insert, not_false_eq_true, Finset.sum_insert, pr_pure,        ite_false, mul_zero, ite_true, mul_one, Finset.sum_singleton, zero_add, ge_iff_le,        vera_score] at safe ⊢      generalize hbs : bobs o (bob s b q) (vera c s v) p.tail y.tail = bs      simp only [hbs, 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, Comp.prob', pr_pure, ↓reduceIte, pr_bind] at safe ⊢      trans (bs.prob (some false) + bs.prob none * (1 - v)) * (1 - q)      · refine le_trans ?_ (mul_le_mul_of_nonneg_right safe (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 _)          simp only [Oracle.probs, Nat.succ_sub_one, close_succ, Vector.head_cons, Vector.tail_cons,            pbn, and_true, not_le] at pb          rw [mul_comm]          refine le_exp_of_cut (fun x ↦ x = false) (1-q) (1-v) ?_ ?_ ?_ (by linarith)          · have bs := bob_sound o BobId sb q0 (le_of_lt pb)            simp only [Nat.succ_sub_one, bool_prob_false_of_true, pr_eq_prob, bob,              Comp.prob'] at bs ⊢            linarith          · intro x _ x0            have vs := bob_sound o VeraId cs v0 (le_of_lt (lt_trans sb pb))            simp only [x0, if_false, Option.some_inj, exp_eq_prob, bool_prob_false_of_true, vera,              Nat.succ_sub_one, Comp.prob'] at vs ⊢            linarith          · intro _ _ t            simp only [Bool.not_eq_false] at t; simp only [t, if_true, if_false, exp_const, le_refl]    · specialize h pbn      refine le_trans ?_ (le_pr_bind_of_cut _ (1-q) h ?_ (by linarith))      · rw [mul_assoc, pow_succ]      · intro _ _ f; simp only [f, pr_pure, if_true]; linarith