Theorem: Imo1998P2.A_maps_to_offDiag_judgePair (Compfiles/Imo1998P2.lean)

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
a : AgreedTriple C J
⊢ a ∈ A r → a.judgePair ∈ Finset.univ.offDiag
Tactic:
simp [A, Finset.mem_offDiag]
State after:
no goals