-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem comap_id_eq_map (U V : Opens (PrimeSpectrum.Top R)) (iVU : V ⟶ U) :
    (comap (RingHom.id R) U V fun _ hpV => leOfHom iVU <| hpV) =
      ((structureSheaf R).1.map iVU.op).hom :=
  RingHom.ext fun s => Subtype.eq <| funext fun p => by
    rw [comap_apply]
    -- Unfortunately, we cannot use `Localization.localRingHom_id` here, because
    -- `PrimeSpectrum.comap (RingHom.id R) p` is not *definitionally* equal to `p`. Instead, we use
    -- that we can write `s` as a fraction `a/b` in a small neighborhood around `p`. Since
    -- `PrimeSpectrum.comap (RingHom.id R) p` equals `p`, it is also contained in the same
    -- neighborhood, hence `s` equals `a/b` there too.
    obtain ⟨W, hpW, iWU, h⟩ := s.2 (iVU p)
    obtain ⟨a, b, h'⟩ := h.eq_mk'
    obtain ⟨hb₁, s_eq₁⟩ := h' ⟨p, hpW⟩
    obtain ⟨hb₂, s_eq₂⟩ :=
      h' ⟨PrimeSpectrum.comap (RingHom.id _) p.1, hpW⟩
    dsimp only at s_eq₁ s_eq₂
    erw [s_eq₂, Localization.localRingHom_mk', ← s_eq₁, ← res_apply _ _ _ iVU]

Proof state:
case intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op V))
W : Opens ↑(PrimeSpectrum.Top R)
hpW : ↑(iVU p) ∈ W
iWU : W ⟶ unop (op U)
h : (isFractionPrelocal R).pred fun x => ↑s (iWU x)
a b : R
h' :
  ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), ↑s (iWU x) = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) a ⟨b, hs⟩
⊢ (Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).val.map iVU.op)) s) p

Tactic:
obtain ⟨hb₁, s_eq₁⟩ := h' ⟨p, hpW⟩

Result:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op V))
W : Opens ↑(PrimeSpectrum.Top R)
hpW : ↑(iVU p) ∈ W
iWU : W ⟶ unop (op U)
h : (isFractionPrelocal R).pred fun x => ↑s (iWU x)
a b : R
h' :
  ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), ↑s (iWU x) = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) a ⟨b, hs⟩
hb₁ : b ∉ (↑⟨↑p, hpW⟩).asIdeal
s_eq₁ : ↑s (iWU ⟨↑p, hpW⟩) = IsLocalization.mk' (Localization.AtPrime (↑⟨↑p, hpW⟩).asIdeal) a ⟨b, hb₁⟩
⊢ (Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).val.map iVU.op)) s) p

Proof state:
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op V))
⊢ ↑((comap (RingHom.id R) U V ⋯) s) p = ↑((CommRingCat.Hom.hom ((structureSheaf R).val.map iVU.op)) s) p

Tactic:
rw [comap_apply]

Result:
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op V))
⊢ (Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).val.map iVU.op)) s) p

Proof state:
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op V))
W : Opens ↑(PrimeSpectrum.Top R)
hpW : ↑(iVU p) ∈ W
iWU : W ⟶ unop (op U)
h : (isFractionPrelocal R).pred fun x => ↑s (iWU x)
a b : R
h' :
  ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), ↑s (iWU x) = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) a ⟨b, hs⟩
hb₁ : b ∉ (↑⟨↑p, hpW⟩).asIdeal
s_eq₁ : ↑s (iWU ⟨↑p, hpW⟩) = IsLocalization.mk' (Localization.AtPrime (↑⟨↑p, hpW⟩).asIdeal) a ⟨b, hb₁⟩
hb₂ : b ∉ (↑⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, hpW⟩).asIdeal
s_eq₂ :
  ↑s (iWU ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, hpW⟩) =
    IsLocalization.mk' (Localization.AtPrime (↑⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, hpW⟩).asIdeal) a ⟨b, hb₂⟩
⊢ (Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).val.map iVU.op)) s) p

Tactic:
dsimp only at s_eq₁ s_eq₂

Result:
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op V))
W : Opens ↑(PrimeSpectrum.Top R)
hpW : ↑(iVU p) ∈ W
iWU : W ⟶ unop (op U)
h : (isFractionPrelocal R).pred fun x => ↑s (iWU x)
a b : R
h' :
  ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), ↑s (iWU x) = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) a ⟨b, hs⟩
hb₁ : b ∉ (↑⟨↑p, hpW⟩).asIdeal
s_eq₁ : ↑s (iWU ⟨↑p, hpW⟩) = IsLocalization.mk' (Localization.AtPrime (↑p).asIdeal) a ⟨b, hb₁⟩
hb₂ : b ∉ (↑⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, hpW⟩).asIdeal
s_eq₂ :
  ↑s (iWU ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, hpW⟩) =
    IsLocalization.mk' (Localization.AtPrime ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal) a ⟨b, hb₂⟩
⊢ (Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).val.map iVU.op)) s) p

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op V))
W : Opens ↑(PrimeSpectrum.Top R)
hpW : ↑(iVU p) ∈ W
iWU : W ⟶ unop (op U)
h : (isFractionPrelocal R).pred fun x => ↑s (iWU x)
a b : R
h' :
  ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), ↑s (iWU x) = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) a ⟨b, hs⟩
hb₁ : b ∉ (↑⟨↑p, hpW⟩).asIdeal
s_eq₁ : ↑s (iWU ⟨↑p, hpW⟩) = IsLocalization.mk' (Localization.AtPrime (↑⟨↑p, hpW⟩).asIdeal) a ⟨b, hb₁⟩
⊢ (Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).val.map iVU.op)) s) p

Tactic:
obtain ⟨hb₂, s_eq₂⟩ :=
  h' ⟨PrimeSpectrum.comap (RingHom.id _) p.1, hpW⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op V))
W : Opens ↑(PrimeSpectrum.Top R)
hpW : ↑(iVU p) ∈ W
iWU : W ⟶ unop (op U)
h : (isFractionPrelocal R).pred fun x => ↑s (iWU x)
a b : R
h' :
  ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), ↑s (iWU x) = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) a ⟨b, hs⟩
hb₁ : b ∉ (↑⟨↑p, hpW⟩).asIdeal
s_eq₁ : ↑s (iWU ⟨↑p, hpW⟩) = IsLocalization.mk' (Localization.AtPrime (↑⟨↑p, hpW⟩).asIdeal) a ⟨b, hb₁⟩
hb₂ : b ∉ (↑⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, hpW⟩).asIdeal
s_eq₂ :
  ↑s (iWU ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, hpW⟩) =
    IsLocalization.mk' (Localization.AtPrime (↑⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, hpW⟩).asIdeal) a ⟨b, hb₂⟩
⊢ (Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).val.map iVU.op)) s) p