-- Mathlib/RingTheory/SurjectiveOnStalks.lean
/--
`R_p →+* S_q` is surjective if and only if
every `x : S` is of the form `f x / f r` for some `f r ∉ q`.
This is useful when proving `SurjectiveOnStalks`.
-/
lemma surjective_localRingHom_iff (P : Ideal S) [P.IsPrime] :
    Function.Surjective (Localization.localRingHom _ P f rfl) ↔
      ∀ s : S, ∃ x r : R, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x

Proof state:
case mp.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha : ∃ c, ↑c * f a = ↑c * (↑⟨f ↑t, ⋯⟩ * y)
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
obtain ⟨c, hc⟩ := ha

Result:
case mp.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
c : ↥P.primeCompl
hc : ↑c * f a = ↑c * (↑⟨f ↑t, ⋯⟩ * y)
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Proof state:
case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
obtain ⟨a, ha⟩ := H (IsLocalization.mk' _ y (1 : P.primeCompl))

Result:
case mp.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : Localization.AtPrime (Ideal.comap f P)
ha : (Localization.localRingHom (Ideal.comap f P) P f ⋯) a = IsLocalization.mk' (Localization.AtPrime P) y 1
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ tx ∈ (Ideal.comap f P).primeCompl

Tactic:
exact fun H ↦ mul_mem (P.primeCompl.mul_mem hyt ht) h (et ▸ Ideal.mul_mem_left _ yt H)

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ ∃ a, (Localization.localRingHom (Ideal.comap f P) P f ⋯) a = Localization.mk y ⟨t, h⟩

Tactic:
refine ⟨Localization.mk (yx * ts) ⟨ys * tx, Submonoid.mul_mem _ hy ?_⟩, ?_⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ tx ∈ (Ideal.comap f P).primeCompl

case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯) (Localization.mk (yx * ts) ⟨ys * tx, ⋯⟩) =
    Localization.mk y ⟨t, h⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) ↔
    ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) →
    ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x

case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ (∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x) →
    Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)

Proof state:
case mp.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha :
  (Localization.localRingHom (Ideal.comap f P) P f ⋯)
      (IsLocalization.mk' (Localization.AtPrime (Ideal.comap f P)) a t) =
    IsLocalization.mk' (Localization.AtPrime P) y 1
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
rw [Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq,
  Submonoid.coe_one, one_mul, IsLocalization.eq_iff_exists P.primeCompl] at ha

Result:
case mp.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha : ∃ c, ↑c * f a = ↑c * (↑⟨f ↑t, ⋯⟩ * y)
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ ∃ c, ↑c * (t * (f yx * f ts)) = ↑c * (f ys * f tx * y)

Tactic:
refine ⟨⟨yc, hyc⟩ * ⟨yt, hyt⟩, ?_⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ ↑(⟨yc, hyc⟩ * ⟨yt, hyt⟩) * (t * (f yx * f ts)) = ↑(⟨yc, hyc⟩ * ⟨yt, hyt⟩) * (f ys * f tx * y)