Choose s conflict alpha

lemma choose_s_conflict_alpha (hn : 1 ≤ n) (αᵢ : ZMod p)    (srs : Vector G₁ (n + 1) × Vector G₂ 2) :    ¬ αᵢ ∈ chooseSConflict αᵢ srs hn := by  unfold chooseSConflict  set arr := (Array.range p).filterMap fun i =>    if h : i < p then      let x : ZMod p := (⟨i, h⟩ : Fin p)      if srs.1[0] ^ x.val ≠ srs.1[1]'(Nat.lt_add_of_pos_left hn) ∧ x ≠ αᵢ then some x      else none    else none  simp only [List.mem_toFinset]  intro hmem  have htoList : (arr.take n).toList = arr.toList.take n := by simp [Array.take]  rw [htoList] at hmem  have hmem := (List.take_sublist n arr.toList).subset hmem  simp only [arr, Array.toList_filterMap, Array.toList_range, List.mem_filterMap] at hmem  obtain ⟨i, -, hi⟩ := hmem  split at hi  · split at hi    · next _ hcond => exact absurd (Option.some.inj hi) hcond.2    · simp at hi  · simp at hi