simp only [gt_iff_lt, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_exists, not_and]
case h
x : ℕ × ℕ
⊢ x ∈ {x | ∃ n > 0, next^[n] x = x} ↔ x ∈ ∅
case h
x : ℕ × ℕ
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬next^[x_1] x = x