case inl
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
x : R
n : ℕ
hnorm : ↑normalize 0 = 0
hle : 0 ^ n ∣ x
hlt : ¬0 ^ (n + 1) ∣ x
⊢ count 0 (normalizedFactors x) = n

case inr
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
p x : R
hnorm : ↑normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hp : Irreducible p
⊢ count p (normalizedFactors x) = n
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
p x : R
hp : p = 0 ∨ Irreducible p
hnorm : ↑normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
⊢ count p (normalizedFactors x) = n
rcases hp with (rfl | hp)
case inl.zero
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
x : R
hnorm : ↑normalize 0 = 0
hle : 0 ^ Nat.zero ∣ x
hlt : ¬0 ^ (Nat.zero + 1) ∣ x
⊢ count 0 (normalizedFactors x) = Nat.zero

case inl.succ
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
x : R
hnorm : ↑normalize 0 = 0
n✝ : ℕ
hle : 0 ^ Nat.succ n✝ ∣ x
hlt : ¬0 ^ (Nat.succ n✝ + 1) ∣ x
⊢ count 0 (normalizedFactors x) = Nat.succ n✝
case inl
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
x : R
n : ℕ
hnorm : ↑normalize 0 = 0
hle : 0 ^ n ∣ x
hlt : ¬0 ^ (n + 1) ∣ x
⊢ count 0 (normalizedFactors x) = n
cases n
no goals
case inl.zero
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
x : R
hnorm : ↑normalize 0 = 0
hle : 0 ^ Nat.zero ∣ x
hlt : ¬0 ^ (Nat.zero + 1) ∣ x
⊢ count 0 (normalizedFactors x) = Nat.zero
exact count_eq_zero.2 (zero_not_mem_normalizedFactors _)
case inl.succ
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
x : R
hnorm : ↑normalize 0 = 0
n✝ : ℕ
hle : 0 ∣ x
hlt : ¬0 ∣ x
⊢ count 0 (normalizedFactors x) = Nat.succ n✝
case inl.succ
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
x : R
hnorm : ↑normalize 0 = 0
n✝ : ℕ
hle : 0 ^ Nat.succ n✝ ∣ x
hlt : ¬0 ^ (Nat.succ n✝ + 1) ∣ x
⊢ count 0 (normalizedFactors x) = Nat.succ n✝
rw [zero_pow (Nat.succ_pos _)] at hle hlt
no goals
case inl.succ
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
x : R
hnorm : ↑normalize 0 = 0
n✝ : ℕ
hle : 0 ∣ x
hlt : ¬0 ∣ x
⊢ count 0 (normalizedFactors x) = Nat.succ n✝
exact absurd hle hlt
no goals
case inr
α : Type ?u.1182347
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
p x : R
hnorm : ↑normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hp : Irreducible p
⊢ count p (normalizedFactors x) = n
exact count_normalizedFactors_eq hp hnorm hle hlt