ext p
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ filter (fun p => p ∣ m) n.primeFactors = m.primeFactors
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∈ filter (fun p => p ∣ m) n.primeFactors ↔ p ∈ m.primeFactors