Cond bind le second

lemma cond_bind_le_second {f : Prob α} {g : α → Prob β} (p q : β → Prop) (i : α → Prop) {b : ℝ}    (b0 : 0 ≤ b) (gb : ∀ x, f.prob x ≠ 0 → i x → (g x).cond p q ≤ b) :    (f >>= λ x ↦ Prod.mk x <$> g x).cond (λ y ↦ p y.snd) (λ y ↦ q y.snd ∧ i y.fst) ≤ b := by  simp only [cond]  by_cases d0 : (f >>= λ x ↦ Prod.mk x <$> g x).pr (λ y ↦ q y.2 ∧ i y.1) = 0  · simp only [d0, div_zero, b0]  simp only [div_le_iff ((Ne.symm d0).lt_of_le pr_nonneg)]  simp only [pr, ←exp_const_mul, exp_bind]; apply exp_mono; intro x m  simp only [exp_map, Function.comp]  by_cases ix : i x  · simp only [ix, and_true]; specialize gb x m ix; simp only [cond] at gb    by_cases gq : (g x).pr q = 0    · rw [exp_eq_zero]      · apply exp_nonneg; intro y _; by_cases qy : q y        repeat simp only [qy, if_true, if_false, mul_one, mul_zero, b0, le_refl]      · intro y n; rw [pr_eq_zero] at gq; simp only [gq y n, and_false, if_false]    · simp only [div_le_iff ((Ne.symm gq).lt_of_le pr_nonneg)] at gb;      simp only [pr, ←exp_const_mul] at gb; convert gb  · simp only [ix, and_false, ite_false, mul_zero, le_refl]