-- 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
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)

Tactic:
specialize h_frac ⟨PrimeSpectrum.comap f q, hqW⟩

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
⊢ 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.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
⊢ 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)

Tactic:
refine ⟨h_frac.1, ?_⟩

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
⊢ (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.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
⊢ (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)

Tactic:
dsimp only [comapFun]

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
⊢ (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)