case pos
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : gcd x y = 0
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')

case neg
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
by_cases h : gcd x y = 0
case neg.intro
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
x' : α
ex : x = gcd x y * x'
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
case neg
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
obtain ⟨x', ex⟩ := gcd_dvd_left x y
case neg.intro.intro
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
x' : α
ex : x = gcd x y * x'
y' : α
ey : y = gcd x y * y'
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
case neg.intro
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
x' : α
ex : x = gcd x y * x'
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
obtain ⟨y', ey⟩ := gcd_dvd_right x y
no goals
case neg.intro.intro
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
x' : α
ex : x = gcd x y * x'
y' : α
ey : y = gcd x y * y'
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
exact ⟨x', y', ex, ey, isUnit_gcd_of_eq_mul_gcd ex ey h⟩
case pos.intro
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ ∃ x' y', 0 = gcd 0 0 * x' ∧ 0 = gcd 0 0 * y' ∧ IsUnit (gcd x' y')
case pos
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : gcd x y = 0
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
obtain ⟨rfl, rfl⟩ := (gcd_eq_zero_iff x y).1 h
case pos.intro
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ ∃ x' y', 0 = gcd 0 0 * x' ∧ 0 = gcd 0 0 * y' ∧ Associated (gcd x' y') 1
case pos.intro
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ ∃ x' y', 0 = gcd 0 0 * x' ∧ 0 = gcd 0 0 * y' ∧ IsUnit (gcd x' y')
simp_rw [← associated_one_iff_isUnit]
no goals
case pos.intro
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ ∃ x' y', 0 = gcd 0 0 * x' ∧ 0 = gcd 0 0 * y' ∧ Associated (gcd x' y') 1
exact ⟨1, 1, by rw [h, zero_mul], by rw [h, zero_mul], gcd_one_left' 1⟩
no goals
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ 0 = gcd 0 0 * 1
rw [h, zero_mul]
no goals
α✝ : Type ?u.200688
inst✝² : CancelCommMonoidWithZero α✝
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ 0 = gcd 0 0 * 1
rw [h, zero_mul]