-- Mathlib/Algebra/Squarefree/Basic.lean
theorem squarefree_iff_nodup_normalizedFactors [NormalizationMonoid R] {x : R}
    (x0 : x ≠ 0) : Squarefree x ↔ Multiset.Nodup (normalizedFactors x)

Proof state:
case pos.inl
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
⊢ Multiset.count (normalize a) (normalizedFactors x) ≤ 1

Tactic:
rw [emultiplicity_eq_count_normalizedFactors ha x0] at h

Result:
case pos.inl
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity 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

Proof state:
case mpr.inr.intro.intro
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
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
⊢ emultiplicity b x ≤ 1

Tactic:
rw [emultiplicity_eq_count_normalizedFactors hib x0]

Result:
case mpr.inr.intro.intro
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
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

Proof state:
case mpr
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ ¬IsUnit a → emultiplicity a x ≤ 1

Tactic:
intro hu

Result:
case mpr
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
⊢ emultiplicity a x ≤ 1

Proof state:
case pos.inr
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this✝ : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity 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

Tactic:
contradiction

Result:
no goals

Proof state:
case mpr.inl
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
hu : ¬IsUnit 0
⊢ emultiplicity 0 x ≤ 1

Tactic:
simp [x0]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∉ normalizedFactors x
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
simp [Multiset.count_eq_zero_of_not_mem hmem]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
⊢ (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
haveI := nontrivial_of_ne x 0 x0

Result:
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
⊢ (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1

Proof state:
case mpr.inr
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
⊢ emultiplicity a x ≤ 1

Tactic:
rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩

Result:
case mpr.inr.intro.intro
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
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
⊢ emultiplicity a x ≤ 1

Proof state:
case pos.inl
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity 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

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ emultiplicity a x ≤ 1 ∨ IsUnit a

Tactic:
rw [or_iff_not_imp_right]

Result:
case mpr
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ ¬IsUnit a → emultiplicity a x ≤ 1

Proof state:
case mpr.inr.intro.intro
R : Type u_1
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
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

Tactic:
exact_mod_cast h (normalize b)

Result:
no goals