α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ count p (factors a) ≠ 0 → count p (factors b) = 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ count p (factors a) = 0 ∨ count p (factors b) = 0
rw [or_iff_not_imp_left, ← Ne.def]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
hca : count p (factors a) ≠ 0
⊢ count p (factors b) = 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ count p (factors a) ≠ 0 → count p (factors b) = 0
intro hca
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hca : count p (factors a) ≠ 0
hcb : count p (factors b) ≠ 0
⊢ ∃ d, d ∣ a ∧ d ∣ b ∧ Prime d
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
hca : count p (factors a) ≠ 0
⊢ count p (factors b) = 0
contrapose! hab with hcb
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hca : count p (factors a) ≠ 0
hcb : count p (factors b) ≠ 0
⊢ ∃ d, d ∣ a ∧ d ∣ b ∧ Prime d
exact
  ⟨p, le_of_count_ne_zero ha hp hca, le_of_count_ne_zero hb hp hcb, irreducible_iff_prime.mp hp⟩