Prob Output none seeded Fork le

theorem probOutput_none_seededFork_le :    let acc : ℝ≥0∞ := ∑ s, Pr[= some s | cf <$> main]    let h : ℝ≥0∞ := Fintype.card (spec.Range i)    let q := qb i + 1    Pr[= none | seededFork main qb js i cf] ≤ 1 - acc * (acc / q - h⁻¹) := by  simp only  set ps : Fin (qb i + 1) → ℝ≥0∞ := fun s => Pr[= (some s : Option _) | cf <$> main]  set acc := ∑ s, ps s  set h : ℝ≥0∞ := ↑(Fintype.card (spec.Range i))  have htotal := probOutput_none_add_tsum_some (mx := seededFork main qb js i cf)  rw [probFailure_of_liftM_PMF, tsub_zero] at htotal  calc Pr[= none | seededFork main qb js i cf]    _ = 1 - ∑' p, Pr[= some p | seededFork main qb js i cf] :=        ENNReal.eq_sub_of_add_eq          (ne_top_of_le_ne_top one_ne_top (htotal ▸ le_add_self)) htotal    _ ≤ 1 - ∑ s, Pr[ fun r => r.map (cf ∘ Prod.fst) = some (some s) |            seededFork main qb js i cf] :=        tsub_le_tsub_left (sum_probEvent_fork_le_tsum_some main qb js i cf) 1    _ ≤ 1 - ∑ s, (ps s ^ 2 - ps s / h) :=        tsub_le_tsub_left (Finset.sum_le_sum fun s _ =>          le_probOutput_seededFork main qb js i cf s) 1    _ ≤ 1 - acc * (acc / ↑(qb i + 1) - h⁻¹) := by        refine tsub_le_tsub_left ?_ 1        have hsum : (∑ s, ps s) ≠ ⊤ := ne_top_of_le_ne_top one_ne_top          (sum_probOutput_some_le_one (mx := cf <$> main) (α := Fin (qb i + 1)))        simpa [Finset.card_univ, Fintype.card_fin] using          ENNReal.mul_tsub_inv_le_sum_sq_sub_div            (Finset.univ : Finset (Fin (qb i + 1))) ps h hsum