Function binding interpolation branch maps to arsdh

lemma function_binding_interpolation_branch_maps_to_arsdh {n L : ℕ}    (hn : 1 ≤ n) (hpair : pairing g₁ g₂ ≠ 0)    {τ : 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₁}    (hsrs : srs = Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)    (hgen : srs.1[0] ≠ 1)    (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))    (hFBcond : functionBindingCondExt n L (τ, srs, cm, queryOf, responseOf, accepts, proofs))    {A S : Finset (Fin L)}    (hqueryS : Set.InjOn queryOf ↑S)    (hresS : findS n A cm srs queryOf responseOf = some S)    (hfs_none : List.findSome?        (fun i ↦ if srs.1[0] ^ (queryOf i).val = srs.1[1]'(Nat.lt_add_of_pos_left hn)                  then some (queryOf i) else none)        (List.finRange L) = none) :    Groups.arsdhCondition n      (τ, (interpolationArsdhOutput (p := p) (G₂ := G₂) S        ({ srs := srs, cm := cm, queryOf := queryOf, responseOf := responseOf,           accepts := accepts, proofs := proofs } :          FunctionBindingExtTranscript (p := p) n L G₁ G₂)).toTuple) := by  simp only [interpolationArsdhOutput, FunctionBindingArsdhOutput.toTuple,    Groups.arsdhCondition, ne_eq, one_div]  have hresS_symm : some S = findS n A cm srs queryOf responseOf := hresS.symm  refine ⟨?_, ?_, ?_, ?_⟩  · rw [Finset.card_image_of_injOn hqueryS]    exact find_s_card n cm A S srs queryOf responseOf hresS_symm  · have hτneq_all : ∀ i : Fin L, queryOf i ≠ τ :=      query_ne_tau_of_find_query_with_srs_power_none        (g₁ := g₁) hn τ srs queryOf hsrs hfs_none    have hτ_not_image : τ ∉ S.image queryOf := by      simp only [Finset.mem_image, not_exists, not_and]      intro i _      exact hτneq_all i    exact prod_x_sub_c_eval_ne_zero hτ_not_image  · intro hdiv    have hcm_eq_c' : cm =        commit srs.1 ((CLagrange.interpolate S queryOf responseOf).val.coeff ∘ Fin.val) :=      div_eq_one.mp hdiv    exact (find_s_diverges n cm A S queryOf responseOf srs hresS_symm) hcm_eq_c'.symm  · have hcard : S.card = n + 1 :=      find_s_card n cm A S srs queryOf responseOf hresS_symm    have hdeg : (CLagrange.interpolate S queryOf responseOf).degree ≤ (n : WithBot ℕ) := by      exact interp_degree_le_of_card S queryOf responseOf hqueryS hcard    have hS_ne : S.Nonempty := by      rw [← Finset.card_pos, hcard]; exact Nat.succ_pos _    have hτneq : ∀ i ∈ S, queryOf i ≠ τ := by      intro i _      exact query_ne_tau_of_find_query_with_srs_power_none        (g₁ := g₁) hn τ srs queryOf hsrs hfs_none i    have hVer : ∀ i ∈ S,        KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)          srs.2 cm (proofs i) (queryOf i) (responseOf i) := by      intro i _      exact hverify_all i (hFBcond.1 i (Finset.mem_univ _))    have key := h1_zs_eq_h2_prime (g₁ := g₁) (g₂ := g₂) (pairing := pairing)      n τ cm S queryOf responseOf proofs srs hn hsrs hτneq hVer      hgen hpair hdeg hS_ne hqueryS    simpa only [one_div] using key