case inl
p : ℕ
h : p ∈ (factorization 0).support
⊢ p ∣ 0

case inr
n p : ℕ
h : p ∈ (factorization n).support
hn : n ≠ 0
⊢ p ∣ n
n p : ℕ
h : p ∈ (factorization n).support
⊢ p ∣ n
rcases eq_or_ne n 0 with (rfl | hn)
no goals
case inr
n p : ℕ
h : p ∈ (factorization n).support
hn : n ≠ 0
⊢ p ∣ n
simp [← mem_factors_iff_dvd hn (prime_of_mem_factorization h), factor_iff_mem_factorization.mp h]
no goals
case inl
p : ℕ
h : p ∈ (factorization 0).support
⊢ p ∣ 0
simp