Filter map conflict nodup

lemma filter_map_conflict_nodup    (αᵢ : ZMod p) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (hn : 1 ≤ n) :    ((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).toList.Nodup := by  rw [Array.toList_filterMap, Array.toList_range]  apply List.Nodup.filterMap _ List.nodup_range  intro a a' b hb hb'  simp only [Option.mem_def] at hb hb'  -- Extract a < p from hb (outer dite must take the then-branch)  have ha : a < p := by    by_contra h; push Not at h; rw [dif_neg (by omega)] at hb; simp at hb  have ha' : a' < p := by    by_contra h; push Not at h; rw [dif_neg (by omega)] at hb'; simp at hb'  -- Both branches must hit `some x`, giving `b = ↑↑⟨a, ha⟩` and `b = ↑↑⟨a', ha'⟩`.  simp only [ha, ha', dite_true] at hb hb'  split at hb <;> simp at hb  split at hb' <;> simp at hb'  -- hb : ↑↑⟨a, ha⟩ = b, hb' : ↑↑⟨a', ha'⟩ = b  have hval := congr_arg ZMod.val (hb.trans hb'.symm)  simp only [ZMod.val_natCast, Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt ha'] at hval  exact hval