Prob Event cache has value le of unique preimage

theorem probEvent_cache_has_value_le_of_unique_preimage {α : Type}    [Inhabited ι]    (oa : OracleComp spec α)    (n : ℕ) (hbound : IsTotalQueryBound oa n)    (hrange : ∀ t, Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t))    (v₀ : spec.Range default)    (cache₀ : QueryCache spec)    (hunique_v₀ :      ∀ t₀ t₁ : spec.Domain,        ∀ v₁ : spec.Range t₀, ∀ v₂ : spec.Range t₁,          cache₀ t₀ = some v₁ →          cache₀ t₁ = some v₂ →          HEq v₁ v₀ →          HEq v₂ v₀ →          t₀ = t₁) :    Pr[fun z => ∃ t₀ : spec.Domain, ∃ v : spec.Range t₀,        z.2 t₀ = some v ∧ cache₀ t₀ = none ∧ HEq v v₀ |      (simulateQ cachingOracle oa).run cache₀] ≤      (n : ℝ≥0∞) * (Fintype.card (spec.Range default) : ℝ≥0∞)⁻¹ := by  classical  let C := (Fintype.card (spec.Range default) : ℝ≥0∞)  induction oa using OracleComp.inductionOn generalizing n cache₀ with  | pure x =>    refine le_of_eq_of_le (b := 0) ?_ zero_le    rw [simulateQ_pure]    refine probEvent_eq_zero fun z hz h => ?_    change z ∈ support (pure (x, cache₀) : OracleComp _ _) at hz    rw [support_pure, Set.mem_singleton_iff] at hz    subst hz    obtain ⟨t₀, v, hcache, hnone, _⟩ := h    simp [hnone] at hcache  | query_bind t mx ih =>    rw [isTotalQueryBound_query_bind_iff] at hbound    obtain ⟨hpos, hrest⟩ := hbound    by_cases ht : ∃ v, cache₀ t = some v    · obtain ⟨v, hv⟩ := ht      have hrun : (simulateQ cachingOracle (liftM (query t) >>= mx)).run cache₀ =          (simulateQ cachingOracle (mx v)).run cache₀ := by        simp only [simulateQ_query_bind, OracleQuery.input_query, StateT.run_bind]        have hcache : (liftM (cachingOracle t) : StateT _ (OracleComp spec) _).run cache₀ =            pure (v, cache₀) := by          simp [liftM, MonadLiftT.monadLift, MonadLift.monadLift,            StateT.run_bind, StateT.run_get, hv, pure_bind, StateT.run_pure]        rw [hcache, pure_bind]        simp [OracleQuery.cont_query]      rw [hrun]      calc Pr[fun z => ∃ t₀ v, z.2 t₀ = some v ∧ cache₀ t₀ = none ∧ HEq v v₀ |            (simulateQ cachingOracle (mx v)).run cache₀]          ≤ ((n - 1 : ℕ) : ℝ≥0∞) * C⁻¹ := ih v (n - 1) (hrest v) cache₀ hunique_v₀        _ ≤ (n : ℝ≥0∞) * C⁻¹ := by gcongr; exact_mod_cast Nat.sub_le n 1    · push Not at ht      have ht_none : cache₀ t = none := Option.eq_none_iff_forall_ne_some.mpr ht      have hrun : (simulateQ cachingOracle (liftM (query t) >>= mx)).run cache₀ =          (liftM (query t) >>= fun u =>            (simulateQ cachingOracle (mx u)).run (cache₀.cacheQuery t u)) := by        simp only [simulateQ_query_bind, OracleQuery.input_query, StateT.run_bind]        have hstep : (liftM (cachingOracle t) : StateT _ (OracleComp spec) _).run cache₀ =            (liftM (query t) >>= fun u =>              pure (u, cache₀.cacheQuery t u) : OracleComp spec _) := by          simp only [cachingOracle.apply_eq, liftM, MonadLiftT.monadLift, MonadLift.monadLift,            StateT.run_bind, StateT.run_get, pure_bind, ht_none]          change (StateT.lift (PFunctor.FreeM.lift (P := spec.toPFunctor) t) cache₀ >>= _) = _          simp only [StateT.lift, monad_norm,            modifyGet, MonadState.modifyGet, MonadStateOf.modifyGet,            StateT.modifyGet, StateT.run]          rfl        rw [hstep]; simp [monad_norm]      rw [hrun, probEvent_bind_eq_tsum]      have hih : ∀ u : spec.Range t, ¬HEq u v₀ →          Pr[fun z => ∃ t₀ v, z.2 t₀ = some v ∧ cache₀ t₀ = none ∧ HEq v v₀ |            (simulateQ cachingOracle (mx u)).run (cache₀.cacheQuery t u)] ≤          ((n - 1 : ℕ) : ℝ≥0∞) * C⁻¹ := by        intro u heq_v₀        have hunique_v₀' :            ∀ t₀ t₁ : spec.Domain,              ∀ v₁ : spec.Range t₀, ∀ v₂ : spec.Range t₁,                (cache₀.cacheQuery t u) t₀ = some v₁ →                (cache₀.cacheQuery t u) t₁ = some v₂ →                HEq v₁ v₀ →                HEq v₂ v₀ →                t₀ = t₁ := by          intro t₀ t₁ v₁ v₂ hcache₁ hcache₂ hheq₁ hheq₂          by_cases heq_t₀ : t₀ = t          · subst heq_t₀            rw [QueryCache.cacheQuery_self] at hcache₁            cases hcache₁            exact (heq_v₀ hheq₁).elim          · by_cases heq_t₁ : t₁ = t            · subst heq_t₁              rw [QueryCache.cacheQuery_self] at hcache₂              cases hcache₂              exact (heq_v₀ hheq₂).elim            · rw [QueryCache.cacheQuery_of_ne _ _ heq_t₀] at hcache₁              rw [QueryCache.cacheQuery_of_ne _ _ heq_t₁] at hcache₂              exact hunique_v₀ t₀ t₁ v₁ v₂ hcache₁ hcache₂ hheq₁ hheq₂        calc Pr[fun z => ∃ t₀ v, z.2 t₀ = some v ∧ cache₀ t₀ = none ∧ HEq v v₀ |              (simulateQ cachingOracle (mx u)).run (cache₀.cacheQuery t u)]            ≤ Pr[fun z => ∃ t₀ v, z.2 t₀ = some v ∧                (cache₀.cacheQuery t u) t₀ = none ∧ HEq v v₀ |              (simulateQ cachingOracle (mx u)).run (cache₀.cacheQuery t u)] := by              apply probEvent_mono              intro z hz ⟨t₀, v, hcache_f, hnone₀, hheq⟩              by_cases heq_t : t₀ = t              · exfalso                subst heq_t                have hle := simulateQ_cachingOracle_cache_le (mx u)                  (cache₀.cacheQuery t₀ u) _ hz                have hcu := QueryCache.cacheQuery_self cache₀ t₀ u                have hzu : z.2 t₀ = some u := hle hcu                rw [hzu] at hcache_f; cases hcache_f                exact heq_v₀ hheq              · exact ⟨t₀, v, hcache_f, QueryCache.cacheQuery_of_ne _ _ heq_t ▸ hnone₀, hheq⟩          _ ≤ ((n - 1 : ℕ) : ℝ≥0∞) * C⁻¹ := ih u (n - 1) (hrest u) _ hunique_v₀'      calc ∑' u, Pr[= u | (spec.query t : OracleComp spec _)] *            Pr[fun z => ∃ t₀ v, z.2 t₀ = some v ∧ cache₀ t₀ = none ∧ HEq v v₀ |              (simulateQ cachingOracle (mx u)).run (cache₀.cacheQuery t u)]          ≤ ∑' u, ((if HEq u v₀ then C⁻¹ else 0) +              Pr[= u | (spec.query t : OracleComp spec _)] *                (((n - 1 : ℕ) : ℝ≥0∞) * C⁻¹)) := by            refine ENNReal.tsum_le_tsum fun u => ?_            by_cases h : HEq u v₀            · simp only [h, ite_true]              calc Pr[= u | (spec.query t : OracleComp spec _)] *                    Pr[fun z => ∃ t₀ v, z.2 t₀ = some v ∧ cache₀ t₀ = none ∧ HEq v v₀ |                      (simulateQ cachingOracle (mx u)).run (cache₀.cacheQuery t u)]                  ≤ Pr[= u | (spec.query t : OracleComp spec _)] * 1 :=                    mul_le_mul' le_rfl probEvent_le_one                _ = Pr[= u | (spec.query t : OracleComp spec _)] := mul_one _                _ ≤ (Fintype.card (spec.Range t) : ℝ≥0∞)⁻¹ := (probOutput_query t u).le                _ ≤ C⁻¹ := ENNReal.inv_le_inv.mpr (Nat.cast_le.mpr (hrange t))                _ ≤ C⁻¹ + _ := le_add_right le_rfl            · simp only [h, ite_false, zero_add]              exact mul_le_mul' le_rfl (hih u h)        _ = (∑' u, (if HEq u v₀ then C⁻¹ else 0)) +            (∑' u, Pr[= u | (spec.query t : OracleComp spec _)]) *              (((n - 1 : ℕ) : ℝ≥0∞) * C⁻¹) := by            rw [ENNReal.tsum_add, ENNReal.tsum_mul_right]        _ ≤ C⁻¹ + 1 * (((n - 1 : ℕ) : ℝ≥0∞) * C⁻¹) := by            apply add_le_add            · calc ∑' u, (if HEq u v₀ then C⁻¹ else (0 : ℝ≥0∞))                  ≤ ∑' u, (if HEq u v₀ then (1 : ℝ≥0∞) else 0) * C⁻¹ := by                    refine ENNReal.tsum_le_tsum fun u => ?_                    split_ifs <;> simp                _ = (∑' u, if HEq u v₀ then (1 : ℝ≥0∞) else 0) * C⁻¹ :=                    ENNReal.tsum_mul_right                _ ≤ 1 * C⁻¹ := by                    apply mul_le_mul' _ le_rfl                    rw [tsum_eq_sum (s := Finset.univ) (by simp),                      show ∑ u : spec.Range t, (if HEq u v₀ then (1 : ℝ≥0∞) else 0) =                        ((Finset.univ.filter (fun u : spec.Range t => HEq u v₀)).card : ℝ≥0∞)                        from by rw [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.trans hb.symm)                _ = C⁻¹ := one_mul _            · exact mul_le_mul' tsum_probOutput_le_one le_rfl        _ = (n : ℝ≥0∞) * C⁻¹ := by            rw [one_mul, ← one_add_mul, ← Nat.cast_one, ← Nat.cast_add, Nat.add_sub_cancel' hpos]