Binding game ext eq binding game

lemma binding_game_ext_eq_binding_game {n : ℕ} {AuxState : Type} [SampleableType G₁]    (adversary : KzgBindingAdversary p G₁ G₂ n unifSpec AuxState) :    Pr[Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p) |      Commitment.bindingGame (init := pure ∅) (impl := randomOracle) (AuxState := AuxState)        (scheme := kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing))        (adversary := adversary)]    = Pr[bindingCondExt (p := p) (n := n) | bindingGameExt (g₁ := g₁) (g₂ := g₂)      AuxState adversary (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing))] := by  let proj : BindingExtOutput (p := p) n G₁ G₂ → BindingOutput (p := p) n :=    fun ⟨_, _, _, query, resp₁, resp₂, accept₁, accept₂, _, _⟩ =>      ⟨query, resp₁, resp₂, accept₁, accept₂⟩  have hcond_eq :      (bindingCondExt (p := p) (n := n) : _ → Prop) =        (Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p)) ∘ proj := by    funext x    rcases x with ⟨_, _, _, _, _, _, _, _, _, _⟩    rfl  rw [hcond_eq]  apply OptionT.probEvent_eq_of_run_map_eq _ _ proj    (Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p))  simp only [Commitment.bindingGame, bindingGameExt, kzg, OptionT.run, OptionT.mk]  rw [pure_bind]  have hsample :      (simulateQ randomOracle (Groups.sampleNonzeroZMod (p := p))).run' ∅ =        Groups.sampleNonzeroZMod (p := p) :=    Groups.simulateQ_randomOracle_sampleNonzeroZMod (p := p)  have hkeygen :      (simulateQ randomOracle (do        let a ← Groups.sampleNonzeroZMod (p := p)        pure (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,          Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))).run' ∅        =      (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,        Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))          <$> Groups.sampleNonzeroZMod (p := p) := by    calc      (simulateQ randomOracle (do        let a ← Groups.sampleNonzeroZMod (p := p)        pure (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,          Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))).run' ∅          = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,              Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))              <$> (simulateQ randomOracle (Groups.sampleNonzeroZMod (p := p))).run' ∅ := by            rw [← StateT.run'_map_comm, ← simulateQ_map]            rfl      _ = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,              Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))              <$> Groups.sampleNonzeroZMod (p := p) := by            rw [hsample]  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'))  let sample : ProbComp (ZMod p) := Groups.sampleNonzeroZMod (p := p)  let bodyBase : ZMod p → OracleComp _ (Option (BindingOutput (p := p) n)) := fun τ => 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)      ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).opening        (srs, srs)).verifier    let accept₁ := (← (reduction.verdict      (cm, (⟨query, resp₁⟩ :        (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×          OracleInterface.Response q)) st₁).run).getD false    let accept₂ := (← (reduction.verdict      (cm, (⟨query, resp₂⟩ :        (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×          OracleInterface.Response q)) st₂).run).getD false    pure (some (⟨query, resp₁, resp₂, accept₁, accept₂⟩ : BindingOutput (p := p) n))  let bodyExt : ZMod p → OracleComp _ (Option (BindingExtOutput (p := p) n G₁ G₂)) :=    fun τ => 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)        ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).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₂))  rw [hkeygen]  simp only [map_eq_bind_pure_comp, bind_assoc, pure_bind, Function.comp]  change (OptionT.mk (do    let τ ← sample    (simulateQ impl (bodyBase τ)).run' (∅ : unifSpec.QueryCache))).run =      (OptionT.mk (do        let τ ← sample        let r ← (simulateQ impl (bodyExt τ)).run' (∅ : unifSpec.QueryCache)        pure (Option.map (proj) r))).run  simpa only [id_map] using    congrArg OptionT.run      (OptionT.map_mk_bind_eq_of_body        (sample := sample)        (body₁ := fun τ => (simulateQ impl (bodyBase τ)).run' (∅ : unifSpec.QueryCache))        (body₂ := fun τ => (simulateQ impl (bodyExt τ)).run' (∅ : unifSpec.QueryCache))        (f := id) (post := fun _ => proj)        (hBody := by          intro τ          rw [← StateT.run'_map_comm (Option.map id),            ← StateT.run'_map_comm (Option.map proj)]          apply congrArg (fun mx : StateT unifSpec.QueryCache ProbComp            (Option (BindingOutput (p := p) n)) => mx.run' ∅)          dsimp only [bodyBase, bodyExt]          rw [← simulateQ_map, ← simulateQ_map]          apply congrArg (simulateQ impl)          simp only [map_eq_bind_pure_comp, bind_assoc]          congr 1          funext claim          rcases claim with ⟨cm, query, resp₁, resp₂, st₁, st₂⟩          rw [Reduction.verdict_run_eq_map_run, Reduction.verdict_run_eq_map_run]          exact bind_two_option_project_get_d            (mx := ((Reduction.mk              (adversary.prover (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ))              ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).opening                (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ,                  Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)).verifier).run              (cm, (⟨query, resp₁⟩ :                (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×                  OracleInterface.Response q)) st₁).run)            (my := ((Reduction.mk              (adversary.prover (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ))              ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).opening                (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ,                  Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)).verifier).run              (cm, (⟨query, resp₂⟩ :                (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×                  OracleInterface.Response q)) st₂).run)            (fa := fun result : (FullTranscript pSpec' × Bool × Unit) × Bool => result.2)            (fb := fun result : (FullTranscript pSpec' × Bool × Unit) × Bool => result.2)            (da := false) (db := false)            (mkBase := fun accept₁ accept₂ =>              (⟨query, resp₁, resp₂, accept₁, accept₂⟩ : BindingOutput (p := p) n))            (mkExt := fun result₁ result₂ =>              (τ, Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ, cm, query,                resp₁, resp₂,                (Option.map (fun result => result.2) result₁).getD false,                (Option.map (fun result => result.2) result₂).getD false,                (Option.map (fun result => result.1.1 0) result₁).getD (1 : G₁),                (Option.map (fun result => result.1.1 0) result₂).getD (1 : G₁)))            (proj := proj) (by intro result₁ result₂; rfl)))