[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
z : A
⊢ ∃ a b, IsUnit (gcd a b) ∧ z * ↑(algebraMap R A) b = ↑(algebraMap R A) a
[PROOFSTEP]
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.mk'_surjective M z
[GOAL]
case intro.intro.mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
⊢ ∃ a b, IsUnit (gcd a b) ∧ mk' A x { val := y, property := hy } * ↑(algebraMap R A) b = ↑(algebraMap R A) a
[PROOFSTEP]
obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y
[GOAL]
case intro.intro.mk.intro.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ ∃ a b, IsUnit (gcd a b) ∧ mk' A x { val := y, property := hy } * ↑(algebraMap R A) b = ↑(algebraMap R A) a
[PROOFSTEP]
use x', y', hu
[GOAL]
case right
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ mk' A x { val := y, property := hy } * ↑(algebraMap R A) y' = ↑(algebraMap R A) x'
[PROOFSTEP]
rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]
[GOAL]
case right
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ mk' A (y' * x) { val := y, property := hy } = ↑(algebraMap R A) x'
[PROOFSTEP]
convert IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2
[GOAL]
case h.e'_2.h.e'_8
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ y' * x = ↑{ val := y, property := hy } * x'
[PROOFSTEP]
rw [Subtype.coe_mk, hy', ← mul_comm y', mul_assoc]
[GOAL]
case h.e'_2.h.e'_8
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ y' * x = y' * (gcd x y * x')
[PROOFSTEP]
conv_lhs => rw [hx']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
| y' * x
[PROOFSTEP]
rw [hx']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
| y' * x
[PROOFSTEP]
rw [hx']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
| y' * x
[PROOFSTEP]
rw [hx']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = X
[PROOFSTEP]
obtain ⟨x, y, hg, he⟩ := IsLocalization.surj_of_gcd_domain (nonZeroDivisors R) X
[GOAL]
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = X
[PROOFSTEP]
have :=
  Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero (IsFractionRing.injective R <| FractionRing R) hp₁ y x _ hp₂
    (by rw [mul_comm, he])
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
⊢ ↑(algebraMap R (FractionRing R)) y * X = ↑(algebraMap R (FractionRing R)) x
[PROOFSTEP]
rw [mul_comm, he]
[GOAL]
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this : y ∣ x ^ Polynomial.natDegree p
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = X
[PROOFSTEP]
have : IsUnit y := by
  rw [isUnit_iff_dvd_one, ← one_pow]
  exact
    (dvd_gcd this <| dvd_refl y).trans
      (gcd_pow_left_dvd_pow_gcd.trans <| pow_dvd_pow_of_dvd (isUnit_iff_dvd_one.1 hg) _)
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this : y ∣ x ^ Polynomial.natDegree p
⊢ IsUnit y
[PROOFSTEP]
rw [isUnit_iff_dvd_one, ← one_pow]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this : y ∣ x ^ Polynomial.natDegree p
⊢ y ∣ 1 ^ ?m.56326
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this : y ∣ x ^ Polynomial.natDegree p
⊢ ℕ
[PROOFSTEP]
exact
  (dvd_gcd this <| dvd_refl y).trans (gcd_pow_left_dvd_pow_gcd.trans <| pow_dvd_pow_of_dvd (isUnit_iff_dvd_one.1 hg) _)
[GOAL]
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ Polynomial.natDegree p
this : IsUnit y
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = X
[PROOFSTEP]
use x * (this.unit⁻¹ : _)
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ Polynomial.natDegree p
this : IsUnit y
⊢ ↑(algebraMap R (FractionRing R)) (x * ↑(IsUnit.unit this)⁻¹) = X
[PROOFSTEP]
erw [map_mul, ← Units.coe_map_inv, eq_comm, Units.eq_mul_inv_iff_mul_eq]
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ Polynomial.natDegree p
this : IsUnit y
⊢ X * ↑(↑(Units.map ↑(algebraMap R (FractionRing R))) (IsUnit.unit this)) = ↑(algebraMap R (FractionRing R)) x
[PROOFSTEP]
exact he
