case inl
n : ℕ
⊢ List.toFinset (factors 0) = filter Prime (divisors 0)

case inr
n✝ n : ℕ
hn : n > 0
⊢ List.toFinset (factors n) = filter Prime (divisors n)
n✝ n : ℕ
⊢ List.toFinset (factors n) = filter Prime (divisors n)
rcases n.eq_zero_or_pos with (rfl | hn)
no goals
case inl
n : ℕ
⊢ List.toFinset (factors 0) = filter Prime (divisors 0)
simp
case inr.a
n✝ n : ℕ
hn : n > 0
q : ℕ
⊢ q ∈ List.toFinset (factors n) ↔ q ∈ filter Prime (divisors n)
case inr
n✝ n : ℕ
hn : n > 0
⊢ List.toFinset (factors n) = filter Prime (divisors n)
ext q
no goals
case inr.a
n✝ n : ℕ
hn : n > 0
q : ℕ
⊢ q ∈ List.toFinset (factors n) ↔ q ∈ filter Prime (divisors n)
simpa [hn, hn.ne', mem_factors] using and_comm