aesop
case H.a.a
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
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝.2.2 = x₂✝.2.2
no goals