case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : factors a ≤ factors b
ha : a = 0
⊢ count p (factors a) ≤ count p (factors b)

case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : factors a ≤ factors b
ha : ¬a = 0
⊢ count p (factors a) ≤ count p (factors b)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : factors a ≤ factors b
⊢ count p (factors a) ≤ count p (factors b)
by_cases ha : a = 0
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
⊢ count p (factors a) ≤ count p (factors b)
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : factors a ≤ factors b
ha : ¬a = 0
⊢ count p (factors a) ≤ count p (factors b)
obtain ⟨sa, h_sa⟩ := factors_eq_some_iff_ne_zero.mpr ha
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h_sb : factors b = some sb
⊢ count p (factors a) ≤ count p (factors b)
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
⊢ count p (factors a) ≤ count p (factors b)
obtain ⟨sb, h_sb⟩ := factors_eq_some_iff_ne_zero.mpr hb
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h✝ : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : some sa ≤ some sb
h_sb : factors b = some sb
⊢ count p (some sa) ≤ count p (some sb)
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h_sb : factors b = some sb
⊢ count p (factors a) ≤ count p (factors b)
rw [h_sa, h_sb] at h⊢
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h✝ : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : some sa ≤ some sb
h_sb : factors b = some sb
⊢ Multiset.count { val := p, property := hp } sa ≤ Multiset.count { val := p, property := hp } sb
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h✝ : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : some sa ≤ some sb
h_sb : factors b = some sb
⊢ count p (some sa) ≤ count p (some sb)
rw [count_some hp, count_some hp]
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h✝ : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : sa ≤ sb
h_sb : factors b = some sb
⊢ Multiset.count { val := p, property := hp } sa ≤ Multiset.count { val := p, property := hp } sb
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h✝ : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : some sa ≤ some sb
h_sb : factors b = some sb
⊢ Multiset.count { val := p, property := hp } sa ≤ Multiset.count { val := p, property := hp } sb
rw [WithTop.some_le_some] at h
no goals
case neg.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h✝ : factors a ≤ factors b
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : sa ≤ sb
h_sb : factors b = some sb
⊢ Multiset.count { val := p, property := hp } sa ≤ Multiset.count { val := p, property := hp } sb
exact Multiset.count_le_of_le _ h
no goals
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : factors a ≤ factors b
ha : a = 0
⊢ count p (factors a) ≤ count p (factors b)
simp_all