case a
α : Type ?u.1033931
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ multiplicity a b ≤ ↑(count (↑normalize a) (normalizedFactors b))

case a
α : Type ?u.1033931
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ↑(count (↑normalize a) (normalizedFactors b)) ≤ multiplicity a b
α : Type ?u.1033931
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ multiplicity a b = ↑(count (↑normalize a) (normalizedFactors b))
apply le_antisymm
no goals
case a
α : Type ?u.1033931
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ↑(count (↑normalize a) (normalizedFactors b)) ≤ multiplicity a b
rw [le_multiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]
case a.h
α : Type ?u.1033931
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ multiplicity a b < ↑(count (↑normalize a) (normalizedFactors b)) + 1
case a
α : Type ?u.1033931
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ multiplicity a b ≤ ↑(count (↑normalize a) (normalizedFactors b))
apply PartENat.le_of_lt_add_one
case a.h
α : Type ?u.1033931
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ¬count (↑normalize a) (normalizedFactors b) + 1 ≤ count (↑normalize a) (normalizedFactors b)
case a.h
α : Type ?u.1033931
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ multiplicity a b < ↑(count (↑normalize a) (normalizedFactors b)) + 1
rw [← Nat.cast_one, ← Nat.cast_add, lt_iff_not_ge, ge_iff_le,
  le_multiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]
no goals
case a.h
α : Type ?u.1033931
R : Type u_1
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : Nontrivial R
inst✝¹ : NormalizationMonoid R
dec_dvd : DecidableRel Dvd.dvd
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ¬count (↑normalize a) (normalizedFactors b) + 1 ≤ count (↑normalize a) (normalizedFactors b)
simp