Function binding cond ext output maps to arsdh

lemma function_binding_cond_ext_output_maps_to_arsdh {n L : ℕ} {AuxState : Type}    [SampleableType G₁]    (hn : 1 ≤ n) (hp : p ≥ n + 2) (hg₁ : g₁ ≠ 1) (hpair : pairing g₁ g₂ ≠ 0)    (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))))    (hFBcond : functionBindingCondExt n L (τ, srs, cm, queryOf, responseOf, accepts, proofs)) :    ((Groups.arsdhCondition n) ∘ mapFunctionBindingToArsdh hn)      (τ, srs, cm, queryOf, responseOf, accepts, proofs) := by  have hsrs : srs = Groups.PowerSrs.generate n τ (g₂ := g₂) (g₁ := g₁) := by    exact function_binding_game_ext_support_srs (pairing := pairing) adversary hgame  have hgen : srs.1[0] ≠ 1 := by    rw [hsrs]    simp only [Groups.PowerSrs.generate, Groups.PowerSrs.tower, Nat.reduceAdd, Vector.getElem_ofFn,      pow_zero, pow_one, ne_eq]    exact hg₁  have hverify_all : ∀ i : Fin L, accepts i = true →      KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)        srs.2 cm (proofs i) (queryOf i) (responseOf i) := by    exact function_binding_game_ext_support_verify_all (pairing := pairing) adversary hgame  unfold mapFunctionBindingToArsdh  unfold mapFunctionBindingInstanceToArsdhInst mapFunctionBindingInstanceToArsdhInstAux  simp only [FunctionBindingExtTranscript.ofTuple, Option.pure_def, beq_iff_eq,    Option.bind_eq_bind, Function.comp_apply]  cases hfc : findConflict queryOf responseOf with  | some c =>      obtain ⟨i₁, i₂⟩ := c      simp only [Option.getD_some]      exact function_binding_conflicting_evaluations_branch_maps_to_arsdh        (pairing := pairing) hn hp hpair hsrs hgen hverify_all hFBcond hfc  | none =>      cases hfs : List.findSome?        (fun i ↦ if srs.1[0] ^ (queryOf i).val = srs.1[1] then some (queryOf i) else none)        (List.finRange L) with      | some α₁ =>          simp only [Option.getD_some]          have hcond : srs.1[0] ^ α₁.val = srs.1[1]'(Nat.lt_add_of_pos_left hn) := by            exact find_query_with_srs_power_success hn srs queryOf hfs          exact function_binding_query_eq_tau_branch_maps_to_arsdh            (g₁ := g₁) (g₂ := g₂) hn hp hg₁ hsrs hgen hcond      | none =>          -- The interpolation has degree ≥ n + 1, since otherwise its first n + 1          -- coefficients would witness a degree-`n` polynomial fitting all pairs,          -- contradicting the function-binding hypothesis `hFBcond`.          let R := queryReps queryOf          have hRinj : Set.InjOn queryOf ↑R := queryReps_injOn queryOf          have hRnoData : ¬ ∃ d : Fin (n + 1) → ZMod p,              ∀ i ∈ R, (CPolynomial.ofFn d).eval (queryOf i) = responseOf i := by            exact no_data_queryReps_of_function_binding_cond hFBcond hfc          have hRdeg : (↑(n + 1) : WithBot ℕ) ≤              (CLagrange.interpolate R queryOf responseOf).degree := by            exact interpolate_degree_ge_of_no_data R hRinj hRnoData          have hRcard : n + 1 < R.card := by            exact finset_card_gt_of_interpolate_degree_ge R queryOf responseOf hRinj hRdeg          cases hfa : findA R (n + 1) queryOf responseOf with          | some a =>              have hres_a : some a = findA R (n + 1) queryOf responseOf := hfa.symm              have hAsub : a ⊆ R := find_a_subset R a (n + 1) queryOf responseOf hres_a              have hAinj : Set.InjOn queryOf ↑a := hRinj.mono hAsub              cases hfs' : findS n a cm srs queryOf responseOf with              | some a' =>                  have hres_s : some a' = findS n a cm srs queryOf responseOf := hfs'.symm                  have hSsub : a' ⊆ a :=                    find_s_subset n cm a a' srs queryOf responseOf hres_s                  have hSinj : Set.InjOn queryOf ↑a' := hAinj.mono hSsub                  simp only [hfs', Option.bind, Option.getD_some]                  exact function_binding_interpolation_branch_maps_to_arsdh                    (pairing := pairing) hn hpair hsrs hgen hverify_all hFBcond hSinj hfs' hfs              | none =>                  -- `findS` failed: contradicts `find_s_successful`.                  exfalso                  have hAdeg :=                    find_a_deg R a (n + 1) queryOf responseOf hres_a                  have hsome :=                    find_s_successful (g₁ := g₁) n τ cm a queryOf responseOf srs hsrs                      hgen                      (by exact_mod_cast hAdeg) hAinj hn                  rw [hfs'] at hsome                  simp at hsome          | none =>              -- `findA` failed: contradicts `find_a_successful` via `hRdeg`.              exfalso              have hsome :=                find_a_successful R (n + 1) queryOf responseOf hRcard hRinj hRdeg              rw [hfa] at hsome              simp at hsome