rw [A_fibre_over_contestant r]
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
⊢ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card =
    (Finset.filter (fun a => a.contestant = c) (A r)).card
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
⊢ (Finset.image Prod.snd (Finset.filter (fun a => a.contestant = c) (A r))).card =
    (Finset.filter (fun a => a.contestant = c) (A r)).card