case inl
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n b : ℕ
hn : IsPrimePow n
hab : coprime 0 b
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b

case inr
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
rcases eq_or_ne a 0 with (rfl | ha)
case inr.inl
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : coprime a 0
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0

case inr.inr
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
case inr
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
rcases eq_or_ne b 0 with (rfl | hb)
case inr.inr
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b → n ∣ a ∨ n ∣ b
case inr.inr
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
refine'
  ⟨_, fun h =>
    Or.elim h (fun i => i.trans ((@dvd_mul_right a b a hab).mpr (dvd_refl a)))
        fun i => i.trans ((@dvd_mul_left a b b hab.symm).mpr (dvd_refl b))⟩
case inr.inr.intro.intro.intro.intro
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ p ^ k ∣ a * b → p ^ k ∣ a ∨ p ^ k ∣ b
case inr.inr
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b → n ∣ a ∨ n ∣ b
obtain ⟨p, k, hp, _, rfl⟩ := (isPrimePow_nat_iff _).1 hn
case inr.inr.intro.intro.intro.intro
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
case inr.inr.intro.intro.intro.intro
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ p ^ k ∣ a * b → p ^ k ∣ a ∨ p ^ k ∣ b
simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb), Nat.factorization_mul ha hb,
  hp.pow_dvd_iff_le_factorization ha, hp.pow_dvd_iff_le_factorization hb, Pi.add_apply,
  Finsupp.coe_add]
case inr.inr.intro.intro.intro.intro
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
this : ↑(factorization a) p = 0 ∨ ↑(factorization b) p = 0
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
case inr.inr.intro.intro.intro.intro
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
have : a.factorization p = 0 ∨ b.factorization p = 0 := by
  rw [← Finsupp.not_mem_support_iff, ← Finsupp.not_mem_support_iff, ← not_and_or, ←
    Finset.mem_inter]
  intro t simpa using (Nat.factorization_disjoint_of_coprime hab).le_bot t
no goals
case inr.inr.intro.intro.intro.intro
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
this : ↑(factorization a) p = 0 ∨ ↑(factorization b) p = 0
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
cases' this with h h <;> simp [h, imp_or]
case inl
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n b : ℕ
hn : IsPrimePow n
hab : b = 1
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
case inl
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n b : ℕ
hn : IsPrimePow n
hab : coprime 0 b
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
simp only [Nat.coprime_zero_left] at hab
no goals
case inl
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n b : ℕ
hn : IsPrimePow n
hab : b = 1
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
case inr.inl
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : a = 1
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
case inr.inl
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : coprime a 0
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
simp only [Nat.coprime_zero_right] at hab
no goals
case inr.inl
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : a = 1
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ ¬p ∈ (factorization a).support ∩ (factorization b).support
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ ↑(factorization a) p = 0 ∨ ↑(factorization b) p = 0
rw [← Finsupp.not_mem_support_iff, ← Finsupp.not_mem_support_iff, ← not_and_or, ←
  Finset.mem_inter]
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
t : p ∈ (factorization a).support ∩ (factorization b).support
⊢ False
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ ¬p ∈ (factorization a).support ∩ (factorization b).support
intro t
no goals
R : Type ?u.12477
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
t : p ∈ (factorization a).support ∩ (factorization b).support
⊢ False
simpa using (Nat.factorization_disjoint_of_coprime hab).le_bot t