Query Reps exists

lemma queryReps_exists {L : ℕ} (query : Fin L → ZMod p) (i : Fin L) :    ∃ j ∈ queryReps query, query j = query i := by  let same : Finset (Fin L) := Finset.univ.filter fun j => query j = query i  have hsame_nonempty : same.Nonempty := ⟨i, by simp [same]⟩  let j := same.min' hsame_nonempty  have hjsame : j ∈ same := Finset.min'_mem same hsame_nonempty  have hjquery : query j = query i := (Finset.mem_filter.mp hjsame).2  refine ⟨j, ?_, hjquery⟩  simp only [queryReps, Finset.mem_filter, Finset.mem_univ, true_and]  intro k hk  exact Finset.min'_le same k (by simp [same, hk.trans hjquery])