-- Mathlib/RingTheory/RingHom/Surjective.lean
theorem surjective_localizationPreserves :
    LocalizationPreserves surjective

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
x : S'
⊢ ∃ a, (IsLocalization.map S' f ⋯) a = x

Tactic:
obtain ⟨x, ⟨_, s, hs, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (M.map f) x

Result:
case intro.intro.mk.intro.intro
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
x : S
s : R
hs : s ∈ ↑M
⊢ ∃ a, (IsLocalization.map S' f ⋯) a = IsLocalization.mk' S' x ⟨f s, ⋯⟩

Proof state:
case h
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
s : R
hs : s ∈ ↑M
y : R
⊢ (IsLocalization.map S' f ⋯) (IsLocalization.mk' R' y ⟨s, hs⟩) = IsLocalization.mk' S' (f y) ⟨f s, ⋯⟩

Tactic:
rw [IsLocalization.map_mk']

Result:
no goals

Proof state:
case intro.intro.mk.intro.intro
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
x : S
s : R
hs : s ∈ ↑M
⊢ ∃ a, (IsLocalization.map S' f ⋯) a = IsLocalization.mk' S' x ⟨f s, ⋯⟩

Tactic:
obtain ⟨y, rfl⟩ := H x

Result:
case intro.intro.mk.intro.intro.intro
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
s : R
hs : s ∈ ↑M
y : R
⊢ ∃ a, (IsLocalization.map S' f ⋯) a = IsLocalization.mk' S' (f y) ⟨f s, ⋯⟩

Proof state:
⊢ LocalizationPreserves fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f

Tactic:
introv R H x

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
x : S'
⊢ ∃ a, (IsLocalization.map S' f ⋯) a = x

Proof state:
case intro.intro.mk.intro.intro.intro
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
s : R
hs : s ∈ ↑M
y : R
⊢ ∃ a, (IsLocalization.map S' f ⋯) a = IsLocalization.mk' S' (f y) ⟨f s, ⋯⟩

Tactic:
use IsLocalization.mk' R' y ⟨s, hs⟩

Result:
case h
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
s : R
hs : s ∈ ↑M
y : R
⊢ (IsLocalization.map S' f ⋯) (IsLocalization.mk' R' y ⟨s, hs⟩) = IsLocalization.mk' S' (f y) ⟨f s, ⋯⟩