Function binding query eq tau branch maps to arsdh

lemma function_binding_query_eq_tau_branch_maps_to_arsdh {n : ℕ}    (hn : 1 ≤ n) (hp : p ≥ n + 2) (hg₁ : g₁ ≠ 1)    {τ α : ZMod p} {srs : Vector G₁ (n + 1) × Vector G₂ 2}    (hsrs : srs = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)    (hgen : srs.1[0] ≠ 1)    (hpow : srs.1[0] ^ α.val = srs.1[1]'(Nat.lt_add_of_pos_left hn)) :    Groups.arsdhCondition n (τ, (queryEqTauArsdhOutput (p := p) n α srs).toTuple) := by  simp only [queryEqTauArsdhOutput, FunctionBindingArsdhOutput.toTuple,    Groups.arsdhCondition, ne_eq, one_div]  have hord : orderOf g₁ = p := Groups.orderOf_eq_prime_of_ne_one g₁ hg₁  have hα_τ : α = τ :=    zmod_eq_of_srs_power_eq (g₁ := g₁) hn srs hsrs hord hpow  refine ⟨?_, ?_, ?_, ?_⟩  · exact choose_s_middle_card hp α  · rw [← hα_τ]    exact choose_s_middle_eval_ne_zero α  · exact hgen  · rw [hα_τ]