[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 _ _)⟩


[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H✝ : IsCoprime x y
a b : R
H : a * x + b * y = 1
⊢ b * y + a * x = 1
[PROOFSTEP]
rw [add_comm, H]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
x✝ : IsCoprime x x
a b : R
h : a * x + b * x = 1
⊢ x * (a + b) = 1
[PROOFSTEP]
rwa [mul_comm, add_mul]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsUnit x
b : R
hb : b * x = 1
⊢ b * x + 0 * x = 1
[PROOFSTEP]
rwa [zero_mul, add_zero]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
x✝ : IsCoprime 0 x
a b : R
H : a * 0 + b * x = 1
⊢ x * b = 1
[PROOFSTEP]
rwa [mul_zero, zero_add, mul_comm] at H
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsUnit x
b : R
hb : b * x = 1
⊢ 1 * 0 + b * x = 1
[PROOFSTEP]
rwa [one_mul, zero_add]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
x y z : R
inst✝ : Nontrivial R
p : Fin 2 → R
h : IsCoprime (p 0) (p 1)
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
x y z : R
inst✝ : Nontrivial R
h : IsCoprime (OfNat.ofNat 0 0) (OfNat.ofNat 0 1)
⊢ False
[PROOFSTEP]
exact not_isCoprime_zero_zero h
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
x y z : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x ≠ 0 ∨ y ≠ 0
[PROOFSTEP]
apply not_or_of_imp
[GOAL]
case a
R : Type u
inst✝¹ : CommSemiring R
x y z : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x = 0 → y ≠ 0
[PROOFSTEP]
rintro rfl rfl
[GOAL]
case a
R : Type u
inst✝¹ : CommSemiring R
z : R
inst✝ : Nontrivial R
h : IsCoprime 0 0
⊢ False
[PROOFSTEP]
exact not_isCoprime_zero_zero h
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ 1 * 1 + 0 * x = 1
[PROOFSTEP]
rw [one_mul, zero_mul, add_zero]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ 0 * x + 1 * 1 = 1
[PROOFSTEP]
rw [one_mul, zero_mul, zero_add]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
⊢ x ∣ y
[PROOFSTEP]
let ⟨a, b, H⟩ := H1
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y
[PROOFSTEP]
rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y * a * x + b * (y * z)
[PROOFSTEP]
exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
⊢ x ∣ z
[PROOFSTEP]
let ⟨a, b, H⟩ := H1
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ z
[PROOFSTEP]
rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ a * z * x + b * (y * z)
[PROOFSTEP]
exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ a * c * (x * y) + (a * x * d + b * c * y + b * d * z) * z = (a * x + b * z) * (c * y + d * z)
[PROOFSTEP]
ring
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ (a * x + b * z) * (c * y + d * z) = 1
[PROOFSTEP]
rw [h1, h2, mul_one]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : IsCoprime x z
⊢ IsCoprime x (y * z)
[PROOFSTEP]
rw [isCoprime_comm] at H1 H2 ⊢
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime y x
H2 : IsCoprime z x
⊢ IsCoprime (y * z) x
[PROOFSTEP]
exact H1.mul_left H2
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x y
H1 : x ∣ z
H2 : y ∣ z
⊢ x * y ∣ z
[PROOFSTEP]
obtain ⟨a, b, h⟩ := H
[GOAL]
case intro.intro
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z
[PROOFSTEP]
rw [← mul_one z, ← h, mul_add]
[GOAL]
case intro.intro
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x) + z * (b * y)
[PROOFSTEP]
apply dvd_add
[GOAL]
case intro.intro.h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x)
[PROOFSTEP]
rw [mul_comm z, mul_assoc]
[GOAL]
case intro.intro.h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ a * (x * z)
[PROOFSTEP]
exact (mul_dvd_mul_left _ H2).mul_left _
[GOAL]
case intro.intro.h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (b * y)
[PROOFSTEP]
rw [mul_comm b, ← mul_assoc]
[GOAL]
case intro.intro.h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * y * b
[PROOFSTEP]
exact (mul_dvd_mul_right H1 _).mul_right _
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (x * y) z
a b : R
h : a * (x * y) + b * z = 1
⊢ a * y * x + b * z = 1
[PROOFSTEP]
rwa [mul_right_comm, mul_assoc]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (x * y) z
⊢ IsCoprime y z
[PROOFSTEP]
rw [mul_comm] at H
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (y * x) z
⊢ IsCoprime y z
[PROOFSTEP]
exact H.of_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
⊢ IsCoprime x y
[PROOFSTEP]
rw [isCoprime_comm] at H ⊢
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (y * z) x
⊢ IsCoprime y x
[PROOFSTEP]
exact H.of_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
⊢ IsCoprime x z
[PROOFSTEP]
rw [mul_comm] at H
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (z * y)
⊢ IsCoprime x z
[PROOFSTEP]
exact H.of_mul_right_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
[PROOFSTEP]
rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime y z
hdvd : x ∣ y
⊢ IsCoprime x z
[PROOFSTEP]
obtain ⟨d, rfl⟩ := hdvd
[GOAL]
case intro
R : Type u
inst✝ : CommSemiring R
x z d : R
h : IsCoprime (x * d) z
⊢ IsCoprime x z
[PROOFSTEP]
exact IsCoprime.of_mul_left_left h
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
x y z : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ ↑f a * ↑f x + ↑f b * ↑f y = 1
[PROOFSTEP]
rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
a b : R
H : a * (x + y * z) + b * y = 1
⊢ a * x + (a * z + b) * y = 1
[PROOFSTEP]
simpa only [add_mul, mul_add, add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm, mul_left_comm] using H
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y
[PROOFSTEP]
rw [mul_comm] at h
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
[PROOFSTEP]
rw [isCoprime_comm] at h ⊢
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x
[PROOFSTEP]
exact h.of_add_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y
[PROOFSTEP]
rw [mul_comm] at h
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_left_right
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y * z + x) y
⊢ IsCoprime x y
[PROOFSTEP]
rw [add_comm] at h
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (z * y + x) y
⊢ IsCoprime x y
[PROOFSTEP]
rw [add_comm] at h
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_right_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (x * z + y)
⊢ IsCoprime x y
[PROOFSTEP]
rw [add_comm] at h
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_left_right
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (z * x + y)
⊢ IsCoprime x y
[PROOFSTEP]
rw [add_comm] at h
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_right_right
[GOAL]
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime (x • y) z
a b : R
h : a * x • y + b * z = 1
⊢ x • a * y + b * z = 1
[PROOFSTEP]
rwa [smul_mul_assoc, ← mul_smul_comm]
[GOAL]
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime y z
a b : R
h : a * y + b * z = 1
⊢ x⁻¹ • a * x • y + b * z = 1
[PROOFSTEP]
rwa [smul_mul_smul, inv_mul_self, one_smul]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z + y * -z) y
[PROOFSTEP]
simpa only [mul_neg, add_neg_cancel_right] using h
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z) y
[PROOFSTEP]
exact h.add_mul_left_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + x * z)
[PROOFSTEP]
rw [isCoprime_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + x * z) x
[PROOFSTEP]
exact h.symm.add_mul_left_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)
[PROOFSTEP]
rw [isCoprime_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + z * x) x
[PROOFSTEP]
exact h.symm.add_mul_right_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y * z + x) y
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z) y
[PROOFSTEP]
exact h.add_mul_left_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (z * y + x) y
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y
[PROOFSTEP]
exact h.add_mul_right_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (x * z + y)
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + x * z)
[PROOFSTEP]
exact h.add_mul_left_right z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (z * x + y)
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)
[PROOFSTEP]
exact h.add_mul_right_right z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
⊢ IsCoprime (-x) y
[PROOFSTEP]
obtain ⟨a, b, h⟩ := h
[GOAL]
case intro.intro
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ IsCoprime (-x) y
[PROOFSTEP]
use-a, b
[GOAL]
case h
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ -a * -x + b * y = 1
[PROOFSTEP]
rwa [neg_mul_neg]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
⊢ a ^ 2 + b ^ 2 ≠ 0
[PROOFSTEP]
intro h'
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ False
[PROOFSTEP]
obtain ⟨ha, hb⟩ :=
  (add_eq_zero_iff' (by rw [pow_two]; exact mul_self_nonneg _) (by rw [pow_two]; exact mul_self_nonneg _)).mp h'
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ a ^ 2
[PROOFSTEP]
rw [pow_two]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ a * a
[PROOFSTEP]
exact mul_self_nonneg _
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ b ^ 2
[PROOFSTEP]
rw [pow_two]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ b * b
[PROOFSTEP]
exact mul_self_nonneg _
[GOAL]
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
ha : a ^ 2 = 0
hb : b ^ 2 = 0
⊢ False
[PROOFSTEP]
obtain rfl := pow_eq_zero ha
[GOAL]
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
b : R
hb : b ^ 2 = 0
h : IsCoprime 0 b
h' : 0 ^ 2 + b ^ 2 = 0
ha : 0 ^ 2 = 0
⊢ False
[PROOFSTEP]
obtain rfl := pow_eq_zero hb
[GOAL]
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
ha hb : 0 ^ 2 = 0
h : IsCoprime 0 0
h' : 0 ^ 2 + 0 ^ 2 = 0
⊢ False
[PROOFSTEP]
exact not_isCoprime_zero_zero h