Mathlib v3 is deprecated. Go to Mathlib v4

Theorem judge_pair.agree_iff_same_rating

Modification history