Prob Event pair collision le

theorem probEvent_pair_collision_le {α : Type}    [Inhabited ι]    (oa : OracleComp spec α)    (n : ℕ)    (hrange : ∀ t, Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t))    (i j : Fin n) (hij : i ≠ j) :    Pr[fun z => z.2.length > i.val ∧ z.2.length > j.val ∧        z.2[i]?.bind (fun ei => z.2[j]?.map (fun ej =>          ei.1 ≠ ej.1 ∧ HEq ei.2 ej.2)) = some true |      (simulateQ loggingOracle oa).run] ≤      (Fintype.card (spec.Range default) : ℝ≥0∞)⁻¹ := by  apply le_trans (probEvent_mono fun z _ h => h.2.2)  suffices h : ∀ (β : Type) (ob : OracleComp spec β) (i j : ℕ) (_ : i ≠ j),      Pr[fun z => z.2[i]?.bind (fun ei => z.2[j]?.map (fun ej =>        ei.1 ≠ ej.1 ∧ HEq ei.2 ej.2)) = some true |        (simulateQ loggingOracle ob).run] ≤        (Fintype.card (spec.Range default) : ℝ≥0∞)⁻¹ from    h α oa i.val j.val (Fin.val_ne_of_ne hij)  intro β ob  induction ob using OracleComp.inductionOn with  | pure x => intro i j _; simp [simulateQ_pure]  | query_bind t mx ih =>    intro i j hij    rw [run_simulateQ_loggingOracle_query_bind, probEvent_bind_eq_tsum]    simp_rw [probEvent_map, Function.comp_def]    -- The matched output lives at position `k` in the log; both end cases reduce to    -- `probEvent_log_output_match_le` after extracting the sigma entry.    have key : ∀ (u : spec.Range t) (k : ℕ) (e : β × QueryLog spec → Prop),        (∀ z, e z → ∃ s v, z.2[k]? = some ⟨s, v⟩ ∧ HEq u v) →        Pr[e | (simulateQ loggingOracle (mx u)).run] ≤          (Fintype.card (spec.Range default) : ℝ≥0∞)⁻¹ := fun u k e he =>      (probEvent_mono fun z _ => he z).trans (probEvent_log_output_match_le hrange (mx u) k t u)    match i, j, hij with    | 0, 0, hij => exact absurd rfl hij    | 0, j' + 1, _ =>      simp only [List.getElem?_cons_zero, List.getElem?_cons_succ, Option.bind_some]      refine tsum_query_mul_probEvent_le_aux t mx _ _ fun u => key u j' _ fun z hev => ?_      match hz : z.2[j']? with      | none => simp [hz] at hev      | some ⟨s, v⟩ => exact ⟨s, v, rfl, by simp_all⟩    | i' + 1, 0, _ =>      simp only [List.getElem?_cons_zero, List.getElem?_cons_succ]      refine tsum_query_mul_probEvent_le_aux t mx _ _ fun u => key u i' _ fun z hev => ?_      match hz : z.2[i']? with      | none => simp [hz] at hev      | some ⟨s, v⟩ => exact ⟨s, v, rfl, (by simp_all : v ≍ u).symm⟩    | i' + 1, j' + 1, hij =>      simp only [List.getElem?_cons_succ]      exact tsum_query_mul_probEvent_le_aux t mx _ _ fun u => ih u i' j' (by lia)