-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
e :
  Eq (α :=
    CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) ⟶
      Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
    (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S)) ≫
        Scheme.Hom.app
          (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
            (Function.comp (β := MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))
              (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                    (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                    (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
                (a : MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) →
                  (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
              MvPolynomial.X))
          ⊤ :
      CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) ⟶
        Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
    (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))) :
      CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))) ⟶
        Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤))
⊢ Scheme.Hom.appTop
      (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
          (Function.comp (β := (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v)))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))
                  (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))) :
              (a : (↑(CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))) : Type (max u v))) →
                (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v)))), ⊤) : Type (max u v)))
            MvPolynomial.X) ≫
        (AffineSpace.{v, u} n S).toSpecΓ ≫
          Spec.map
            (CommRingCat.ofHom
              (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace.{v, u} n S ↘ S))) (coord S)))) =
    Scheme.Hom.appTop (𝟙 (Spec (CommRingCat.of (MvPolynomial n (↑Γ(S, ⊤) : Type (max u v))))))

Tactic:
simp only [Scheme.Hom.comp_base, TopologicalSpace.Opens.map_comp_obj,
          TopologicalSpace.Opens.map_top, Scheme.Hom.comp_app, Scheme.toSpecΓ_appTop,
          Scheme.ΓSpecIso_naturality, Category.assoc, Scheme.Hom.id_app, ← Iso.eq_inv_comp,
          Category.comp_id]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.id_app, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.toSpecΓ_appTop, TopologicalSpace.Opens.map_comp_obj, TopologicalSpace.Opens.map_top, AlgebraicGeometry.Scheme.Hom.comp_base, CategoryTheory.Iso.eq_inv_comp