Function binding game ext support verify all

lemma function_binding_game_ext_support_verify_all {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)))) :    ∀ i : Fin L, accepts i = true →      KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)        srs.2 cm (proofs i) (queryOf i) (responseOf i) := by  simp only [functionBindingGameExt, kzg] at hgame  intro i_idx hai  let P : ZMod p × (Vector G₁ (n + 1) × Vector G₂ 2) × G₁ ×      (Fin L → ZMod p) × (Fin L → ZMod p) × (Fin L → Bool) × (Fin L → G₁) → Prop :=    fun y => y.2.2.2.2.2.1 i_idx = true →      KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)        y.2.1.2 y.2.2.1 (y.2.2.2.2.2.2 i_idx) (y.2.2.2.1 i_idx)          (y.2.2.2.2.1 i_idx)  have hP : P (τ, srs, cm, queryOf, responseOf, accepts, proofs) := by    obtain ⟨τ_v, _, hgame⟩ := OptionT.mem_support_bind_mk _ _ hgame    refine OptionT.aux_mem_support_simulateQ_run' _ _ _ P ?_ hgame    intro x hx ⟨τ', srs', cm', queryOf', responseOf', accepts', proofs'⟩ hxeq hai'    rw [hxeq] at hx    rw [mem_support_bind_iff] at hx    obtain ⟨claim_v, _, hx⟩ := hx    let cm_v := claim_v.1    let queryOf_v := claim_v.2.fst    let responseOf_v := claim_v.2.2.1    let stateOf_v := claim_v.2.2.2    rw [mem_support_bind_iff] at hx    obtain ⟨opts_v, hopts, hx⟩ := hx    have hx' : some (τ', srs', cm', queryOf', responseOf', accepts', proofs') =        ((Option.map (fun resultOf i => (resultOf i).1) opts_v).bind fun accepts =>          Option.map            (fun proofs =>              (τ_v, Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v, claim_v.1,                claim_v.2.fst, (fun i => claim_v.2.2.1 i), accepts, proofs))            (Option.map (fun resultOf i => (resultOf i).2) opts_v)) := by      exact (mem_support_pure_iff _ _).mp hx    cases hres : opts_v 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'      have h_srs : srs' = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v := by        simpa using congrArg (fun y => y.2.1) hy      have h_cm : cm' = cm_v := by        simpa using congrArg (fun y => y.2.2.1) hy      have h_q : queryOf' = queryOf_v := by        simpa using congrArg (fun y => y.2.2.2.1) hy      have h_r : responseOf' = fun i => responseOf_v i := by        simpa using congrArg (fun y => y.2.2.2.2.1) hy      have h_a : accepts' = fun i => (resultOf i).1 := by        simpa using congrArg (fun y => y.2.2.2.2.2.1) hy      have h_p : proofs' = fun i => (resultOf i).2 := by        simpa using congrArg (fun y => y.2.2.2.2.2.2) hy      obtain ⟨result, hresult, hres_eq⟩ :=        Reduction.support_allOutputs_index          (fun ((transcript_data, verifier_accept) :            (FullTranscript ⟨!v[.P_to_V], !v[G₁]⟩ × Bool × Unit) × Bool) =>            (verifier_accept, transcript_data.1 0))          (fun i => (cm_v, (⟨queryOf_v i, responseOf_v i⟩ :            (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×              OracleInterface.Response q))) stateOf_v          (Reduction.mk            (adversary.prover (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v))            ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).opening              (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v,               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v)).verifier)          hopts hres i_idx      obtain ⟨td_data, va⟩ := result      have hverif :=        Reduction.support_run_pure_verifier          (Reduction.mk            (adversary.prover (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v))            ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).opening              (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v,               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v)).verifier)          (fun stmt td =>            KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)              (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v).2 stmt.1              (td ⟨0, by decide⟩) stmt.2.1 stmt.2.2)          (by intros; rfl)          (cm_v, ⟨queryOf_v i_idx, responseOf_v i_idx⟩)          (stateOf_v i_idx)          hresult rfl      have hva_eq_v : va = (resultOf i_idx).1 := congrArg Prod.fst hres_eq      have htd_eq_v : td_data.1 0 = (resultOf i_idx).2 := congrArg Prod.snd hres_eq      have h_a_i : accepts' i_idx = (resultOf i_idx).1 := by        have := congrFun h_a i_idx        simpa using this      have h_p_i : proofs' i_idx = (resultOf i_idx).2 := by        have := congrFun h_p i_idx        simpa using this      have h_va_acc : va = accepts' i_idx := by rw [hva_eq_v, ← h_a_i]      have h_td_prf : td_data.1 0 = proofs' i_idx := by rw [htd_eq_v, ← h_p_i]      have hva_true : va = true := h_va_acc.trans hai'      have h_q_i : queryOf' i_idx = queryOf_v i_idx := by        have := congrFun h_q i_idx        simpa using this      have h_r_i : responseOf' i_idx = responseOf_v i_idx := by        have := congrFun h_r i_idx        simpa using this      change KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)        srs'.2 cm' (proofs' i_idx) (queryOf' i_idx) (responseOf' i_idx)      rw [h_srs, h_cm, ← h_td_prf, h_q_i, h_r_i]      have heq : KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)          (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v).2 cm_v          (td_data.1 ⟨0, by decide⟩) (queryOf_v i_idx) (responseOf_v i_idx)            = true := hverif.symm.trans hva_true      exact heq  exact hP hai