R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
⊢ Squarefree x ↔ Multiset.Nodup (normalizedFactors x)
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
⊢ Squarefree x ↔ Multiset.Nodup (normalizedFactors x)
have drel : DecidableRel (Dvd.dvd : R → R → Prop) := by classical infer_instance
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
⊢ (∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
⊢ Squarefree x ↔ Multiset.Nodup (normalizedFactors x)
rw [multiplicity.squarefree_iff_multiplicity_le_one, Multiset.nodup_iff_count_le_one]
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
⊢ (∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
⊢ (∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
haveI := nontrivial_of_ne x 0 x0
case mp
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
⊢ Multiset.count a (normalizedFactors x) ≤ 1

case mpr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ multiplicity a x ≤ 1 ∨ IsUnit a
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
⊢ (∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
constructor <;> intro h a
no goals
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
⊢ DecidableRel Dvd.dvd
classical infer_instance
no goals
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
⊢ DecidableRel Dvd.dvd
infer_instance
case pos
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
⊢ Multiset.count a (normalizedFactors x) ≤ 1

case neg
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : ¬a ∈ normalizedFactors x
⊢ Multiset.count a (normalizedFactors x) ≤ 1
case mp
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
⊢ Multiset.count a (normalizedFactors x) ≤ 1
by_cases hmem : a ∈ normalizedFactors x
case pos
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
⊢ Multiset.count a (normalizedFactors x) ≤ 1
case pos
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
⊢ Multiset.count a (normalizedFactors x) ≤ 1
have ha := irreducible_of_normalized_factor _ hmem
case pos.inl
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : multiplicity a x ≤ 1
⊢ Multiset.count a (normalizedFactors x) ≤ 1

case pos.inr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : IsUnit a
⊢ Multiset.count a (normalizedFactors x) ≤ 1
case pos
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
⊢ Multiset.count a (normalizedFactors x) ≤ 1
rcases h a with (h | h)
case pos.inl
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : multiplicity a x ≤ 1
⊢ Multiset.count (↑normalize a) (normalizedFactors x) ≤ 1
case pos.inl
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : multiplicity a x ≤ 1
⊢ Multiset.count a (normalizedFactors x) ≤ 1
rw [← normalize_normalized_factor _ hmem]
case pos.inl
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : ↑(Multiset.count (↑normalize a) (normalizedFactors x)) ≤ 1
⊢ Multiset.count (↑normalize a) (normalizedFactors x) ≤ 1
case pos.inl
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : multiplicity a x ≤ 1
⊢ Multiset.count (↑normalize a) (normalizedFactors x) ≤ 1
rw [multiplicity_eq_count_normalizedFactors ha x0] at h
no goals
case pos.inl
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : ↑(Multiset.count (↑normalize a) (normalizedFactors x)) ≤ 1
⊢ Multiset.count (↑normalize a) (normalizedFactors x) ≤ 1
assumption_mod_cast
case pos.inr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this✝ : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : IsUnit a
this : ¬IsUnit a
⊢ Multiset.count a (normalizedFactors x) ≤ 1
case pos.inr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : IsUnit a
⊢ Multiset.count a (normalizedFactors x) ≤ 1
have := ha.1
no goals
case pos.inr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this✝ : Nontrivial R
h✝ : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : IsUnit a
this : ¬IsUnit a
⊢ Multiset.count a (normalizedFactors x) ≤ 1
contradiction
no goals
case neg
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : ¬a ∈ normalizedFactors x
⊢ Multiset.count a (normalizedFactors x) ≤ 1
simp [Multiset.count_eq_zero_of_not_mem hmem]
case mpr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ ¬IsUnit a → multiplicity a x ≤ 1
case mpr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ multiplicity a x ≤ 1 ∨ IsUnit a
rw [or_iff_not_imp_right]
case mpr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
⊢ multiplicity a x ≤ 1
case mpr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ ¬IsUnit a → multiplicity a x ≤ 1
intro hu
case pos
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a = 0
⊢ multiplicity a x ≤ 1

case neg
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
⊢ multiplicity a x ≤ 1
case mpr
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
⊢ multiplicity a x ≤ 1
by_cases h0 : a = 0
case neg.intro.intro
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ multiplicity a x ≤ 1
case neg
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
⊢ multiplicity a x ≤ 1
rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
case neg.intro.intro
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ multiplicity b x ≤ 1
case neg.intro.intro
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ multiplicity a x ≤ 1
apply le_trans (multiplicity.multiplicity_le_multiplicity_of_dvd_left hdvd)
case neg.intro.intro
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ ↑(Multiset.count (↑normalize b) (normalizedFactors x)) ≤ 1
case neg.intro.intro
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ multiplicity b x ≤ 1
rw [multiplicity_eq_count_normalizedFactors hib x0]
case neg.intro.intro
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
b : R
hib : Irreducible b
hdvd : b ∣ a
h : Multiset.count (↑normalize b) (normalizedFactors x) ≤ 1
⊢ ↑(Multiset.count (↑normalize b) (normalizedFactors x)) ≤ 1
case neg.intro.intro
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ ↑(Multiset.count (↑normalize b) (normalizedFactors x)) ≤ 1
specialize h (normalize b)
no goals
case neg.intro.intro
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
a : R
hu : ¬IsUnit a
h0 : ¬a = 0
b : R
hib : Irreducible b
hdvd : b ∣ a
h : Multiset.count (↑normalize b) (normalizedFactors x) ≤ 1
⊢ ↑(Multiset.count (↑normalize b) (normalizedFactors x)) ≤ 1
assumption_mod_cast
no goals
case pos
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
drel : DecidableRel Dvd.dvd
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a = 0
⊢ multiplicity a x ≤ 1
simp [h0, x0]