aesop
case a.mp
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.filter (fun c => JudgePair.Agree r p c) Finset.univ
⊢ (c, p) ∈
      Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ) ∧
    AgreedTriple.contestant (c, p) = c
no goals