Theorem: Nat.filter_primeFactors (PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean)

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

State before:
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∈ filter (fun p => p ∣ m) n.primeFactors ↔ p ∈ m.primeFactors
Tactic:
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]
State after:
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∣ m → p.Prime → p ∣ n

State before:
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∣ m → p.Prime → p ∣ n
Tactic:
exact fun h _ ↦ h.trans hmn
State after:
no goals