-- Mathlib/RingTheory/RingHom/Surjective.lean
theorem surjective_ofLocalizationSpan : OfLocalizationSpan surjective

Proof state:
case H.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
a : Localization.Away ↑r
e' : (Localization.awayMap f ↑r) a = (algebraMap S (Localization.Away (f ↑r))) x
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Tactic:
obtain ⟨b, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers (r : R)) a

Result:
case H.intro.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (Localization.awayMap f ↑r) (IsLocalization.mk' (Localization.Away ↑r) b ⟨(fun x => ↑r ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) x
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Proof state:
case H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : ↑⟨(fun x => f ↑r ^ x) n', ⋯⟩ * (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) = ↑⟨(fun x => f ↑r ^ x) n', ⋯⟩ * f b
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Tactic:
dsimp only at e''

Result:
case H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f ↑r ^ n' * (x * f (↑r ^ n)) = f ↑r ^ n' * f b
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Proof state:
case H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f (↑r ^ (n' + n)) * x = f (↑r ^ n' * b)
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Tactic:
exact ⟨n' + n, _, e''.symm⟩

Result:
no goals

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
⊢ Function.Surjective ⇑f

Tactic:
rw [← Set.range_eq_univ, Set.eq_univ_iff_forall]

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
⊢ ∀ (x : S), x ∈ Set.range ⇑f

Proof state:
case H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f ↑r ^ n' * (x * f (↑r ^ n)) = f ↑r ^ n' * f b
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Tactic:
rw [mul_comm x, ← mul_assoc, ← map_pow, ← map_mul, ← map_mul, ← pow_add] at e''

Result:
case H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f (↑r ^ (n' + n)) * x = f (↑r ^ n' * b)
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Proof state:
case H.intro.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Tactic:
obtain ⟨⟨_, n', rfl⟩, e''⟩ := (IsLocalization.eq_iff_exists (Submonoid.powers (f r)) _).mp e'

Result:
case H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : ↑⟨(fun x => f ↑r ^ x) n', ⋯⟩ * (x * ↑⟨f ↑⟨(fun x => ↑r ^ x) n, ⋯⟩, ⋯⟩) = ↑⟨(fun x => f ↑r ^ x) n', ⋯⟩ * f b
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Proof state:
case H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
⊢ ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Tactic:
intro r

Result:
case H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Proof state:
case H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)

Tactic:
obtain ⟨a, e'⟩ := H r (algebraMap _ _ x)

Result:
case H.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
a : Localization.Away ↑r
e' : (Localization.awayMap f ↑r) a = (algebraMap S (Localization.Away (f ↑r))) x
⊢ ∃ n, ↑r ^ n • x ∈ LinearMap.range (Algebra.linearMap R S)