-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem extract_gcd {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α] (x y : α) :
    ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')

Proof state:
case pos.intro
α : Type u_2
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

Tactic:
exact ⟨1, 1, by rw [h, zero_mul], by rw [h, zero_mul], gcd_one_left' 1⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')

Tactic:
by_cases h : gcd x y = 0

Result:
case pos
α : Type u_2
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_2
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')

Proof state:
case pos.intro
α : Type u_2
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')

Tactic:
simp_rw [← associated_one_iff_isUnit]

Result:
case pos.intro
α : Type u_2
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

Proof state:
case pos
α : Type u_2
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')

Tactic:
obtain ⟨rfl, rfl⟩ := (gcd_eq_zero_iff x y).1 h

Result:
case pos.intro
α : Type u_2
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')

Proof state:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ 0 = gcd 0 0 * 1

Tactic:
rw [h, zero_mul]

Result:
no goals

Proof state:
case neg
α : Type u_2
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')

Tactic:
obtain ⟨x', ex⟩ := gcd_dvd_left x y

Result:
case neg.intro
α : Type u_2
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')

Proof state:
case neg.intro
α : Type u_2
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')

Tactic:
obtain ⟨y', ey⟩ := gcd_dvd_right x y

Result:
case neg.intro.intro
α : Type u_2
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')

Proof state:
case neg.intro.intro
α : Type u_2
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')

Tactic:
exact ⟨x', y', ex, ey, isUnit_gcd_of_eq_mul_gcd ex ey h⟩

Result:
no goals