simp only [Finset.mem_filter, Finset.mem_image, Prod.exists] at h
case a.mpr
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
h :
  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))
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
case a.mpr
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
h :
  ∃ a a_1 b,
    (((a, a_1, b) ∈ Finset.univ ∧
          JudgePair.Agree r (AgreedTriple.judgePair (a, a_1, b)) (AgreedTriple.contestant (a, a_1, b)) ∧
            (AgreedTriple.judgePair (a, a_1, b)).Distinct) ∧
        AgreedTriple.judgePair (a, a_1, b) = p) ∧
      AgreedTriple.contestant (a, a_1, b) = c
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ