rfl
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
⊢ Finset.univ.card = Fintype.card J
no goals