M : Type ?u.9200
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ GCDMonoid.gcd a b ∣ 1
M : Type ?u.9200
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ ∃ d, a = d ^ n
refine' exists_eq_pow_of_mul_eq_pow (isUnit_of_dvd_one _) h
case intro.intro
M : Type ?u.9200
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ 1
M : Type ?u.9200
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ GCDMonoid.gcd a b ∣ 1
obtain ⟨x, y, hxy⟩ := cp
case intro.intro
M : Type ?u.9200
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b
case intro.intro
M : Type ?u.9200
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ 1
rw [← hxy]
no goals
case intro.intro
M : Type ?u.9200
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b
exact  dvd_add (dvd_mul_of_dvd_right (GCDMonoid.gcd_dvd_left _ _) _)
    (dvd_mul_of_dvd_right (GCDMonoid.gcd_dvd_right _ _) _)