ext c
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.filter (fun c => JudgePair.Agree r p c) Finset.univ =
    Finset.image AgreedTriple.contestant
      (Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ))
case 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
c : C
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ ↔
    c ∈
      Finset.image AgreedTriple.contestant
        (Finset.filter (fun a => a.judgePair = p)
          (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ))