α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0 ↔ p ∣ a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0 ↔ p ∣ a
nontriviality α
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0 ↔ Associates.mk p ≤ Associates.mk a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0 ↔ p ∣ a
rw [← Associates.mk_le_mk_iff_dvd_iff]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
h : Associates.mk p ≤ Associates.mk a
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0 ↔ Associates.mk p ≤ Associates.mk a
refine'
  ⟨fun h =>
    Associates.le_of_count_ne_zero (Associates.mk_ne_zero.mpr ha0)
      ((Associates.irreducible_mk p).mpr hp) h,
    fun h => _⟩
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
h : 1 ≤ count (Associates.mk p) (factors (Associates.mk a))
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
h : Associates.mk p ≤ Associates.mk a
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0
rw [← pow_one (Associates.mk p),
  Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero.mpr ha0)
    ((Associates.irreducible_mk p).mpr hp)] at h
no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
h : 1 ≤ count (Associates.mk p) (factors (Associates.mk a))
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0
exact (zero_lt_one.trans_le h).ne'