Tsum prob Output simulate Q run mul of rel

theorem tsum_probOutput_simulateQ_run_mul_of_rel    {ι : Type} {spec : OracleSpec ι} {σ : Type}    (impl : QueryImpl spec (StateT σ ProbComp))    {γ : Type} (oa : OracleComp spec γ)    (Rel : σ → σ → Prop)    (hstep : ∀ (t : spec.Domain) (s₁ s₂ : σ), Rel s₁ s₂ →      ∀ (K : spec.Range t → σ → ℝ≥0∞),        (∀ (b : spec.Range t) (t₁ t₂ : σ), Rel t₁ t₂ → K b t₁ = K b t₂) →        (∑' p : spec.Range t × σ, Pr[= p | (impl t).run s₁] * K p.1 p.2)          = ∑' p : spec.Range t × σ, Pr[= p | (impl t).run s₂] * K p.1 p.2) :    ∀ (F : γ → σ → ℝ≥0∞), (∀ (g : γ) (s₁ s₂ : σ), Rel s₁ s₂ → F g s₁ = F g s₂) →      ∀ (s₁ s₂ : σ), Rel s₁ s₂ →        (∑' z : γ × σ, Pr[= z | (simulateQ impl oa).run s₁] * F z.1 z.2)          = ∑' z : γ × σ, Pr[= z | (simulateQ impl oa).run s₂] * F z.1 z.2 := by  induction oa using OracleComp.inductionOn with  | pure a =>      intro F hF s₁ s₂ hs      simp only [simulateQ_pure, StateT.run_pure, tsum_probOutput_pure_mul]      exact hF a s₁ s₂ hs  | query_bind t ob ih =>      intro F hF s₁ s₂ hs      simp only [simulateQ_bind, simulateQ_spec_query, StateT.run_bind, tsum_probOutput_bind_mul]      set K : spec.Range t → σ → ℝ≥0∞ := fun b u =>        ∑' z : γ × σ, Pr[= z | (simulateQ impl (ob b)).run u] * F z.1 z.2 with hK      have hKinv : ∀ (b : spec.Range t) (t₁ t₂ : σ), Rel t₁ t₂ → K b t₁ = K b t₂ :=        fun b t₁ t₂ ht => ih b F hF t₁ t₂ ht      exact hstep t s₁ s₂ hs K hKinv