rw [A_fibre_over_judgePair r h]
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
⊢ (agreedContestants r p).card = (Finset.filter (fun a => a.judgePair = p) (A r)).card
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
⊢ (Finset.image AgreedTriple.contestant (Finset.filter (fun a => a.judgePair = p) (A r))).card =
    (Finset.filter (fun a => a.judgePair = p) (A r)).card