-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
f : X ⟶ Spec ℤ[n]
i : n
⊢ Eq (α := (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u))) (CC :=
            CommRingCat.carrier) (X := ℤ[n]) (Y := CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v)))
            (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)))) :
          (a : (↑ℤ[n] : Type (max v u))) →
            (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
        (MvPolynomial.X i) :
      (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max v u)) →+* (↑S : Type (max v u))) (CC :=
            CommRingCat.carrier) (Iso.inv (Scheme.ΓSpecIso ℤ[n]) ≫ Scheme.Hom.appTop f) :
          (a : (↑ℤ[n] : Type (max v u))) →
            (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
        (MvPolynomial.X i) :
      (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
have a : Eq (α := (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
  ((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)) :
    (↑Γ(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) (Iso.inv (Scheme.ΓSpecIso ℤ[n]) ≫ Scheme.Hom.appTop f) :
        (a : (↑ℤ[n] : Type (max v u))) →
          (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
      (MvPolynomial.X i) :
    (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op ⊤)) : Type (max u v))) : Type (max v u)))
Tactic: rw [ConcreteCategory.hom_ofHom, coe_eval₂Hom, eval₂_X]