α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
⊢ a = p ^ count p (factors a)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
⊢ a = p ^ count p (factors a)
nontriviality α
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
⊢ a = p ^ count p (factors a)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
⊢ a = p ^ count p (factors a)
have hph := pow_ne_zero n hp.ne_zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
⊢ a = p ^ count p (factors a)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
⊢ a = p ^ count p (factors a)
have ha := ne_zero_of_dvd_ne_zero hph h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
⊢ ∀ (p_1 : Associates α), Irreducible p_1 → count p_1 (factors a) = count p_1 (factors (p ^ count p (factors a)))
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
⊢ a = p ^ count p (factors a)
apply eq_of_eq_counts ha (pow_ne_zero _ hp.ne_zero)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
⊢ ∀ (p_1 : Associates α), Irreducible p_1 → count p_1 (factors a) = count p_1 (factors (p ^ count p (factors a)))
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
⊢ ∀ (p_1 : Associates α), Irreducible p_1 → count p_1 (factors a) = count p_1 (factors (p ^ count p (factors a)))
have eq_zero_of_ne : ∀ q : Associates α, Irreducible q → q ≠ p → _ = 0 := fun q hq h' =>
  Nat.eq_zero_of_le_zero <| by
    convert count_le_count_of_le hph hq h
    symm
    rw [count_pow hp.ne_zero hq, count_eq_zero_of_ne hq hp h', MulZeroClass.mul_zero]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
q : Associates α
hq : Irreducible q
⊢ count q (factors a) = count q (factors (p ^ count p (factors a)))
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
⊢ ∀ (p_1 : Associates α), Irreducible p_1 → count p_1 (factors a) = count p_1 (factors (p ^ count p (factors a)))
intro q hq
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
q : Associates α
hq : Irreducible q
⊢ count q (factors a) = count p (factors a) * count q (factors p)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
q : Associates α
hq : Irreducible q
⊢ count q (factors a) = count q (factors (p ^ count p (factors a)))
rw [count_pow hp.ne_zero hq]
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
q : Associates α
hq : Irreducible q
h : q = p
⊢ count q (factors a) = count p (factors a) * count q (factors p)

case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
q : Associates α
hq : Irreducible q
h : ¬q = p
⊢ count q (factors a) = count p (factors a) * count q (factors p)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
q : Associates α
hq : Irreducible q
⊢ count q (factors a) = count p (factors a) * count q (factors p)
by_cases h : q = p
case h.e'_4
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ 0 = count q (factors (p ^ n))
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ ?m.2897509 q ≤ 0
convert count_le_count_of_le hph hq h
case h.e'_4
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ count q (factors (p ^ n)) = 0
case h.e'_4
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ 0 = count q (factors (p ^ n))
symm
no goals
case h.e'_4
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ count q (factors (p ^ n)) = 0
rw [count_pow hp.ne_zero hq, count_eq_zero_of_ne hq hp h', MulZeroClass.mul_zero]
no goals
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
q : Associates α
hq : Irreducible q
h : q = p
⊢ count q (factors a) = count p (factors a) * count q (factors p)
rw [h, count_self hp, mul_one]
no goals
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → count q (factors a) = 0
q : Associates α
hq : Irreducible q
h : ¬q = p
⊢ count q (factors a) = count p (factors a) * count q (factors p)
rw [count_eq_zero_of_ne hq hp h, MulZeroClass.mul_zero, eq_zero_of_ne q hq h]