apply Finset.card_le_mul_card_image_of_maps_to (A_maps_to_offDiag_judgePair r)
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
⊢ (A r).card ≤ k * Finset.univ.offDiag.card
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
⊢ ∀ a ∈ Finset.univ.offDiag, (Finset.filter (fun x => x.judgePair = a) (A r)).card ≤ k