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

Tactic:
rfl

Result:
no goals

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 (((gluedCover 𝒰).ι i).base ≫ (fromGlued 𝒰).base)) x =
    (ConcreteCategory.hom (((gluedCover 𝒰).ι j).base ≫ (fromGlued 𝒰).base)) y
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y

Tactic:
simp_rw [← Scheme.comp_base] at h

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 ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰).base) x =
    (ConcreteCategory.hom ((gluedCover 𝒰).ι j ≫ fromGlued 𝒰).base) y
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y

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 (fromGlued 𝒰).base) ((ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x) =
    (ConcreteCategory.hom (fromGlued 𝒰).base) ((ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y)
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply] at h

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 (((gluedCover 𝒰).ι i).base ≫ (fromGlued 𝒰).base)) x =
    (ConcreteCategory.hom (((gluedCover 𝒰).ι j).base ≫ (fromGlued 𝒰).base)) y
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y

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
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y

Tactic:
let e :=
  (TopCat.pullbackConeIsLimit _ _).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit Scheme.forgetToTop (𝒰.map i) (𝒰.map j))

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))
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y : ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
h : (ConcreteCategory.hom (fromGlued 𝒰).base) x = (ConcreteCategory.hom (fromGlued 𝒰).base) y
⊢ x = y

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x

Result:
case intro.intro
X : Scheme
𝒰 : X.OpenCover
y : ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
i : (gluedCover 𝒰).J
x : ↑↑((gluedCover 𝒰).U i).toPresheafedSpace
h :
  (ConcreteCategory.hom (fromGlued 𝒰).base) ((ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x) =
    (ConcreteCategory.hom (fromGlued 𝒰).base) y
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = y

Proof state:
X : Scheme
𝒰 : X.OpenCover
⊢ Function.Injective ⇑(ConcreteCategory.hom (fromGlued 𝒰).base)

Tactic:
intro x y h

Result:
X : Scheme
𝒰 : X.OpenCover
x y : ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
h : (ConcreteCategory.hom (fromGlued 𝒰).base) x = (ConcreteCategory.hom (fromGlued 𝒰).base) y
⊢ x = y

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 ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰).base) x =
    (ConcreteCategory.hom ((gluedCover 𝒰).ι j ≫ fromGlued 𝒰).base) y
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y

Tactic:
rw [ι_fromGlued, ι_fromGlued] at h

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
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y

Proof state:
case intro.intro
X : Scheme
𝒰 : X.OpenCover
y : ↑↑(gluedCover 𝒰).glued.toPresheafedSpace
i : (gluedCover 𝒰).J
x : ↑↑((gluedCover 𝒰).U i).toPresheafedSpace
h :
  (ConcreteCategory.hom (fromGlued 𝒰).base) ((ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x) =
    (ConcreteCategory.hom (fromGlued 𝒰).base) y
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = y

Tactic:
obtain ⟨j, y, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective y

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 (fromGlued 𝒰).base) ((ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x) =
    (ConcreteCategory.hom (fromGlued 𝒰).base) ((ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y)
⊢ (ConcreteCategory.hom ((gluedCover 𝒰).ι i).base) x = (ConcreteCategory.hom ((gluedCover 𝒰).ι j).base) y