case pos
n : ℕ
hn : n = 0
⊢ ∏ p in toFinset (factors n), p ∣ n

case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p in toFinset (factors n), p ∣ n
n : ℕ
⊢ ∏ p in toFinset (factors n), p ∣ n
by_cases hn : n = 0
no goals
case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p in toFinset (factors n), p ∣ n
simpa [prod_factors hn] using Multiset.toFinset_prod_dvd_prod (n.factors : Multiset ℕ)
case pos

⊢ ∏ p in toFinset (factors 0), p ∣ 0
case pos
n : ℕ
hn : n = 0
⊢ ∏ p in toFinset (factors n), p ∣ n
subst hn
no goals
case pos

⊢ ∏ p in toFinset (factors 0), p ∣ 0
simp