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

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
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
by_cases gcd x y = 0
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
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
replace hy := ((dvd_gcd_iff x x _).2 ⟨dvd_rfl, hy⟩).trans gcd_pow_right_dvd_pow_gcd
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
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
obtain ⟨z, hz⟩ := gcd_dvd_left x y
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
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
nth_rw 1 [hz] at hy⊢
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
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
rw [pow_two, mul_dvd_mul_iff_left h] at hy
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
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
obtain ⟨w, hw⟩ := hy
no goals
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
exact (hx z ⟨w, by rwa [mul_right_comm, ← hw]⟩).mul_right_dvd.2 dvd_rfl
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
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
rw [h]
no goals
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
apply dvd_zero
no goals
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
rwa [mul_right_comm, ← hw]