constructor
x : ℕ
⊢ x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ {m | Even m}
case mp
x : ℕ
⊢ x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m} → x ∈ {m | Even m}

case mpr
x : ℕ
⊢ x ∈ {m | Even m} → x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m}