Find query with srs power success

lemma find_query_with_srs_power_success {L : ℕ} (hn : 1 ≤ n)    (srs : Vector G₁ (n + 1) × Vector G₂ 2) (queryOf : Fin L → ZMod p) {α : ZMod p}    (hfs : 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) = some α) :    srs.1[0] ^ α.val = srs.1[1]'(Nat.lt_add_of_pos_left hn) := by  obtain ⟨_, i, _, _, hbody, _⟩ := List.findSome?_eq_some_iff.mp hfs  by_cases hif : srs.1[0] ^ (queryOf i).val = srs.1[1]'(Nat.lt_add_of_pos_left hn)  · rw [if_pos hif] at hbody    simp only [Option.some.injEq] at hbody    rw [← hbody]    exact hif  · rw [if_neg hif] at hbody    exact absurd hbody (by simp)