-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsAffine S
h₁ :
  (((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)))) ≫
        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 ↘ S =
    𝟙 (AffineSpace.{v, u} n S) ≫ AffineSpace.{v, u} n S ↘ S
h₂ :
  ∀ (i : n),
    Eq (α := (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
      ((@ConcreteCategory.hom _ CommRingCat.instCategory
              (fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) CommRingCat.carrier
              (fun (X Y : CommRingCat) ↦
                (RingHom.instFunLike :
                  FunLike ((↑X : Type (max u v)) →+* (↑Y : Type (max u v))) (↑X : Type (max u v))
                    (↑Y : Type (max u v))))
              _ _ _
              (Scheme.Hom.appTop
                  (((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)))) ≫
                    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)) :
                Γ(𝔸(n; S), ⊤) ⟶ Γ(𝔸(n; S), ⊤)) :
            (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
      ((@ConcreteCategory.hom _ CommRingCat.instCategory
              (fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) CommRingCat.carrier
              (fun (X Y : CommRingCat) ↦
                (RingHom.instFunLike :
                  FunLike ((↑X : Type (max u v)) →+* (↑Y : Type (max u v))) (↑X : Type (max u v))
                    (↑Y : Type (max u v))))
              _ _ _ (Scheme.Hom.appTop (𝟙 (AffineSpace.{v, u} n S))) :
            (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(𝔸(n; S), ⊤) : Type (max u v)))
⊢ ((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)))) ≫
      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)

Tactic:
ext1