case inl
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k b : ℕ
hab : coprime 0 b
⊢ Finset.filter IsPrimePow (divisors (0 * b)) = Finset.filter IsPrimePow (divisors 0 ∪ divisors b)

case inr
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
rcases eq_or_ne a 0 with (rfl | ha)
case inr.inl
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k a : ℕ
ha : a ≠ 0
hab : coprime a 0
⊢ Finset.filter IsPrimePow (divisors (a * 0)) = Finset.filter IsPrimePow (divisors a ∪ divisors 0)

case inr.inr
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
case inr
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
rcases eq_or_ne b 0 with (rfl | hb)
case inr.inr.a
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (divisors (a * b)) ↔ n ∈ Finset.filter IsPrimePow (divisors a ∪ divisors b)
case inr.inr
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
ext n
case inr.inr.a
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)
case inr.inr.a
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (divisors (a * b)) ↔ n ∈ Finset.filter IsPrimePow (divisors a ∪ divisors b)
simp only [ha, hb, Finset.mem_union, Finset.mem_filter, Nat.mul_eq_zero, and_true_iff, Ne.def,
  and_congr_left_iff, not_false_iff, Nat.mem_divisors, or_self_iff]
no goals
case inr.inr.a
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)
apply hab.isPrimePow_dvd_mul
case inl
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k b : ℕ
hab : b = 1
⊢ Finset.filter IsPrimePow (divisors (0 * b)) = Finset.filter IsPrimePow (divisors 0 ∪ divisors b)
case inl
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k b : ℕ
hab : coprime 0 b
⊢ Finset.filter IsPrimePow (divisors (0 * b)) = Finset.filter IsPrimePow (divisors 0 ∪ divisors b)
simp only [Nat.coprime_zero_left] at hab
no goals
case inl
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k b : ℕ
hab : b = 1
⊢ Finset.filter IsPrimePow (divisors (0 * b)) = Finset.filter IsPrimePow (divisors 0 ∪ divisors b)
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
case inr.inl
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k a : ℕ
ha : a ≠ 0
hab : a = 1
⊢ Finset.filter IsPrimePow (divisors (a * 0)) = Finset.filter IsPrimePow (divisors a ∪ divisors 0)
case inr.inl
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k a : ℕ
ha : a ≠ 0
hab : coprime a 0
⊢ Finset.filter IsPrimePow (divisors (a * 0)) = Finset.filter IsPrimePow (divisors a ∪ divisors 0)
simp only [Nat.coprime_zero_right] at hab
no goals
case inr.inl
R : Type ?u.20477
inst✝ : CommMonoidWithZero R
n p : R
k a : ℕ
ha : a ≠ 0
hab : a = 1
⊢ Finset.filter IsPrimePow (divisors (a * 0)) = Finset.filter IsPrimePow (divisors a ∪ divisors 0)
simp [hab, Finset.filter_singleton, not_isPrimePow_one]