Is Query Bound P iff counting filter le

theorem isQueryBoundP_iff_counting_filter_le    [DecidableEq ι] [Fintype ι] [IsUniformSpec spec]    {oa : OracleComp spec α} {n : ℕ} :    IsQueryBoundP oa p n ↔      ∀ z ∈ support (countingOracle.simulate oa 0),        (∑ i ∈ Finset.univ.filter p, z.2 i) ≤ n := by  refine ⟨fun h _ hz => IsQueryBoundP.counting_bounded h hz, fun h => ?_⟩  induction oa using OracleComp.inductionOn generalizing n with  | pure _ => trivial  | query_bind t mx ih =>      rw [isQueryBoundP_query_bind_iff]      have hsplit : ∀ (q : QueryCount ι),          (∑ i ∈ Finset.univ.filter p, (QueryCount.single t + q) i) =          (∑ i ∈ Finset.univ.filter p, QueryCount.single t i) +          (∑ i ∈ Finset.univ.filter p, q i) := by        intro q        simp [Pi.add_apply, Finset.sum_add_distrib]      refine ⟨?_, fun u => ?_⟩      · by_cases hpt : p t        · refine Or.inr ?_          obtain ⟨z₀, hz₀⟩ := countingOracle.support_simulate_nonempty (mx default)          have hbig : (z₀.1, QueryCount.single t + z₀.2) ∈              support (countingOracle.simulate ((query t : OracleComp spec _) >>= mx) 0) :=            countingOracle.add_single_mem_support_simulate_queryBind hz₀          have hbound := h _ hbig          rw [hsplit, sum_single_filter_eq_one hpt] at hbound          omega        · exact Or.inl hpt      · apply ih u        intro z hz        have hbig' : (z.1, QueryCount.single t + z.2) ∈            support (countingOracle.simulate ((query t : OracleComp spec _) >>= mx) 0) :=          countingOracle.add_single_mem_support_simulate_queryBind hz        have hbound := h _ hbig'        rw [hsplit] at hbound        by_cases hpt : p t        · simp only [if_pos hpt]          rw [sum_single_filter_eq_one hpt] at hbound          omega        · simp only [if_neg hpt]          rwa [sum_single_filter_eq_zero hpt, zero_add] at hbound