simp only [A, Finset.mem_univ, Finset.mem_filter, Finset.mem_image, true_and_iff, exists_prop]
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ p ∈ Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ ↔
    p ∈ Finset.image Prod.snd (Finset.filter (fun a => a.contestant = c) (A r))
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ JudgePair.Agree r p c ∧ p.Distinct ↔
    ∃ a,
      ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧
            (AgreedTriple.judgePair a).Distinct) ∧
          AgreedTriple.contestant a = c) ∧
        a.2 = p