case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ IsUnit z
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x : R
h0 : x ≠ 0
h : IsRadical x
⊢ Squarefree x
rintro z ⟨w, rfl⟩
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
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ IsUnit z
specialize h 2 (z * w) ⟨w, by simp_rw [pow_two, mul_left_comm, ← mul_assoc]⟩
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
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
rwa [← one_mul (z * w), mul_assoc, mul_dvd_mul_iff_right, ← isUnit_iff_dvd_one] at h
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
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
rw [mul_assoc, mul_ne_zero_iff] at h0
no goals
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
exact h0.2
no goals
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
simp_rw [pow_two, mul_left_comm, ← mul_assoc]