unfold Set.InjOn
case 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
⊢ Set.InjOn AgreedTriple.contestant ↑(Finset.filter (fun a => a.judgePair = p) (A r))
case 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
⊢ ∀ ⦃x₁ : AgreedTriple C J⦄,
    x₁ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r)) →
      ∀ ⦃x₂ : AgreedTriple C J⦄,
        x₂ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r)) → x₁.contestant = x₂.contestant → x₁ = x₂