R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r' : L
⊢ ∃ a, ↑(algebraMap R L) a = r'
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ Surjective ↑(algebraMap R L)
intro r'
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
⊢ ∃ a, ↑(algebraMap R L) a = IsLocalization.mk' L r₁ s
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r' : L
⊢ ∃ a, ↑(algebraMap R L) a = r'
obtain ⟨r₁, s, rfl⟩ := IsLocalization.mk'_surjective S r'
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
⊢ ∃ r, IsLocalization.mk' L 1 s = ↑(algebraMap R L) r

case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
r₂ : R
h : IsLocalization.mk' L 1 s = ↑(algebraMap R L) r₂
⊢ ∃ a, ↑(algebraMap R L) a = IsLocalization.mk' L r₁ s
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
⊢ ∃ a, ↑(algebraMap R L) a = IsLocalization.mk' L r₁ s
obtain ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
r₂ : R
h : IsLocalization.mk' L 1 s = ↑(algebraMap R L) r₂
⊢ ∃ a, ↑(algebraMap R L) a = IsLocalization.mk' L r₁ s

R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
⊢ ∃ r, IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
⊢ ∃ r, IsLocalization.mk' L 1 s = ↑(algebraMap R L) r

case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
r₂ : R
h : IsLocalization.mk' L 1 s = ↑(algebraMap R L) r₂
⊢ ∃ a, ↑(algebraMap R L) a = IsLocalization.mk' L r₁ s
swap
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑s ^ Nat.succ n • r = ↑s ^ n • 1
⊢ ∃ r, IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
⊢ ∃ r, IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R)
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑s ^ Nat.succ n • r = ↑s ^ n • 1
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑s ^ Nat.succ n • r = ↑s ^ n • 1
⊢ ∃ r, IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
use r
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑s ^ n * (↑s * r) = ↑s ^ n * 1
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑s ^ Nat.succ n • r = ↑s ^ n • 1
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
rw [smul_eq_mul, smul_eq_mul, pow_succ', mul_assoc] at hr
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑(algebraMap R L) (↑s ^ n * (↑s * r)) = ↑(algebraMap R L) (↑s ^ n * 1)
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑s ^ n * (↑s * r) = ↑s ^ n * 1
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
apply_fun algebraMap R L at hr
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr :
  ↑(algebraMap R L) (↑s ^ n) * (↑(algebraMap R L) ↑s * ↑(algebraMap R L) r) =
    ↑(algebraMap R L) (↑s ^ n) * ↑(algebraMap R L) 1
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr : ↑(algebraMap R L) (↑s ^ n * (↑s * r)) = ↑(algebraMap R L) (↑s ^ n * 1)
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
simp only [map_mul] at hr
no goals
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
n : ℕ
r : R
hr :
  ↑(algebraMap R L) (↑s ^ n) * (↑(algebraMap R L) ↑s * ↑(algebraMap R L) r) =
    ↑(algebraMap R L) (↑s ^ n) * ↑(algebraMap R L) 1
⊢ IsLocalization.mk' L 1 s = ↑(algebraMap R L) r
rw [← IsLocalization.mk'_one (M := S) L, IsLocalization.mk'_eq_iff_eq, mul_one, Submonoid.coe_one,
  ← (IsLocalization.map_units L (s ^ n)).mul_left_cancel hr, map_mul]
no goals
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
r₂ : R
h : IsLocalization.mk' L 1 s = ↑(algebraMap R L) r₂
⊢ ∃ a, ↑(algebraMap R L) a = IsLocalization.mk' L r₁ s
exact ⟨r₁ * r₂, by rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]⟩
no goals
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : { x // x ∈ S }
r₂ : R
h : IsLocalization.mk' L 1 s = ↑(algebraMap R L) r₂
⊢ ↑(algebraMap R L) (r₁ * r₂) = IsLocalization.mk' L r₁ s
rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]