-- Mathlib/Data/Nat/Factorization/PrimePow.lean
theorem Nat.mul_divisors_filter_prime_pow {a b : ℕ} (hab : a.Coprime b) :
    (a * b).divisors.filter IsPrimePow = (a.divisors ∪ b.divisors).filter IsPrimePow

Proof state:
case inr.inl
a : ℕ
ha : a ≠ 0
hab : a = 1
⊢ Finset.filter IsPrimePow (a * 0).divisors = Finset.filter IsPrimePow (a.divisors ∪ divisors 0)

Tactic:
simp [hab, Finset.filter_singleton, not_isPrimePow_one]

Result:
no goals

Proof state:
case inr.inr.h
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (a * b).divisors ↔ n ∈ Finset.filter IsPrimePow (a.divisors ∪ b.divisors)

Tactic:
simp only [ha, hb, Finset.mem_union, Finset.mem_filter, Nat.mul_eq_zero, and_true, Ne,
  and_congr_left_iff, not_false_iff, Nat.mem_divisors, or_self_iff]

Result:
case inr.inr.h
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)

Proof state:
case inr.inl
a : ℕ
ha : a ≠ 0
hab : a.Coprime 0
⊢ Finset.filter IsPrimePow (a * 0).divisors = Finset.filter IsPrimePow (a.divisors ∪ divisors 0)

Tactic:
simp only [Nat.coprime_zero_right] at hab

Result:
case inr.inl
a : ℕ
ha : a ≠ 0
hab : a = 1
⊢ Finset.filter IsPrimePow (a * 0).divisors = Finset.filter IsPrimePow (a.divisors ∪ divisors 0)

Proof state:
case inr.inr.h
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)

Tactic:
apply hab.isPrimePow_dvd_mul

Result:
no goals

Proof state:
case inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
⊢ Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Result:
case inr.inl
a : ℕ
ha : a ≠ 0
hab : a.Coprime 0
⊢ Finset.filter IsPrimePow (a * 0).divisors = Finset.filter IsPrimePow (a.divisors ∪ divisors 0)

case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
⊢ Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)

Proof state:
case inl
b : ℕ
hab : b = 1
⊢ Finset.filter IsPrimePow (0 * b).divisors = Finset.filter IsPrimePow (divisors 0 ∪ b.divisors)

Tactic:
simp [hab, Finset.filter_singleton, not_isPrimePow_one]

Result:
no goals

Proof state:
a b : ℕ
hab : a.Coprime b
⊢ Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
b : ℕ
hab : Coprime 0 b
⊢ Finset.filter IsPrimePow (0 * b).divisors = Finset.filter IsPrimePow (divisors 0 ∪ b.divisors)

case inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
⊢ Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)

Proof state:
case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
⊢ Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)

Tactic:
ext n

Result:
case inr.inr.h
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (a * b).divisors ↔ n ∈ Finset.filter IsPrimePow (a.divisors ∪ b.divisors)

Proof state:
case inl
b : ℕ
hab : Coprime 0 b
⊢ Finset.filter IsPrimePow (0 * b).divisors = Finset.filter IsPrimePow (divisors 0 ∪ b.divisors)

Tactic:
simp only [Nat.coprime_zero_left] at hab

Result:
case inl
b : ℕ
hab : b = 1
⊢ Finset.filter IsPrimePow (0 * b).divisors = Finset.filter IsPrimePow (divisors 0 ∪ b.divisors)