-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem comapFunIsLocallyFraction (f : R →+* S) (U : Opens (PrimeSpectrum.Top R))
    (V : Opens (PrimeSpectrum.Top S)) (hUV : V.1 ⊆ PrimeSpectrum.comap f ⁻¹' U.1)
    (s : ∀ x : U, Localizations R x) (hs : (isLocallyFraction R).toPrelocalPredicate.pred s) :
    (isLocallyFraction S).toPrelocalPredicate.pred (comapFun f U V hUV s)

Proof state:
case mk.intro.intro.intro.intro.intro.mk.intro
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W
iWU : W ⟶ U
a b : R
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑((Opens.comap (PrimeSpectrum.comap f)) W)
hqV : q ∈ ↑V
h_frac :
  b ∉ (↑⟨(PrimeSpectrum.comap f) q, hqW⟩).asIdeal ∧
    (fun x => s (iWU x)) ⟨(PrimeSpectrum.comap f) q, hqW⟩ *
        (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) b =
      (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) a
⊢ (Localization.localRingHom
          ((PrimeSpectrum.comap f) ↑((((Opens.comap (PrimeSpectrum.comap f)) W).infLERight V) ⟨q, ⋯⟩)).asIdeal
          (↑((((Opens.comap (PrimeSpectrum.comap f)) W).infLERight V) ⟨q, ⋯⟩)).asIdeal f ⋯)
        (s ⟨(PrimeSpectrum.comap f) ↑((((Opens.comap (PrimeSpectrum.comap f)) W).infLERight V) ⟨q, ⋯⟩), ⋯⟩) *
      (algebraMap S (Localizations S q)) (f b) =
    (algebraMap S (Localizations S q)) (f a)

Tactic:
erw [← Localization.localRingHom_to_map (PrimeSpectrum.comap f q).asIdeal, ← RingHom.map_mul,
  h_frac.2, Localization.localRingHom_to_map]

Result:
case mk.intro.intro.intro.intro.intro.mk.intro
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W
iWU : W ⟶ U
a b : R
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑((Opens.comap (PrimeSpectrum.comap f)) W)
hqV : q ∈ ↑V
h_frac :
  b ∉ (↑⟨(PrimeSpectrum.comap f) q, hqW⟩).asIdeal ∧
    (fun x => s (iWU x)) ⟨(PrimeSpectrum.comap f) q, hqW⟩ *
        (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) b =
      (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) a
⊢ (algebraMap S (Localization.AtPrime (↑((((Opens.comap (PrimeSpectrum.comap f)) W).infLERight V) ⟨q, ⋯⟩)).asIdeal))
      (f a) =
    (algebraMap S (Localizations S q)) (f a)

Proof state:
case mk.intro.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W
iWU : W ⟶ U
a b : R
h_frac :
  ∀ (x : ↥W),
    b ∉ (↑x).asIdeal ∧
      (fun x => s (iWU x)) x * (algebraMap R (Localizations R ↑x)) b = (algebraMap R (Localizations R ↑x)) a
⊢ ∀ (x : ↥((Opens.comap (PrimeSpectrum.comap f)) W ⊓ V)),
    f b ∉ (↑x).asIdeal ∧
      (fun x => comapFun f U V hUV s ((((Opens.comap (PrimeSpectrum.comap f)) W).infLERight V) x)) x *
          (algebraMap S (Localizations S ↑x)) (f b) =
        (algebraMap S (Localizations S ↑x)) (f a)

Tactic:
rintro ⟨q, ⟨hqW, hqV⟩⟩

Result:
case mk.intro.intro.intro.intro.intro.mk.intro
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W
iWU : W ⟶ U
a b : R
h_frac :
  ∀ (x : ↥W),
    b ∉ (↑x).asIdeal ∧
      (fun x => s (iWU x)) x * (algebraMap R (Localizations R ↑x)) b = (algebraMap R (Localizations R ↑x)) a
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑((Opens.comap (PrimeSpectrum.comap f)) W)
hqV : q ∈ ↑V
⊢ f b ∉ (↑⟨q, ⋯⟩).asIdeal ∧
    (fun x => comapFun f U V hUV s ((((Opens.comap (PrimeSpectrum.comap f)) W).infLERight V) x)) ⟨q, ⋯⟩ *
        (algebraMap S (Localizations S ↑⟨q, ⋯⟩)) (f b) =
      (algebraMap S (Localizations S ↑⟨q, ⋯⟩)) (f a)

Proof state:
case mk.intro.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W
iWU : W ⟶ U
a b : R
h_frac :
  ∀ (x : ↥W),
    b ∉ (↑x).asIdeal ∧
      (fun x => s (iWU x)) x * (algebraMap R (Localizations R ↑x)) b = (algebraMap R (Localizations R ↑x)) a
⊢ ∃ V_1, ∃ (_ : ↑⟨p, hpV⟩ ∈ V_1), ∃ i, (isFractionPrelocal S).pred fun x => comapFun f U V hUV s (i x)

Tactic:
refine ⟨Opens.comap (PrimeSpectrum.comap f) W ⊓ V, ⟨m, hpV⟩, Opens.infLERight _ _, f a, f b, ?_⟩

Result:
case mk.intro.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W
iWU : W ⟶ U
a b : R
h_frac :
  ∀ (x : ↥W),
    b ∉ (↑x).asIdeal ∧
      (fun x => s (iWU x)) x * (algebraMap R (Localizations R ↑x)) b = (algebraMap R (Localizations R ↑x)) a
⊢ ∀ (x : ↥((Opens.comap (PrimeSpectrum.comap f)) W ⊓ V)),
    f b ∉ (↑x).asIdeal ∧
      (fun x => comapFun f U V hUV s ((((Opens.comap (PrimeSpectrum.comap f)) W).infLERight V) x)) x *
          (algebraMap S (Localizations S ↑x)) (f b) =
        (algebraMap S (Localizations S ↑x)) (f a)

Proof state:
case mk.intro.intro.intro.intro.intro.mk.intro
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
s : (x : ↥U) → Localizations R ↑x
hs : (isLocallyFraction R).pred s
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W
iWU : W ⟶ U
a b : R
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑((Opens.comap (PrimeSpectrum.comap f)) W)
hqV : q ∈ ↑V
h_frac :
  b ∉ (↑⟨(PrimeSpectrum.comap f) q, hqW⟩).asIdeal ∧
    (fun x => s (iWU x)) ⟨(PrimeSpectrum.comap f) q, hqW⟩ *
        (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) b =
      (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) a
⊢ (algebraMap S (Localization.AtPrime (↑((((Opens.comap (PrimeSpectrum.comap f)) W).infLERight V) ⟨q, ⋯⟩)).asIdeal))
      (f a) =
    (algebraMap S (Localizations S q)) (f a)

Tactic:
rfl

Result:
no goals