-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
f : X ⟶ Spec ℤ[n]
a :
  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))) =
    Iso.inv (Scheme.ΓSpecIso ℤ[n]) ≫ Scheme.Hom.appTop f
⊢ 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:
simp only [Scheme.toSpecΓ_appTop, Scheme.ΓSpecIso_naturality, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.toSpecΓ_appTop