Prob Event hidden Read List le

theorem probEvent_hiddenReadList_le {oa : ProbComp R} {ε : ℝ≥0∞} (hε : ∀ r : R, Pr[= r | oa] ≤ ε)    (q : ℕ) (σ : List Bool → R) (n : ℕ) :    Pr[(fun b : Bool => b = true) | hiddenReadList oa q σ n] ≤ (n : ℝ≥0∞) * ((q : ℝ≥0∞) * ε) := by  induction n with  | zero => simp [hiddenReadList]  | succ n ih =>    rw [hiddenReadList, probEvent_bind_eq_tsum]    have hsplit : ∀ w : R,        Pr[= w | oa] * Pr[(fun c : Bool => c = true) |            hiddenReadList oa q σ n >>= fun b => pure (readMany w q σ || b)]          ≤ Pr[= w | oa] * Pr[(fun c : Bool => c = true) | (pure (readMany w q σ) : ProbComp Bool)]            + Pr[= w | oa] * Pr[(fun c : Bool => c = true) | hiddenReadList oa q σ n] := by      intro w      rw [← mul_add]      gcongr      exact probEvent_bind_const_or_pure (readMany w q σ) (hiddenReadList oa q σ n)    refine le_trans (ENNReal.tsum_le_tsum hsplit) ?_    rw [ENNReal.tsum_add]    have h1 : (∑' w : R, Pr[= w | oa] *        Pr[(fun c : Bool => c = true) | (pure (readMany w q σ) : ProbComp Bool)])        = Pr[(fun b : Bool => b = true) | hiddenReadMany oa q σ] := by      rw [hiddenReadMany, probEvent_bind_eq_tsum]    have h2 : (∑' w : R, Pr[= w | oa] *        Pr[(fun c : Bool => c = true) | hiddenReadList oa q σ n])        ≤ Pr[(fun c : Bool => c = true) | hiddenReadList oa q σ n] := by      rw [ENNReal.tsum_mul_right]      exact mul_le_of_le_one_left zero_le tsum_probOutput_le_one    rw [h1]    calc Pr[(fun b : Bool => b = true) | hiddenReadMany oa q σ]          + (∑' w : R, Pr[= w | oa] *              Pr[(fun c : Bool => c = true) | hiddenReadList oa q σ n])        ≤ (q : ℝ≥0∞) * ε + (n : ℝ≥0∞) * ((q : ℝ≥0∞) * ε) :=          add_le_add (probEvent_hiddenReadMany_le hε q σ) (le_trans h2 ih)      _ = (↑(n + 1) : ℝ≥0∞) * ((q : ℝ≥0∞) * ε) := by push_cast; ring