-- Mathlib/RingTheory/Artinian/Ring.lean
theorem localization_surjective : Function.Surjective (algebraMap R L)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ Function.Surjective ⇑(algebraMap R L)

Tactic:
intro r'

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r' : L
⊢ ∃ a, (algebraMap R L) a = r'

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L) r₂
⊢ ∃ a, (algebraMap R L) a = IsLocalization.mk' L r₁ s

Tactic:
exact ⟨r₁ * r₂, by rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n.succ • r = ↑s ^ n • 1
⊢ ∃ r, IsLocalization.mk' L 1 s = (algebraMap R L) r

Tactic:
use r

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n.succ • r = ↑s ^ n • 1
⊢ IsLocalization.mk' L 1 s = (algebraMap R L) r

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n * (↑s * r) = ↑s ^ n * 1
⊢ IsLocalization.mk' L 1 s = (algebraMap R L) r

Tactic:
apply_fun algebraMap R L at hr

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥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

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥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

Tactic:
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]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L) r₂
⊢ (algebraMap R L) (r₁ * r₂) = IsLocalization.mk' L r₁ s

Tactic:
rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r' : L
⊢ ∃ a, (algebraMap R L) a = r'

Tactic:
obtain ⟨r₁, s, rfl⟩ := IsLocalization.mk'_surjective S r'

Result:
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
⊢ ∃ a, (algebraMap R L) a = IsLocalization.mk' L r₁ s

Proof state:
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
⊢ ∃ a, (algebraMap R L) a = IsLocalization.mk' L r₁ s

Tactic:
rsuffices ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥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✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
⊢ ∃ r, IsLocalization.mk' L 1 s = (algebraMap R L) r

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n.succ • r = ↑s ^ n • 1
⊢ IsLocalization.mk' L 1 s = (algebraMap R L) r

Tactic:
rw [smul_eq_mul, smul_eq_mul, pow_succ, mul_assoc] at hr

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n * (↑s * r) = ↑s ^ n * 1
⊢ IsLocalization.mk' L 1 s = (algebraMap R L) r

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
⊢ ∃ r, IsLocalization.mk' L 1 s = (algebraMap R L) r

Tactic:
obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R)

Result:
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n.succ • r = ↑s ^ n • 1
⊢ ∃ r, IsLocalization.mk' L 1 s = (algebraMap R L) r

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥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

Tactic:
simp only [map_mul] at hr

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥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