∀ (n : Type u_2) {X : AlgebraicGeometry.Scheme} (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))),
  (fun f i =>
        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
          ((CategoryTheory.ConcreteCategory.hom
              (AlgebraicGeometry.Scheme.ΓSpecIso
                  { carrier := MvPolynomial n (ULift.{u_1, 0} ℤ),
                    commRing := MvPolynomial.instCommRingMvPolynomial }).inv)
            (MvPolynomial.X i)))
      ((fun v =>
          CategoryTheory.CategoryStruct.comp X.toSpecΓ
            (AlgebraicGeometry.Spec.map
              (CommRingCat.ofHom
                (MvPolynomial.eval₂Hom ((algebraMap ℤ ↑(X.presheaf.1 (Opposite.op ⊤))).comp ULift.ringEquiv.toRingHom)
                  v))))
        v) =
    v