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
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
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.mk'_surjective M z
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
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
obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y
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')
⊢ mk' A x { val := y, property := hy } * ↑(algebraMap R A) y' = ↑(algebraMap R A) x'
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
use x', y', hu
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')
⊢ mk' A (y' * x) { val := y, property := hy } = ↑(algebraMap R A) x'
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')
⊢ mk' A x { val := y, property := hy } * ↑(algebraMap R A) y' = ↑(algebraMap R A) x'
rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]
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'
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')
⊢ mk' A (y' * x) { val := y, property := hy } = ↑(algebraMap R A) x'
convert IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2
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')
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'
rw [Subtype.coe_mk, hy', ← mul_comm y', mul_assoc]
no goals
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')
conv_lhs => rw [hx']