rfl
case a.h
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
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ Finset.univ.card = Fintype.card J
no goals