Cond bind le first

lemma cond_bind_le_first {f : Prob α} {g : α → Prob β} (p q : β → Prop) (i j : α → Prop)    (pi : ∀ x y, f.prob x ≠ 0 → (g x).prob y ≠ 0 → j x → p y → q y → i x)    (jq : ∀ x y, f.prob x ≠ 0 → (g x).prob y ≠ 0 → j x → q y) :    (f >>= λ x ↦ Prod.mk x <$> g x).cond (λ y ↦ p y.snd) (λ y ↦ q y.snd ∧ j y.fst) ≤      f.cond i j := by  simp only [cond]; by_cases fj : f.pr j = 0  · have qj : (f >>= λ x ↦ Prod.mk x <$> g x).pr (λ y ↦ q y.2 ∧ j y.1) = 0 := by      refine le_antisymm ?_ pr_nonneg; rw [←fj]      apply pr_enrich_le_pr; intro x y _ _ ⟨_,jx⟩; exact jx    simp only [fj, qj, div_zero, le_refl]  refine div_le_div pr_nonneg ?_ ((Ne.symm fj).lt_of_le pr_nonneg) ?_  · apply pr_enrich_le_pr; intro x y fx gy ⟨py,qy,jx⟩; exact ⟨pi x y fx gy jx py qy, jx⟩  · apply pr_le_pr_enrich; intro x y fx gy jx; exact ⟨jq x y fx gy jx,jx⟩