[GOAL]
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬Squarefree 0
[PROOFSTEP]
erw [not_forall]
[GOAL]
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ∃ x, ¬(x * x ∣ 0 → IsUnit x)
[PROOFSTEP]
exact ⟨0, by simp⟩
[GOAL]
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬(0 * 0 ∣ 0 → IsUnit 0)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
m : R
hm : Squarefree m
⊢ m ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hm : Squarefree 0
⊢ False
[PROOFSTEP]
exact not_squarefree_zero hm
[GOAL]
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
⊢ Squarefree x
[PROOFSTEP]
rintro y ⟨z, hz⟩
[GOAL]
case intro
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * y * z
⊢ IsUnit y
[PROOFSTEP]
rw [mul_assoc] at hz 
[GOAL]
case intro
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
⊢ IsUnit y
[PROOFSTEP]
rcases h.isUnit_or_isUnit hz with (hu | hu)
[GOAL]
case intro.inl
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit y
⊢ IsUnit y
[PROOFSTEP]
exact hu
[GOAL]
case intro.inr
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit (y * z)
⊢ IsUnit y
[PROOFSTEP]
apply isUnit_of_mul_isUnit_left hu
[GOAL]
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r : R
⊢ Squarefree r ↔ ∀ (x : R), multiplicity x r ≤ 1 ∨ IsUnit x
[PROOFSTEP]
refine' forall_congr' fun a => _
[GOAL]
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r a : R
⊢ a * a ∣ r → IsUnit a ↔ multiplicity a r ≤ 1 ∨ IsUnit a
[PROOFSTEP]
rw [← sq, pow_dvd_iff_le_multiplicity, or_iff_not_imp_left, not_le, imp_congr _ Iff.rfl]
[GOAL]
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r a : R
⊢ ↑2 ≤ multiplicity a r ↔ 1 < multiplicity a r
[PROOFSTEP]
rw [← one_add_one_eq_two]
[GOAL]
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r a : R
⊢ ↑(1 + 1) ≤ multiplicity a r ↔ 1 < multiplicity a r
[PROOFSTEP]
simpa using PartENat.add_one_le_iff_lt (PartENat.natCast_ne_top 1)
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
hb : b ≠ 0
⊢ Finite a b
[PROOFSTEP]
classical
revert hb
refine' WfDvdMonoid.induction_on_irreducible b (fun c => c.irrefl.elim) (fun u hu _ => _) fun b p hb hp ih _ => _
· rw [multiplicity.finite_iff_dom, multiplicity.isUnit_right ha.not_unit hu]
  exact PartENat.dom_natCast 0
· refine'
    multiplicity.finite_mul ha
      (multiplicity.finite_iff_dom.mpr (PartENat.dom_of_le_natCast (show multiplicity a p ≤ ↑1 from _))) (ih hb)
  norm_cast
  exact ((multiplicity.squarefree_iff_multiplicity_le_one p).mp hp.squarefree a).resolve_right ha.not_unit
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
hb : b ≠ 0
⊢ Finite a b
[PROOFSTEP]
revert hb
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
⊢ b ≠ 0 → Finite a b
[PROOFSTEP]
refine' WfDvdMonoid.induction_on_irreducible b (fun c => c.irrefl.elim) (fun u hu _ => _) fun b p hb hp ih _ => _
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
u : R
hu : IsUnit u
x✝ : u ≠ 0
⊢ Finite a u
[PROOFSTEP]
rw [multiplicity.finite_iff_dom, multiplicity.isUnit_right ha.not_unit hu]
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
u : R
hu : IsUnit u
x✝ : u ≠ 0
⊢ 0.Dom
[PROOFSTEP]
exact PartENat.dom_natCast 0
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b✝ : R
ha : Prime a
b p : R
hb : b ≠ 0
hp : Irreducible p
ih : b ≠ 0 → Finite a b
x✝ : p * b ≠ 0
⊢ Finite a (p * b)
[PROOFSTEP]
refine'
  multiplicity.finite_mul ha
    (multiplicity.finite_iff_dom.mpr (PartENat.dom_of_le_natCast (show multiplicity a p ≤ ↑1 from _))) (ih hb)
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b✝ : R
ha : Prime a
b p : R
hb : b ≠ 0
hp : Irreducible p
ih : b ≠ 0 → Finite a b
x✝ : p * b ≠ 0
⊢ multiplicity a p ≤ 1
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b✝ : R
ha : Prime a
b p : R
hb : b ≠ 0
hp : Irreducible p
ih : b ≠ 0 → Finite a b
x✝ : p * b ≠ 0
⊢ multiplicity a p ≤ 1
[PROOFSTEP]
exact ((multiplicity.squarefree_iff_multiplicity_le_one p).mp hp.squarefree a).resolve_right ha.not_unit
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
[PROOFSTEP]
symm
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r → ∀ (x : R), Irreducible x → ¬x * x ∣ r
[PROOFSTEP]
rintro (⟨rfl, h⟩ | h)
[GOAL]
case mp.inl.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), ¬Irreducible x
⊢ ∀ (x : R), Irreducible x → ¬x * x ∣ 0
[PROOFSTEP]
simpa using h
[GOAL]
case mp.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : Squarefree r
⊢ ∀ (x : R), Irreducible x → ¬x * x ∣ r
[PROOFSTEP]
intro x hx t
[GOAL]
case mp.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : Squarefree r
x : R
hx : Irreducible x
t : x * x ∣ r
⊢ False
[PROOFSTEP]
exact hx.not_unit (h x t)
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) → (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
[PROOFSTEP]
rcases eq_or_ne r 0 with (rfl | hr)
[GOAL]
case mpr.inl
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ (0 = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree 0
[PROOFSTEP]
exact Or.inl (by simpa using h)
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ 0 = 0 ∧ ∀ (x : R), ¬Irreducible x
[PROOFSTEP]
simpa using h
[GOAL]
case mpr.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
[PROOFSTEP]
right
[GOAL]
case mpr.inr.h
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
⊢ Squarefree r
[PROOFSTEP]
intro x hx
[GOAL]
case mpr.inr.h
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
x : R
hx : x * x ∣ r
⊢ IsUnit x
[PROOFSTEP]
by_contra i
[GOAL]
case mpr.inr.h
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
x : R
hx : x * x ∣ r
i : ¬IsUnit x
⊢ False
[PROOFSTEP]
have : x ≠ 0 := by
  rintro rfl
  apply hr
  simpa only [zero_dvd_iff, mul_zero] using hx
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
x : R
hx : x * x ∣ r
i : ¬IsUnit x
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
hx : 0 * 0 ∣ r
i : ¬IsUnit 0
⊢ False
[PROOFSTEP]
apply hr
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
hx : 0 * 0 ∣ r
i : ¬IsUnit 0
⊢ r = 0
[PROOFSTEP]
simpa only [zero_dvd_iff, mul_zero] using hx
[GOAL]
case mpr.inr.h
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
x : R
hx : x * x ∣ r
i : ¬IsUnit x
this : x ≠ 0
⊢ False
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := WfDvdMonoid.exists_irreducible_factor i this
[GOAL]
case mpr.inr.h.intro.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
x : R
hx : x * x ∣ r
i : ¬IsUnit x
this : x ≠ 0
j : R
hj₁ : Irreducible j
hj₂ : j ∣ x
⊢ False
[PROOFSTEP]
exact h _ hj₁ ((mul_dvd_mul hj₂ hj₂).trans hx)
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : r ≠ 0
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
[PROOFSTEP]
simpa [hr] using (irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree r).symm
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
[PROOFSTEP]
rw [irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree, ← not_exists]
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ¬∃ x, Irreducible x) ∨ Squarefree r
[PROOFSTEP]
simp only [hr, not_true, false_or_iff, and_false_iff]
[GOAL]
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x : R
h0 : x ≠ 0
h : IsRadical x
⊢ Squarefree x
[PROOFSTEP]
rintro z ⟨w, rfl⟩
[GOAL]
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ IsUnit z
[PROOFSTEP]
specialize h 2 (z * w) ⟨w, by simp_rw [pow_two, mul_left_comm, ← mul_assoc]⟩
[GOAL]
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ (z * w) ^ 2 = z * z * w * w
[PROOFSTEP]
simp_rw [pow_two, mul_left_comm, ← mul_assoc]
[GOAL]
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : z * z * w ∣ z * w
⊢ IsUnit z
[PROOFSTEP]
rwa [← one_mul (z * w), mul_assoc, mul_dvd_mul_iff_right, ← isUnit_iff_dvd_one] at h 
[GOAL]
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0
[PROOFSTEP]
rw [mul_assoc, mul_ne_zero_iff] at h0 
[GOAL]
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z ≠ 0 ∧ z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0
[PROOFSTEP]
exact h0.2
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ y ^ 2
⊢ x ∣ gcd x y
[PROOFSTEP]
by_cases gcd x y = 0
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ y ^ 2
⊢ x ∣ gcd x y
[PROOFSTEP]
by_cases gcd x y = 0
[GOAL]
case pos
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ y ^ 2
h : gcd x y = 0
⊢ x ∣ gcd x y
[PROOFSTEP]
rw [h]
[GOAL]
case pos
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ y ^ 2
h : gcd x y = 0
⊢ x ∣ 0
[PROOFSTEP]
apply dvd_zero
[GOAL]
case neg
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ y ^ 2
h : ¬gcd x y = 0
⊢ x ∣ gcd x y
[PROOFSTEP]
replace hy := ((dvd_gcd_iff x x _).2 ⟨dvd_rfl, hy⟩).trans gcd_pow_right_dvd_pow_gcd
[GOAL]
case neg
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
h : ¬gcd x y = 0
hy : x ∣ gcd x y ^ 2
⊢ x ∣ gcd x y
[PROOFSTEP]
obtain ⟨z, hz⟩ := gcd_dvd_left x y
[GOAL]
case neg.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
h : ¬gcd x y = 0
hy : x ∣ gcd x y ^ 2
z : R
hz : x = gcd x y * z
⊢ x ∣ gcd x y
[PROOFSTEP]
nth_rw 1 [hz] at hy ⊢
[GOAL]
case neg.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
h : ¬gcd x y = 0
z : R
hy : gcd x y * z ∣ gcd x y ^ 2
hz : x = gcd x y * z
⊢ gcd x y * z ∣ gcd x y
[PROOFSTEP]
rw [pow_two, mul_dvd_mul_iff_left h] at hy 
[GOAL]
case neg.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
h : ¬gcd x y = 0
z : R
hy : z ∣ gcd x y
hz : x = gcd x y * z
⊢ gcd x y * z ∣ gcd x y
[PROOFSTEP]
obtain ⟨w, hw⟩ := hy
[GOAL]
case neg.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
h : ¬gcd x y = 0
z : R
hz : x = gcd x y * z
w : R
hw : gcd x y = z * w
⊢ gcd x y * z ∣ gcd x y
[PROOFSTEP]
exact (hx z ⟨w, by rwa [mul_right_comm, ← hw]⟩).mul_right_dvd.2 dvd_rfl
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
hx : Squarefree x
y : R
h : ¬gcd x y = 0
z : R
hz : x = gcd x y * z
w : R
hw : gcd x y = z * w
⊢ x = z * z * w
[PROOFSTEP]
rwa [mul_right_comm, ← hw]
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
⊢ x = 0 → IsRadical x
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
⊢ IsRadical 0
[PROOFSTEP]
rw [zero_isRadical_iff]
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
⊢ IsReduced R
[PROOFSTEP]
infer_instance
[GOAL]
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)
[PROOFSTEP]
have drel : DecidableRel (Dvd.dvd : R → R → Prop) := by classical infer_instance
[GOAL]
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
⊢ DecidableRel Dvd.dvd
[PROOFSTEP]
classical infer_instance
[GOAL]
R : Type u_1
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
x0 : x ≠ 0
⊢ DecidableRel Dvd.dvd
[PROOFSTEP]
infer_instance
[GOAL]
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)
[PROOFSTEP]
rw [multiplicity.squarefree_iff_multiplicity_le_one, Multiset.nodup_iff_count_le_one]
[GOAL]
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
[PROOFSTEP]
haveI := nontrivial_of_ne x 0 x0
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
⊢ (∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1) → ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
[PROOFSTEP]
intro h a
[GOAL]
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
⊢ (∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1) → ∀ (x_1 : R), multiplicity x_1 x ≤ 1 ∨ IsUnit x_1
[PROOFSTEP]
intro h a
[GOAL]
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
[PROOFSTEP]
by_cases hmem : a ∈ normalizedFactors x
[GOAL]
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
[PROOFSTEP]
have ha := irreducible_of_normalized_factor _ hmem
[GOAL]
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
[PROOFSTEP]
rcases h a with (h | h)
[GOAL]
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
[PROOFSTEP]
rw [← normalize_normalized_factor _ hmem]
[GOAL]
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
[PROOFSTEP]
rw [multiplicity_eq_count_normalizedFactors ha x0] at h 
[GOAL]
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
[PROOFSTEP]
assumption_mod_cast
[GOAL]
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
[PROOFSTEP]
have := ha.1
[GOAL]
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
[PROOFSTEP]
contradiction
[GOAL]
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
[PROOFSTEP]
simp [Multiset.count_eq_zero_of_not_mem hmem]
[GOAL]
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
[PROOFSTEP]
rw [or_iff_not_imp_right]
[GOAL]
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
[PROOFSTEP]
intro hu
[GOAL]
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
[PROOFSTEP]
by_cases h0 : a = 0
[GOAL]
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
[PROOFSTEP]
simp [h0, x0]
[GOAL]
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
[PROOFSTEP]
rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
[GOAL]
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
[PROOFSTEP]
apply le_trans (multiplicity.multiplicity_le_multiplicity_of_dvd_left hdvd)
[GOAL]
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
[PROOFSTEP]
rw [multiplicity_eq_count_normalizedFactors hib x0]
[GOAL]
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
[PROOFSTEP]
specialize h (normalize b)
[GOAL]
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
[PROOFSTEP]
assumption_mod_cast
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
x y : R
n : ℕ
hsq : Squarefree x
h0 : n ≠ 0
⊢ x ∣ y ^ n ↔ x ∣ y
[PROOFSTEP]
classical
haveI := UniqueFactorizationMonoid.toGCDMonoid R
exact ⟨hsq.isRadical n y, fun h => h.pow h0⟩
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
x y : R
n : ℕ
hsq : Squarefree x
h0 : n ≠ 0
⊢ x ∣ y ^ n ↔ x ∣ y
[PROOFSTEP]
haveI := UniqueFactorizationMonoid.toGCDMonoid R
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
x y : R
n : ℕ
hsq : Squarefree x
h0 : n ≠ 0
this : GCDMonoid R
⊢ x ∣ y ^ n ↔ x ∣ y
[PROOFSTEP]
exact ⟨hsq.isRadical n y, fun h => h.pow h0⟩
[GOAL]
R : Type u_1
n : ℤ
⊢ Squarefree (natAbs n) ↔ Squarefree n
[PROOFSTEP]
simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs, isUnit_iff_natAbs_eq, Nat.isUnit_iff]
[GOAL]
R : Type u_1
n : ℕ
⊢ Squarefree ↑n ↔ Squarefree n
[PROOFSTEP]
rw [← squarefree_natAbs, natAbs_ofNat]
