-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f : X ⟶ Spec ℤ[n]
⊢ Eq (α := Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (Opposite.op ℤ[n])) :
          (a : X ⟶ Scheme.Spec.obj (Opposite.op ℤ[n])) → Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
        ((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
            (X.toSpecΓ ≫
                Spec.map
                  (CommRingCat.ofHom
                    (eval₂Hom
                      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                        (algebraMap ℤ (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v)))
                        (RingEquiv.toRingHom ULift.ringEquiv))
                      v)) :
              X ⟶ Spec ℤ[n]))
          ((fun (f : X ⟶ Spec ℤ[n]) (i : n) ↦
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                      (CC := CommRingCat.carrier) (Scheme.Hom.appTop f) :
                    (a : (↑Γ(Spec ℤ[n], ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦
                        (↑R : Type (max v u)) →+* (↑S : Type (max v u))) (CC := CommRingCat.carrier) (X := ℤ[n])
                        (Iso.inv (Scheme.ΓSpecIso ℤ[n])) :
                      (a : (↑ℤ[n] : Type (max v u))) → (↑Γ(Spec ℤ[n], ⊤) : Type (max v u)))
                    (MvPolynomial.X i)) :
                (↑Γ(X, ⊤) : Type (max u v))))
            f)) :
      Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (Opposite.op ℤ[n])) :
          (a : X ⟶ Scheme.Spec.obj (Opposite.op ℤ[n])) → Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
        f :
      Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
have a : Eq (α := Opposite.unop (Opposite.op ℤ[n]) ⟶ Opposite.unop (Scheme.Γ.rightOp.obj X))
  (Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (Opposite.op ℤ[n])) :
        (a : X ⟶ Scheme.Spec.obj (Opposite.op ℤ[n])) → Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
      ((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
          (X.toSpecΓ ≫
              Spec.map
                (CommRingCat.ofHom
                  (eval₂Hom
                    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                      (algebraMap ℤ (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v)))
                      (RingEquiv.toRingHom ULift.ringEquiv))
                    v)) :
            X ⟶ Spec ℤ[n]))
        ((fun (f : X ⟶ Spec ℤ[n]) (i : n) ↦
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                    (CC := CommRingCat.carrier) (Scheme.Hom.appTop f) :
                  (a : (↑Γ(Spec ℤ[n], ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u)))
                      (CC := CommRingCat.carrier) (X := ℤ[n]) (Iso.inv (Scheme.ΓSpecIso ℤ[n])) :
                    (a : (↑ℤ[n] : Type (max v u))) → (↑Γ(Spec ℤ[n], ⊤) : Type (max v u)))
                  (MvPolynomial.X i)) :
              (↑Γ(X, ⊤) : Type (max u v))))
          f))))
  (Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (Opposite.op ℤ[n])) :
        (a : X ⟶ Scheme.Spec.obj (Opposite.op ℤ[n])) → Scheme.Γ.rightOp.obj X ⟶ Opposite.op ℤ[n])
      f))
Tactic: apply Quiver.Hom.unop_inj