-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem fromGlued_injective : Function.Injective 𝒰.fromGlued.base

Proof state:
case h.right
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↑↑((gluedCover 𝒰).U i).toPresheafedSpace
j : (gluedCover 𝒰).J
y : ↑↑((gluedCover 𝒰).U j).toPresheafedSpace
h : (ConcreteCategory.hom (𝒰.map i).base) x = (ConcreteCategory.hom (𝒰.map j).base) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.map i) (𝒰.map j)))
      (forgetToTop.map (pullback.snd (𝒰.map i) (𝒰.map j))) ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.map i) (𝒰.map j))
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).t ⟨i, x⟩.fst ⟨j, y⟩.fst ≫ (gluedCover 𝒰).f ⟨j, y⟩.fst ⟨i, x⟩.fst).base)
      ((ConcreteCategory.hom e.hom) ⟨(x, y), h⟩) =
    ⟨j, y⟩.snd

Tactic:
erw [← ConcreteCategory.comp_apply e.hom, pullbackSymmetry_hom_comp_fst,
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right]

Result:
case h.right
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↑↑((gluedCover 𝒰).U i).toPresheafedSpace
j : (gluedCover 𝒰).J
y : ↑↑((gluedCover 𝒰).U j).toPresheafedSpace
h : (ConcreteCategory.hom (𝒰.map i).base) x = (ConcreteCategory.hom (𝒰.map j).base) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.map i) (𝒰.map j)))
      (forgetToTop.map (pullback.snd (𝒰.map i) (𝒰.map j))) ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.map i) (𝒰.map j))
⊢ (ConcreteCategory.hom
        ((TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).π.app WalkingCospan.right))
      ⟨(x, y), h⟩ =
    ⟨j, y⟩.snd

Proof state:
case intro.intro.intro.intro
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↑↑((gluedCover 𝒰).U i).toPresheafedSpace
j : (gluedCover 𝒰).J
y : ↑↑((gluedCover 𝒰).U j).toPresheafedSpace
h : (ConcreteCategory.hom (𝒰.map i).base) x = (ConcreteCategory.hom (𝒰.map j).base) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.map i) (𝒰.map j)))
      (forgetToTop.map (pullback.snd (𝒰.map i) (𝒰.map j))) ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.map i) (𝒰.map j))
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y

Tactic:
rw [𝒰.gluedCover.ι_eq_iff]

Result:
case intro.intro.intro.intro
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↑↑((gluedCover 𝒰).U i).toPresheafedSpace
j : (gluedCover 𝒰).J
y : ↑↑((gluedCover 𝒰).U j).toPresheafedSpace
h : (ConcreteCategory.hom (𝒰.map i).base) x = (ConcreteCategory.hom (𝒰.map j).base) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.map i) (𝒰.map j)))
      (forgetToTop.map (pullback.snd (𝒰.map i) (𝒰.map j))) ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.map i) (𝒰.map j))
⊢ (gluedCover 𝒰).Rel ⟨i, x⟩ ⟨j, y⟩