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

Proof state:
case h.left
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 𝒰).f ⟨i, x⟩.fst ⟨j, y⟩.fst).base) ((ConcreteCategory.hom e.hom) ⟨(x, y), h⟩) =
    ⟨i, x⟩.snd

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

Result:
case h.left
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.left))
      ⟨(x, y), h⟩ =
    ⟨i, x⟩.snd

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
        ((TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).π.app WalkingCospan.right))
      ⟨(x, y), h⟩ =
    ⟨j, y⟩.snd

Tactic:
rfl

Result:
no goals

Proof state:
case h
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 𝒰).f ⟨i, x⟩.fst ⟨j, y⟩.fst).base) ((ConcreteCategory.hom e.hom) ⟨(x, y), h⟩) =
      ⟨i, x⟩.snd ∧
    (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:
constructor

Result:
case h.left
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 𝒰).f ⟨i, x⟩.fst ⟨j, y⟩.fst).base) ((ConcreteCategory.hom e.hom) ⟨(x, y), h⟩) =
    ⟨i, x⟩.snd

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

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))
⊢ (gluedCover 𝒰).Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
use e.hom ⟨⟨x, y⟩, h⟩

Result:
case h
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 𝒰).f ⟨i, x⟩.fst ⟨j, y⟩.fst).base) ((ConcreteCategory.hom e.hom) ⟨(x, y), h⟩) =
      ⟨i, x⟩.snd ∧
    (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