apply Finset.mem_univ
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
z : ℕ
hJ : Fintype.card J = 2 * z + 1
a✝¹ : AgreedTriple C J
a✝ : a✝¹ ∈ A r
⊢ a✝¹.1 ∈ Finset.univ
no goals