case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ p ^ k ≤ Associates.mk a ↔ k ≤ count p (factors (Associates.mk a))
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
⊢ p ^ k ≤ m ↔ k ≤ count p (factors m)
obtain ⟨a, nz, rfl⟩ := Associates.exists_non_zero_rep h₁
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ some (replicate k { val := p, property := h₂ }) ≤ ↑(factors' a) ↔
    replicate k { val := p, property := ?intro.intro.hp } ≤ factors' a

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ p ^ k ≤ Associates.mk a ↔ k ≤ count p (factors (Associates.mk a))
rw [factors_mk _ nz, ← WithTop.some_eq_coe, count_some, Multiset.le_count_iff_replicate_le, ←
  factors_le, factors_prime_pow h₂, factors_mk _ nz]
no goals
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ some (replicate k { val := p, property := h₂ }) ≤ ↑(factors' a) ↔
    replicate k { val := p, property := ?intro.intro.hp } ≤ factors' a

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p

case intro.intro.hp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
p : Associates α
h₂ : Irreducible p
k : ℕ
a : α
nz : a ≠ 0
h₁ : Associates.mk a ≠ 0
⊢ Irreducible p
exact WithTop.coe_le_coe