T sdh game eq

lemma t_sdh_game_eq {n : ℕ} {AuxState : Type} [SampleableType G₁]    (adversary : KzgBindingAdversary p G₁ G₂ n unifSpec AuxState) :    Pr[Groups.tSdhCondition (p := p) (g₁ := g₁) |      mapBindingToTsdh (p := p) (n := n) <$> bindingGameExt (g₁ := g₁) (g₂ := g₂)        AuxState adversary        (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing))]    = Groups.tSdhExperiment (g₁ := g₁) (g₂ := g₂) n      (bindingReduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) AuxState        adversary) := by  let scheme := kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)  simp only [Groups.tSdhExperiment, Groups.tSdhGame]  congr 1  let pSpec' : ProtocolSpec 1 := ⟨!v[.P_to_V], !v[G₁]⟩  let impl : QueryImpl _ (StateT unifSpec.QueryCache ProbComp) :=    QueryImpl.addLift      (randomOracle : QueryImpl unifSpec (StateT unifSpec.QueryCache ProbComp))      (challengeQueryImpl (pSpec := pSpec'))  dsimp only [bindingGameExt, bindingReduction, kzg, OptionT.mk, pSpec', impl, scheme,    OptionT.run_map]  convert OptionT.map_mk_bind_eq_of_body      (sample := (Groups.sampleNonzeroZMod (p := p) : ProbComp (ZMod p)))      (body₁ := fun τ => (simulateQ impl (do        let srs := Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ        let ⟨cm, query, resp₁, resp₂, st₁, st₂⟩ ← liftComp (adversary.claim srs) _        let reduction := Reduction.mk (adversary.prover srs) (scheme.opening (srs, srs)).verifier        let result₁ ← (reduction.run          (cm, (⟨query, resp₁⟩ :            (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) × OracleInterface.Response q))          st₁).run        let result₂ ← (reduction.run          (cm, (⟨query, resp₂⟩ :            (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) × OracleInterface.Response q))          st₂).run        let accept₁ := result₁.map (fun result => result.2) |>.getD false        let accept₂ := result₂.map (fun result => result.2) |>.getD false        let proof₁ : G₁ := result₁.map (fun result => result.1.1 0) |>.getD (1 : G₁)        let proof₂ : G₁ := result₂.map (fun result => result.1.1 0) |>.getD (1 : G₁)        pure (some (τ, srs, cm, query, resp₁, resp₂, accept₁, accept₂, proof₁,          proof₂)))).run' (∅ : unifSpec.QueryCache))      (body₂ := fun τ => (simulateQ impl (do        let srs := Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ        let ⟨cm, query, resp₁, resp₂, st₁, st₂⟩ ← liftComp (adversary.claim srs) _        let reduction := Reduction.mk (adversary.prover srs) (scheme.opening (srs, srs)).verifier        let result₁ ← (reduction.run          (cm, (⟨query, resp₁⟩ :            (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) × OracleInterface.Response q))          st₁).run        let result₂ ← (reduction.run          (cm, (⟨query, resp₂⟩ :            (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) × OracleInterface.Response q))          st₂).run        let accept₁ := result₁.map (fun result => result.2) |>.getD false        let accept₂ := result₂.map (fun result => result.2) |>.getD false        let proof₁ : G₁ := result₁.map (fun result => result.1.1 0) |>.getD (1 : G₁)        let proof₂ : G₁ := result₂.map (fun result => result.1.1 0) |>.getD (1 : G₁)        pure (some (mapBindingInstanceToTsdh (p := p) (n := n)          (srs, cm, query, resp₁, resp₂, accept₁, accept₂, proof₁, proof₂))))).run'            (∅ : unifSpec.QueryCache))      (f := mapBindingToTsdh (p := p) (n := n))      (post := fun τ ((c, h) : ZMod p × G₁) => (τ, c, h))      (hBody := by        intro τ        dsimp only        refine StateT.map_run'_eq_of_map_eq (∅ : unifSpec.QueryCache) ?_        simp only [simulateQ_bind, simulateQ_pure, map_eq_bind_pure_comp, bind_assoc]        congr 1) using 1 <;> rfl