n p : ℕ
⊢ ¬p ∈ factors n ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
n p : ℕ
⊢ ↑(factorization n) p = 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
rw [← not_mem_support_iff, support_factorization, mem_toFinset]
case inl
p : ℕ
⊢ ¬p ∈ factors 0 ↔ ¬Prime p ∨ ¬p ∣ 0 ∨ 0 = 0

case inr
n p : ℕ
hn : n ≠ 0
⊢ ¬p ∈ factors n ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
n p : ℕ
⊢ ¬p ∈ factors n ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
rcases eq_or_ne n 0 with (rfl | hn)
no goals
case inl
p : ℕ
⊢ ¬p ∈ factors 0 ↔ ¬Prime p ∨ ¬p ∣ 0 ∨ 0 = 0
simp
no goals
case inr
n p : ℕ
hn : n ≠ 0
⊢ ¬p ∈ factors n ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
simp [hn, Nat.mem_factors, not_and_or, -not_and]