∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (x : ↑(X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app hU.fromSpec U)) x =
    (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯)))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv) x)