Sum prob Event option map eq some le is Some

lemma sum_probEvent_option_map_eq_some_le_isSome    [Fintype γ] (select : α → Option γ) :    ∑ k : γ, Pr[fun r => r.map select = some (some k) | mx] ≤      Pr[fun r => r.isSome | mx] := by  classical  calc    ∑ k : γ, Pr[fun r => r.map select = some (some k) | mx]        ≤ ∑' x : α, Pr[= some x | mx] := by      simp_rw [probEvent_eq_tsum_ite]      have hsplit : ∀ k : γ,          (∑' r : Option α,            if r.map select = some (some k) then Pr[= r | mx] else 0) =            ∑' x : α, if select x = some k then Pr[= some x | mx] else 0 := by        intro k        simpa only [Option.map, reduceCtorEq, ite_false, zero_add, Option.some.injEq] using          tsum_option (fun r : Option α =>            if r.map select = some (some k) then Pr[= r | mx] else 0) ENNReal.summable      simp_rw [hsplit]      rw [← tsum_fintype (L := .unconditional _), ENNReal.tsum_comm]      refine ENNReal.tsum_le_tsum fun x => ?_      rw [tsum_fintype (L := .unconditional _)]      rcases hselect : select x with _ | k₀      · simp      · rw [Finset.sum_eq_single k₀          (by intro k _ hne; simp [Ne.symm hne]) (by simp)]        simp    _ = Pr[fun r => r.isSome | mx] :=      (probEvent_isSome_eq_tsum_probOutput_some mx).symm