Arsdh game eq

lemma arsdh_game_eq {n L : ℕ} {AuxState : Type} [SampleableType G₁]    (hn : 1 ≤ n) (adversary : KzgFunctionBindingAdversary p G₁ G₂ n unifSpec L AuxState) :  Pr[(Groups.arsdhCondition n) |      mapFunctionBindingToArsdh hn <$> functionBindingGameExt (g₁ := g₁) (g₂ := g₂)        AuxState adversary (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing))]    = Groups.arsdhExperiment (g₁ := g₁) (g₂ := g₂) n      (reduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) L hn AuxState adversary) := by  let scheme := kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)  simp only [Groups.arsdhExperiment, Groups.arsdhGame]  unfold Groups.arsdhCondition  simp only  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'))  simpa only [functionBindingGameExt, reduction, kzg, OptionT.mk, pSpec', impl, scheme,      OptionT.run_map] using    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 claimResult ← liftComp (adversary.claim srs) _        let cm := claimResult.1        let queryOf := claimResult.2.1        let responseOf := claimResult.2.2.1        let stateOf := claimResult.2.2.2        let reduction := Reduction.mk (adversary.prover srs) (scheme.opening (srs, srs)).verifier        let (resultPairs : Option (Fin L → Bool × G₁)) ← reduction.allOutputs          (fun ((transcript_data, verifier_accept) :            (FullTranscript ⟨!v[.P_to_V], !v[G₁]⟩ × Bool × Unit) × Bool) =>            (verifier_accept, transcript_data.1 0))          (fun i => (cm, (⟨queryOf i, responseOf i⟩ :            (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×              OracleInterface.Response q))) stateOf        let accepts : Option (Fin L → Bool) :=          resultPairs.map (fun resultOf => fun i => (resultOf i).1)        let proofs : Option (Fin L → G₁) :=          resultPairs.map (fun resultOf => fun i => (resultOf i).2)        pure (accepts.bind (fun accepts => proofs.map (fun proofs =>          (τ, srs, cm, queryOf, ((fun i => responseOf i) : Fin L → ZMod p), accepts, proofs))))      )).run' (∅ : unifSpec.QueryCache))      (body₂ := fun τ => (simulateQ impl (do        let srs := Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ        let claimResult ← liftComp (adversary.claim srs) _        let cm := claimResult.1        let queryOf := claimResult.2.1        let responseOf := claimResult.2.2.1        let stateOf := claimResult.2.2.2        let reduction := Reduction.mk (adversary.prover srs) (scheme.opening (srs, srs)).verifier        let (resultPairs : Option (Fin L → Bool × G₁)) ← reduction.allOutputs          (fun ((transcript_data, verifier_accept) :            (FullTranscript ⟨!v[.P_to_V], !v[G₁]⟩ × Bool × Unit) × Bool) =>            (verifier_accept, transcript_data.1 0))          (fun i => (cm, (⟨queryOf i, responseOf i⟩ :            (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×              OracleInterface.Response q))) stateOf        return resultPairs.map (fun resultOf =>          mapFunctionBindingInstanceToArsdhInst hn            (srs, cm, queryOf, responseOf, (fun i => (resultOf i).1), (fun i => (resultOf i).2)))      )).run' (∅ : unifSpec.QueryCache))      (f := mapFunctionBindingToArsdh hn)      (post := fun τ ((S, h₁, h₂) : Finset (ZMod p) × G₁ × G₁) => (τ, S, h₁, 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        funext claimResult        congr 1        funext resultPairs        cases resultPairs <;> rfl)