Prob Event log output match le

theorem probEvent_log_output_match_le {α : Type}    [Inhabited ι]    (hrange : ∀ t, Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t))    (oa : OracleComp spec α)    (k : ℕ) (t₀ : spec.Domain) (u₀ : spec.Range t₀) :    Pr[fun z => ∃ (s : spec.Domain) (v : spec.Range s),        z.2[k]? = some ⟨s, v⟩ ∧ HEq u₀ v |      (simulateQ loggingOracle oa).run] ≤      (Fintype.card (spec.Range default) : ℝ≥0∞)⁻¹ := by  classical  induction oa using OracleComp.inductionOn generalizing k with  | pure _ =>    refine le_of_eq_of_le (probEvent_eq_zero fun z hmem h => ?_) zero_le    simp only [simulateQ_pure, WriterT.run_pure', List.empty_eq, support_pure,      Set.mem_singleton_iff] at hmem    obtain ⟨_, rfl⟩ := hmem    obtain ⟨s, v, hlog, _⟩ := h; simp at hlog  | query_bind t mx ih =>    rw [run_simulateQ_loggingOracle_query_bind, probEvent_bind_eq_tsum]    simp_rw [probEvent_map, Function.comp_def]    cases k with    | zero =>      have hpred : ∀ u' : spec.Range t,          (fun z : α × QueryLog spec =>            ∃ (s : spec.Domain) (v : spec.Range s),              ((⟨t, u'⟩ : (i : spec.Domain) × spec.Range i) :: z.2)[0]? = some ⟨s, v⟩ ∧              HEq u₀ v) =          (fun _ => HEq u₀ u') := by        intro u'; ext z        simp only [List.getElem?_cons_zero, Option.some.injEq]        exact ⟨fun ⟨s, v, heq, hheq⟩ => by cases heq; exact hheq, fun h => ⟨t, u', rfl, h⟩⟩      simp_rw [hpred, probEvent_const, probFailure_of_liftM_PMF, tsub_zero, probOutput_query]      rw [ENNReal.tsum_mul_left]      have hind_le : ∑' (u' : spec.Range t), (if HEq u₀ u' then (1 : ℝ≥0∞) else 0) ≤ 1 := by        rw [tsum_eq_sum (s := Finset.univ) (by simp), Finset.sum_ite, Finset.sum_const_zero,          add_zero, Finset.sum_const, nsmul_eq_mul, mul_one]        exact_mod_cast Finset.card_le_one.mpr fun a ha b hb => by          simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha hb          exact eq_of_heq (ha.symm.trans hb)      exact le_trans (mul_le_of_le_one_right' hind_le)        (ENNReal.inv_le_inv.mpr (by exact_mod_cast hrange t))    | succ k' =>      simp_rw [List.getElem?_cons_succ]      exact tsum_query_mul_probEvent_le_aux t mx _ _ fun u => ih u k'