α✝ : Type ?u.198677
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ Associated (gcd x' y') 1
α✝ : Type ?u.198677
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ IsUnit (gcd x' y')
rw [← associated_one_iff_isUnit]
α✝ : Type ?u.198677
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ Associated (gcd x y * gcd x' y') (gcd x y * 1)
α✝ : Type ?u.198677
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ Associated (gcd x' y') 1
refine' Associated.of_mul_left _ (Associated.refl <| gcd x y) h
case h.e'_4
α✝ : Type ?u.198677
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ gcd x y * 1 = gcd (gcd x y * x') (gcd x y * y')
α✝ : Type ?u.198677
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ Associated (gcd x y * gcd x' y') (gcd x y * 1)
convert (gcd_mul_left' (gcd x y) x' y').symm using 1
no goals
case h.e'_4
α✝ : Type ?u.198677
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ gcd x y * 1 = gcd (gcd x y * x') (gcd x y * y')
rw [← ex, ← ey, mul_one]