-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem count_ne_zero_iff_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
    (Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a

Proof state:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ Associates.mk p ≤ Associates.mk a

Tactic:
refine
  ⟨fun h =>
    Associates.le_of_count_ne_zero (Associates.mk_ne_zero.mpr ha0)
      (Associates.irreducible_mk.mpr hp) h,
    fun h => ?_⟩

Result:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
h : Associates.mk p ≤ Associates.mk a
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0

Proof state:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
h : Associates.mk p ≤ Associates.mk a
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0

Tactic:
rw [← pow_one (Associates.mk p),
  Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero.mpr ha0)
    (Associates.irreducible_mk.mpr hp)] at h

Result:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
h : 1 ≤ (Associates.mk p).count (Associates.mk a).factors
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0

Proof state:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a

Tactic:
rw [← Associates.mk_le_mk_iff_dvd]

Result:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ Associates.mk p ≤ Associates.mk a

Proof state:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
h : 1 ≤ (Associates.mk p).count (Associates.mk a).factors
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0

Tactic:
exact (zero_lt_one.trans_le h).ne'

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a

Tactic:
nontriviality α

Result:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
inst✝ : Nontrivial α
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a