-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f : X ⟶ Spec ℤ[n]
⊢ Quiver.Hom.unop
      (Scheme.Γ.rightOp.map
          ((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)) ≫
        ΓSpec.adjunction.counit.app (Opposite.op ℤ[n])) =
    (Scheme.Γ.rightOp.map f ≫ ΓSpec.adjunction.counit.app (Opposite.op ℤ[n])).unop
have a : Iso.inv (Scheme.ΓSpecIso ℤ[n]) ≫
    CategoryStruct.comp (Y := Γ(Spec Γ(X, ⊤), ⊤))
      (Scheme.Hom.app
          (Spec.map
            (CommRingCat.ofHom
              (eval₂Hom
                (RingHom.comp (Int.castRingHom (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v)))
                  (↑ULift.ringEquiv : ULift.{u, 0} ℤ →+* ℤ))
                fun (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])) :
                        (↑ℤ[n] : Type (max v u)) →+* (↑Γ(Spec ℤ[n], ⊤) : Type (max v u))) :
                      (a : MvPolynomial n (ULift.{u, 0} ℤ)) → (↑Γ(Spec ℤ[n], ⊤) : Type (max v u)))
                    (MvPolynomial.X i)))))
          ⊤ :
        Γ(Spec ℤ[n], ⊤) ⟶
          Γ(Spec Γ(X, ⊤),
            Spec.map
                (CommRingCat.ofHom
                  (eval₂Hom
                    (RingHom.comp (Int.castRingHom (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v)))
                      (↑ULift.ringEquiv : ULift.{u, 0} ℤ →+* ℤ))
                    fun (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])) :
                            (↑ℤ[n] : Type (max v u)) →+* (↑Γ(Spec ℤ[n], ⊤) : Type (max v u))) :
                          (a : MvPolynomial n (ULift.{u, 0} ℤ)) → (↑Γ(Spec ℤ[n], ⊤) : Type (max v u)))
                        (MvPolynomial.X i)))) ⁻¹ᵁ
              ⊤))
      (Scheme.Hom.app X.toSpecΓ ⊤) =
  Iso.inv (Scheme.ΓSpecIso ℤ[n]) ≫ Scheme.Hom.appTop f
Tactic: dsimp