[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
⊢ ↑(algebraMap R S) x * invSelf x = 1
[PROOFSTEP]
convert IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 1
[GOAL]
case h.e'_2.h.e'_5
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
⊢ ↑(algebraMap R S) x = mk' S (↑{ val := x, property := (_ : x ∈ Submonoid.powers x) }) 1
[PROOFSTEP]
symm
[GOAL]
case h.e'_2.h.e'_5
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
⊢ mk' S (↑{ val := x, property := (_ : x ∈ Submonoid.powers x) }) 1 = ↑(algebraMap R S) x
[PROOFSTEP]
apply IsLocalization.mk'_one
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
g : R →+* P
hg : IsUnit (↑g x)
y : { x_1 // x_1 ∈ Submonoid.powers x }
⊢ IsUnit (↑g ↑y)
[PROOFSTEP]
obtain ⟨n, hn⟩ := y.2
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
g : R →+* P
hg : IsUnit (↑g x)
y : { x_1 // x_1 ∈ Submonoid.powers x }
n : ℕ
hn : (fun x x_1 => x ^ x_1) x n = ↑y
⊢ IsUnit (↑g ↑y)
[PROOFSTEP]
rw [← hn, g.map_pow]
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
g : R →+* P
hg : IsUnit (↑g x)
y : { x_1 // x_1 ∈ Submonoid.powers x }
n : ℕ
hn : (fun x x_1 => x ^ x_1) x n = ↑y
⊢ IsUnit (↑g x ^ n)
[PROOFSTEP]
exact IsUnit.map (powMonoidHom n : P →* P) hg
[GOAL]
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
P : Type u_3
inst✝³ : CommSemiring P
x : R
inst✝² : Away x S
g : R →+* P
y : R
inst✝¹ : Algebra R P
inst✝ : Away (x * y) P
⊢ ↑(algebraMap R P) x * mk' P y { val := x * y, property := (_ : x * y ∈ Submonoid.powers (x * y)) } = 1
[PROOFSTEP]
rw [mul_mk'_eq_mk'_of_mul, mk'_self]
[GOAL]
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
P : Type u_3
inst✝⁵ : CommSemiring P
x : R
inst✝⁴ : Away x S
g : R →+* P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (↑f r) Q
⊢ Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r))
[PROOFSTEP]
rintro x ⟨n, rfl⟩
[GOAL]
case intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
P : Type u_3
inst✝⁵ : CommSemiring P
x : R
inst✝⁴ : Away x S
g : R →+* P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (↑f r) Q
n : ℕ
⊢ (fun x x_1 => x ^ x_1) r n ∈ Submonoid.comap f (Submonoid.powers (↑f r))
[PROOFSTEP]
use n
[GOAL]
case h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
P : Type u_3
inst✝⁵ : CommSemiring P
x : R
inst✝⁴ : Away x S
g : R →+* P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (↑f r) Q
n : ℕ
⊢ (fun x x_1 => x ^ x_1) (↑f r) n = ↑f ((fun x x_1 => x ^ x_1) r n)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
⊢ R ≃ₐ[R] S
[PROOFSTEP]
refine' AlgEquiv.ofBijective (Algebra.ofId R S) ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
⊢ Function.Injective ↑(Algebra.ofId R S)
[PROOFSTEP]
intro x y hxy
[GOAL]
case refine'_1
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
x y : R
hxy : ↑(Algebra.ofId R S) x = ↑(Algebra.ofId R S) y
⊢ x = y
[PROOFSTEP]
obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy
[GOAL]
case refine'_1.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
x y : R
hxy : ↑(Algebra.ofId R S) x = ↑(Algebra.ofId R S) y
c : { x // x ∈ M }
eq : ↑c * x = ↑c * y
⊢ x = y
[PROOFSTEP]
obtain ⟨u, hu⟩ := H c
[GOAL]
case refine'_1.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
x y : R
hxy : ↑(Algebra.ofId R S) x = ↑(Algebra.ofId R S) y
c : { x // x ∈ M }
eq : ↑c * x = ↑c * y
u : Rˣ
hu : ↑u = ↑c
⊢ x = y
[PROOFSTEP]
rwa [← hu, Units.mul_right_inj] at eq 
[GOAL]
case refine'_2
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
⊢ Function.Surjective ↑(Algebra.ofId R S)
[PROOFSTEP]
intro y
[GOAL]
case refine'_2
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
y : S
⊢ ∃ a, ↑(Algebra.ofId R S) a = y
[PROOFSTEP]
obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y
[GOAL]
case refine'_2.intro.mk
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
y : S
x : R
s : { x // x ∈ M }
eq : y * ↑(algebraMap R S) ↑(x, s).snd = ↑(algebraMap R S) (x, s).fst
⊢ ∃ a, ↑(Algebra.ofId R S) a = y
[PROOFSTEP]
obtain ⟨u, hu⟩ := H s
[GOAL]
case refine'_2.intro.mk.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
y : S
x : R
s : { x // x ∈ M }
eq : y * ↑(algebraMap R S) ↑(x, s).snd = ↑(algebraMap R S) (x, s).fst
u : Rˣ
hu : ↑u = ↑s
⊢ ∃ a, ↑(Algebra.ofId R S) a = y
[PROOFSTEP]
use x * u.inv
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
y : S
x : R
s : { x // x ∈ M }
eq : y * ↑(algebraMap R S) ↑(x, s).snd = ↑(algebraMap R S) (x, s).fst
u : Rˣ
hu : ↑u = ↑s
⊢ ↑(Algebra.ofId R S) (x * u.inv) = y
[PROOFSTEP]
dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
y : S
x : R
s : { x // x ∈ M }
eq : y * ↑(algebraMap R S) ↑(x, s).snd = ↑(algebraMap R S) (x, s).fst
u : Rˣ
hu : ↑u = ↑s
⊢ ↑(algebraMap R S) (x * ↑u⁻¹) = y
[PROOFSTEP]
rw [RingHom.map_mul, ← eq, ← hu, mul_assoc, ← RingHom.map_mul]
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
H : ∀ (x : { x // x ∈ M }), IsUnit ↑x
y : S
x : R
s : { x // x ∈ M }
eq : y * ↑(algebraMap R S) ↑(x, s).snd = ↑(algebraMap R S) (x, s).fst
u : Rˣ
hu : ↑u = ↑s
⊢ y * ↑(algebraMap R S) (↑u * ↑u⁻¹) = y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
e : IsUnit x
inst✝ : Away x S
⊢ R ≃ₐ[R] S
[PROOFSTEP]
apply atUnits R (Submonoid.powers x)
[GOAL]
case H
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
e : IsUnit x
inst✝ : Away x S
⊢ ∀ (x_1 : { x_1 // x_1 ∈ Submonoid.powers x }), IsUnit ↑x_1
[PROOFSTEP]
rintro ⟨xn, n, hxn⟩
[GOAL]
case H.mk.intro
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
e : IsUnit x
inst✝ : Away x S
xn : R
n : ℕ
hxn : (fun x x_1 => x ^ x_1) x n = xn
⊢ IsUnit ↑{ val := xn, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = xn) }
[PROOFSTEP]
obtain ⟨u, hu⟩ := e
[GOAL]
case H.mk.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
inst✝ : Away x S
xn : R
n : ℕ
hxn : (fun x x_1 => x ^ x_1) x n = xn
u : Rˣ
hu : ↑u = x
⊢ IsUnit ↑{ val := xn, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = xn) }
[PROOFSTEP]
rw [isUnit_iff_exists_inv]
[GOAL]
case H.mk.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
inst✝ : Away x S
xn : R
n : ℕ
hxn : (fun x x_1 => x ^ x_1) x n = xn
u : Rˣ
hu : ↑u = x
⊢ ∃ b, ↑{ val := xn, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = xn) } * b = 1
[PROOFSTEP]
use u.inv ^ n
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
inst✝ : Away x S
xn : R
n : ℕ
hxn : (fun x x_1 => x ^ x_1) x n = xn
u : Rˣ
hu : ↑u = x
⊢ ↑{ val := xn, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = xn) } * u.inv ^ n = 1
[PROOFSTEP]
simp [← hxn, ← hu, ← mul_pow]
[GOAL]
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
⊢ ∀ (y : { x // x ∈ Submonoid.powers r }), IsUnit (↑(algebraMap R S) ↑y)
[PROOFSTEP]
rintro ⟨_, n, rfl⟩
[GOAL]
case mk.intro
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
n : ℕ
⊢ IsUnit
    (↑(algebraMap R S)
      ↑{ val := (fun x x_1 => x ^ x_1) r n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) r y = (fun x x_1 => x ^ x_1) r n) })
[PROOFSTEP]
exact (algebraMap R S).isUnit_map (hr.pow _)
[GOAL]
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
z : S
⊢ ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
[PROOFSTEP]
obtain ⟨z', rfl⟩ := H.2 z
[GOAL]
case intro
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
z' : R
⊢ ∃ x, ↑(algebraMap R S) z' * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
[PROOFSTEP]
exact ⟨⟨z', 1⟩, by simp⟩
[GOAL]
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
z' : R
⊢ ↑(algebraMap R S) z' * ↑(algebraMap R S) ↑(z', 1).snd = ↑(algebraMap R S) (z', 1).fst
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ ↑(algebraMap R S) x = ↑(algebraMap R S) y ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
erw [H.1.eq_iff]
[GOAL]
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ x = y ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
constructor
[GOAL]
case mp
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ x = y → ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x : R
⊢ ∃ c, ↑c * x = ↑c * x
[PROOFSTEP]
exact ⟨1, rfl⟩
[GOAL]
case mpr
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → x = y
[PROOFSTEP]
rintro ⟨⟨_, n, rfl⟩, e⟩
[GOAL]
case mpr.intro.mk.intro
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁶ : CommSemiring S✝
inst✝⁵ : Algebra R✝ S✝
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ↑(algebraMap R S)
x y : R
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) r n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) r y = (fun x x_1 => x ^ x_1) r n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) r n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) r y = (fun x x_1 => x ^ x_1) r n) } *
      y
⊢ x = y
[PROOFSTEP]
exact (hr.pow _).mul_right_inj.mp e
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
⊢ selfZpow x B 0 = 1
[PROOFSTEP]
simp [selfZpow_of_nonneg _ _ le_rfl]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
⊢ selfZpow x B n = mk' B 1 (Submonoid.pow x (Int.natAbs n))
[PROOFSTEP]
by_cases hn0 : n = 0
[GOAL]
case pos
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : n = 0
⊢ selfZpow x B n = mk' B 1 (Submonoid.pow x (Int.natAbs n))
[PROOFSTEP]
simp [hn0, selfZpow_zero, Submonoid.pow_apply]
[GOAL]
case neg
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZpow x B n = mk' B 1 (Submonoid.pow x (Int.natAbs n))
[PROOFSTEP]
simp [selfZpow_of_neg _ _ (lt_of_le_of_ne hn hn0)]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℕ
⊢ selfZpow x B (-↑d) = mk' B 1 (Submonoid.pow x d)
[PROOFSTEP]
simp [selfZpow_of_nonpos _ _ (neg_nonpos.mpr (Int.coe_nat_nonneg d))]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
⊢ selfZpow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
[PROOFSTEP]
by_cases h : m ≤ n
[GOAL]
case pos
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ selfZpow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
[PROOFSTEP]
rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h, selfZpow_coe_nat, ←
  map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h]
[GOAL]
case neg
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : ¬m ≤ n
⊢ selfZpow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
[PROOFSTEP]
rw [← neg_sub, ← Int.ofNat_sub (le_of_not_le h), selfZpow_neg_coe_nat, IsLocalization.mk'_eq_iff_eq]
[GOAL]
case neg
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : ¬m ≤ n
⊢ ↑(algebraMap R B) (↑(Submonoid.pow x m) * 1) = ↑(algebraMap R B) (↑(Submonoid.pow x (m - n)) * x ^ n)
[PROOFSTEP]
simp [Submonoid.pow_apply, ← pow_add, Nat.sub_add_cancel (le_of_not_le h)]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
⊢ selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m
[PROOFSTEP]
cases' le_or_lt 0 n with hn hn
[GOAL]
case inl
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
⊢ selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m
[PROOFSTEP]
cases' le_or_lt 0 m with hm hm
[GOAL]
case inr
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
⊢ selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m
[PROOFSTEP]
cases' le_or_lt 0 m with hm hm
[GOAL]
case inl.inl
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : 0 ≤ m
⊢ selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m
[PROOFSTEP]
rw [selfZpow_of_nonneg _ _ hn, selfZpow_of_nonneg _ _ hm, selfZpow_of_nonneg _ _ (add_nonneg hn hm),
  Int.natAbs_add_nonneg hn hm, pow_add]
[GOAL]
case inl.inr
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m
[PROOFSTEP]
have : n + m = n.natAbs - m.natAbs := by rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ n + m = ↑(Int.natAbs n) - ↑(Int.natAbs m)
[PROOFSTEP]
rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]
[GOAL]
case inl.inr
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
this : n + m = ↑(Int.natAbs n) - ↑(Int.natAbs m)
⊢ selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m
[PROOFSTEP]
rw [selfZpow_of_nonneg _ _ hn, selfZpow_of_neg _ _ hm, this, selfZpow_sub_cast_nat, IsLocalization.mk'_eq_mul_mk'_one,
  map_pow]
[GOAL]
case inr.inl
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
⊢ selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m
[PROOFSTEP]
have : n + m = m.natAbs - n.natAbs := by
  rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_comm]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
⊢ n + m = ↑(Int.natAbs m) - ↑(Int.natAbs n)
[PROOFSTEP]
rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_comm]
[GOAL]
case inr.inl
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
this : n + m = ↑(Int.natAbs m) - ↑(Int.natAbs n)
⊢ selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m
[PROOFSTEP]
rw [selfZpow_of_nonneg _ _ hm, selfZpow_of_neg _ _ hn, this, selfZpow_sub_cast_nat, IsLocalization.mk'_eq_mul_mk'_one,
  map_pow, mul_comm]
[GOAL]
case inr.inr
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m
[PROOFSTEP]
rw [selfZpow_of_neg _ _ hn, selfZpow_of_neg _ _ hm, selfZpow_of_neg _ _ (add_neg hn hm), Int.natAbs_add_neg hn hm, ←
  mk'_mul, one_mul]
[GOAL]
case inr.inr
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ mk' B 1 (Submonoid.pow x (Int.natAbs n + Int.natAbs m)) =
    mk' B 1 (Submonoid.pow x (Int.natAbs n) * Submonoid.pow x (Int.natAbs m))
[PROOFSTEP]
congr
[GOAL]
case inr.inr.e_y
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ Submonoid.pow x (Int.natAbs n + Int.natAbs m) = Submonoid.pow x (Int.natAbs n) * Submonoid.pow x (Int.natAbs m)
[PROOFSTEP]
ext
[GOAL]
case inr.inr.e_y.a
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ ↑(Submonoid.pow x (Int.natAbs n + Int.natAbs m)) = ↑(Submonoid.pow x (Int.natAbs n) * Submonoid.pow x (Int.natAbs m))
[PROOFSTEP]
simp [pow_add]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
⊢ selfZpow x B d * selfZpow x B (-d) = 1
[PROOFSTEP]
by_cases hd : d ≤ 0
[GOAL]
case pos
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ selfZpow x B d * selfZpow x B (-d) = 1
[PROOFSTEP]
erw [selfZpow_of_nonpos x B hd, selfZpow_of_nonneg, ← map_pow, Int.natAbs_neg, IsLocalization.mk'_spec, map_one]
[GOAL]
case pos.hn
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d
[PROOFSTEP]
apply nonneg_of_neg_nonpos
[GOAL]
case pos.hn.a
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ - -d ≤ 0
[PROOFSTEP]
rwa [neg_neg]
[GOAL]
case neg
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : ¬d ≤ 0
⊢ selfZpow x B d * selfZpow x B (-d) = 1
[PROOFSTEP]
erw [selfZpow_of_nonneg x B (le_of_not_le hd), selfZpow_of_nonpos, ← map_pow, Int.natAbs_neg,
  @IsLocalization.mk'_spec' R _ (Submonoid.powers x) B _ _ _ 1 (Submonoid.pow x d.natAbs), map_one]
[GOAL]
case neg.hn
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : ¬d ≤ 0
⊢ -d ≤ 0
[PROOFSTEP]
refine' nonpos_of_neg_nonneg (le_of_lt _)
[GOAL]
case neg.hn
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : ¬d ≤ 0
⊢ 0 < - -d
[PROOFSTEP]
rwa [neg_neg, ← not_le]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
⊢ selfZpow x B (-d) * selfZpow x B d = 1
[PROOFSTEP]
rw [mul_comm, selfZpow_mul_neg x B d]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
⊢ selfZpow x B (m - d) * mk' B a 1 = b ↔ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
[PROOFSTEP]
rw [sub_eq_add_neg, selfZpow_add, mul_assoc, mul_comm _ (mk' B a 1), ← mul_assoc]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b ↔ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b → selfZpow x B m * mk' B a 1 = selfZpow x B d * b
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
[PROOFSTEP]
have := congr_arg (fun s : B => s * selfZpow x B d) h
[GOAL]
case mp
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
this : (fun s => s * selfZpow x B d) (selfZpow x B m * mk' B a 1 * selfZpow x B (-d)) = (fun s => s * selfZpow x B d) b
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
[PROOFSTEP]
simp only at this 
[GOAL]
case mp
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
this : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) * selfZpow x B d = b * selfZpow x B d
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
[PROOFSTEP]
rwa [mul_assoc, mul_assoc, selfZpow_neg_mul, mul_one, mul_comm b _] at this 
[GOAL]
case mpr
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b → selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 = selfZpow x B d * b
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
[PROOFSTEP]
have := congr_arg (fun s : B => s * selfZpow x B (-d)) h
[GOAL]
case mpr
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 = selfZpow x B d * b
this :
  (fun s => s * selfZpow x B (-d)) (selfZpow x B m * mk' B a 1) = (fun s => s * selfZpow x B (-d)) (selfZpow x B d * b)
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
[PROOFSTEP]
simp only at this 
[GOAL]
case mpr
R : Type u_1
inst✝³ : CommRing R
x : R
B : Type u_2
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 = selfZpow x B d * b
this : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = selfZpow x B d * b * selfZpow x B (-d)
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
[PROOFSTEP]
rwa [mul_comm _ b, mul_assoc b _ _, selfZpow_mul_neg, mul_one] at this 
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
[PROOFSTEP]
obtain ⟨⟨a₀, y⟩, H⟩ := surj (Submonoid.powers x) b
[GOAL]
case intro.mk
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
[PROOFSTEP]
obtain ⟨d, hy⟩ := (Submonoid.mem_powers_iff y.1 x).mp y.2
[GOAL]
case intro.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
[PROOFSTEP]
have ha₀ : a₀ ≠ 0 :=
  by
  haveI :=
    @isDomain_of_le_nonZeroDivisors B _ R _ _ _ (Submonoid.powers x) _
      (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
  simp only [map_zero, ← hy, map_pow] at H 
  apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
  rw [← H]
  apply mul_ne_zero hb (pow_ne_zero _ _)
  exact
    IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
      (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)
  exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
⊢ a₀ ≠ 0
[PROOFSTEP]
haveI :=
  @isDomain_of_le_nonZeroDivisors B _ R _ _ _ (Submonoid.powers x) _
    (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
⊢ a₀ ≠ 0
[PROOFSTEP]
simp only [map_zero, ← hy, map_pow] at H 
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ a₀ ≠ 0
[PROOFSTEP]
apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ ¬↑(algebraMap R B) a₀ = 0
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
[PROOFSTEP]
rw [← H]
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ ¬b * ↑(algebraMap R B) x ^ d = 0
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
[PROOFSTEP]
apply mul_ne_zero hb (pow_ne_zero _ _)
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ ↑(algebraMap R B) x ≠ 0
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
[PROOFSTEP]
exact
  IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
    (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
[PROOFSTEP]
exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
[GOAL]
case intro.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
[PROOFSTEP]
simp only [← hy] at H 
[GOAL]
case intro.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
[PROOFSTEP]
classical
obtain ⟨m, a, hyp1, hyp2⟩ := max_power_factor ha₀ hx
refine' ⟨a, m - d, _⟩
rw [← mk'_one (M := Submonoid.powers x) B, selfZpow_pow_sub, selfZpow_coe_nat, selfZpow_coe_nat, ← map_pow _ _ d,
  mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m]
exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩
[GOAL]
case intro.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
[PROOFSTEP]
obtain ⟨m, a, hyp1, hyp2⟩ := max_power_factor ha₀ hx
[GOAL]
case intro.mk.intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
[PROOFSTEP]
refine' ⟨a, m - d, _⟩
[GOAL]
case intro.mk.intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ selfZpow x B (↑m - ↑d) * ↑(algebraMap R B) a = b
[PROOFSTEP]
rw [← mk'_one (M := Submonoid.powers x) B, selfZpow_pow_sub, selfZpow_coe_nat, selfZpow_coe_nat, ← map_pow _ _ d,
  mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m]
[GOAL]
case intro.mk.intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
x : R
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ ↑(algebraMap R B) x ^ m * mk' B a 1 = ↑(algebraMap R B) x ^ m * ↑(algebraMap R B) a
[PROOFSTEP]
exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩
