∀ (n : Type v) {X : AlgebraicGeometry.Scheme}
  (f :
    X ⟶
      AlgebraicGeometry.Spec
        { carrier := MvPolynomial n (ULift.{u, 0} ℤ), commRing := MvPolynomial.instCommRingMvPolynomial })
  (i : n),
  (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n) f i =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
      ((CategoryTheory.ConcreteCategory.hom
          (AlgebraicGeometry.Scheme.ΓSpecIso
              { carrier := MvPolynomial n (ULift.{u, 0} ℤ), commRing := MvPolynomial.instCommRingMvPolynomial }).inv)
        (MvPolynomial.X i))