Lean-Workbook Syntax 67158: Congruence between even and odd products

$\prod_{i=0}^{999}(2i+2)-\prod_{i=0}^{999}(2i+1)\equiv0\pmod{2001}$.

Source: Lean-Workbook row lean_workbook_plus_67158 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.