Function binding game ext support srs

lemma function_binding_game_ext_support_srs {n L : ℕ} {AuxState : Type} [SampleableType G₁]    (adversary : KzgFunctionBindingAdversary p G₁ G₂ n unifSpec L AuxState)    {τ : ZMod p} {srs : Vector G₁ (n + 1) × Vector G₂ 2} {cm : G₁}    {queryOf responseOf : Fin L → ZMod p} {accepts : Fin L → Bool} {proofs : Fin L → G₁}    (hgame : (τ, srs, cm, queryOf, responseOf, accepts, proofs) ∈      support (functionBindingGameExt (g₁ := g₁) (g₂ := g₂) AuxState adversary        (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)))) :    srs = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ := by  simp only [functionBindingGameExt, kzg] at hgame  obtain ⟨τ', _, hgame⟩ := OptionT.mem_support_bind_mk _ _ hgame  refine OptionT.aux_mem_support_simulateQ_run' _ _ _    (fun y => y.2.1 = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n y.1) ?_ hgame  intro x hx y hxy  rw [hxy] at hx  rw [mem_support_bind_iff] at hx  obtain ⟨⟨cm', queryOf', responseOf', stateOf'⟩, _, hx⟩ := hx  rw [mem_support_bind_iff] at hx  obtain ⟨resultPairs, _, hx⟩ := hx  have hx' : some y =      ((Option.map (fun resultOf i => (resultOf i).1) resultPairs).bind fun accepts =>        Option.map          (fun proofs =>            (τ', Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ', cm', queryOf',              (fun i => responseOf' i), accepts, proofs))          (Option.map (fun resultOf i => (resultOf i).2) resultPairs)) := by    exact (mem_support_pure_iff _ _).mp hx  cases hres : resultPairs with  | none => simp [hres] at hx'  | some resultOf =>      simp only [hres, Option.map_some, Option.bind_some] at hx'      have hy := Option.some.inj hx'      rw [hy]