simp only [mem_filter, mem_primeFactors, ne_eq, hn, not_false_eq_true, and_true,
  ne_zero_of_dvd_ne_zero hn hmn, and_congr_left_iff, and_iff_left_iff_imp]
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∈ filter (fun p => p ∣ m) n.primeFactors ↔ p ∈ m.primeFactors
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∣ m → p.Prime → p ∣ n