Prob Event congr

lemma probEvent_congr' {p q : α → Prop} {oa : OracleComp spec α} {oa' : OracleComp spec' α}    (h1 : ∀ x, x ∈ support oa → (p x ↔ q x))    (h2 : 𝒟[oa] = 𝒟[oa']) : Pr[ p | oa] = Pr[ q | oa'] := by  have hpr : (Pr[= · | oa]) = (Pr[= · | oa']) := funext fun x => probOutput_congr rfl h2  rw [probEvent_eq_tsum_indicator, probEvent_eq_tsum_indicator, hpr]  refine tsum_congr fun x => ?_  by_cases hx : x ∈ support oa  · have hs : x ∈ ({x | p x} : Set α) ↔ x ∈ ({x | q x} : Set α) := h1 x hx    by_cases hp : x ∈ ({x | p x} : Set α)    · rw [Set.indicator_of_mem hp, Set.indicator_of_mem (hs.mp hp)]    · rw [Set.indicator_of_notMem hp, Set.indicator_of_notMem (hs.not.mp hp)]  · have hz : Pr[= x | oa'] = 0 := congrFun hpr.symm x ▸ probOutput_eq_zero_of_not_mem_support hx    rw [Set.indicator_apply_eq_zero.2 fun _ => hz, Set.indicator_apply_eq_zero.2 fun _ => hz]