Function binding game ext eq function binding game

lemma function_binding_game_ext_eq_function_binding_game {n L : ℕ} {AuxState : Type}    [SampleableType G₁]    (adversary : KzgFunctionBindingAdversary p G₁ G₂ n unifSpec L AuxState) :    Pr[Commitment.functionBindingCondition (Data := Fin (n + 1) → ZMod p) |      Commitment.functionBindingGame (init := pure ∅) (impl := randomOracle) (hn := rfl)        (AuxState := AuxState)        (scheme := kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing))        (adversary := adversary)]    = Pr[functionBindingCondExt n L |      functionBindingGameExt (g₁ := g₁) (g₂ := g₂) AuxState adversary        (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing))] := by  -- Define the projection from the extended output tuple to the basic output tuple.  let proj : (ZMod p × (Vector G₁ (n + 1) × Vector G₂ 2) × G₁ ×      (Fin L → ZMod p) × (Fin L → ZMod p) × (Fin L → Bool) × (Fin L → G₁)) →      ((queryOf : Fin L → OracleInterface.Query (Fin (n + 1) → ZMod p)) ×        ((i : Fin L) → OracleInterface.Response (queryOf i)) × (Fin L → Bool)) :=    fun x => ⟨x.2.2.2.1, x.2.2.2.2.1, x.2.2.2.2.2.1⟩  -- The extended condition factors through the projection.  have hcond_eq :      (functionBindingCondExt n L : _ → Prop) =        (Commitment.functionBindingCondition (Data := Fin (n + 1) → ZMod p)) ∘ proj := by    funext x    rcases x with ⟨_, _, _, _, _, _, _⟩    rfl  rw [hcond_eq]  -- Apply the OptionT bridge lemma with the run-level equality proved inline.  apply OptionT.probEvent_eq_of_run_map_eq _ _ proj    (Commitment.functionBindingCondition (Data := Fin (n + 1) → ZMod p))  simp only [Commitment.functionBindingGame, functionBindingGameExt, 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]  rw [hkeygen]  simp only [map_eq_bind_pure_comp, bind_assoc, pure_bind, Function.comp]  congr 1  funext τ  rw [← map_eq_bind_pure_comp, ← StateT.run'_map_comm, ← simulateQ_map]  simp only [map_eq_bind_pure_comp, bind_assoc, pure_bind, Function.comp]  congr 1  funext x  apply congr_fun  apply congr_arg  congr 1  funext x_1  rw [Reduction.allVerdicts_eq_map_allOutputs_fst (fun result =>    (result.1.1 0 : G₁))]  simp only [map_eq_bind_pure_comp, bind_assoc, Option.map_bind]  congr 1  funext resultPairs  cases resultPairs <;> rfl