-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }
a :
  (↑((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
              (Subtype.mk (p := fun (f : X ⟶ AffineSpace.{v, u} n S) ↦ Scheme.Hom.IsOver f S) (homOfVector (X ↘ S) v)
                  ⋯ :
                { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
            ((fun (f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }) (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 : X ⟶ 𝔸(n; S))) :
                      (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
                    (coord S i) :
                  (↑Γ(X, ⊤) : Type (max u v))))
              f)) :
        X ⟶ 𝔸(n; S)) ≫
      AffineSpace.{v, u} n S ↘ S =
    (↑f : X ⟶ 𝔸(n; S)) ≫ AffineSpace.{v, u} n S ↘ S
a₁ :
  ∀ (i : n),
    Eq (α := (↑Γ(X, ⊤) : 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 := Γ(𝔸(n; S), ⊤)) (Y := Γ(X, ⊤))
              (Scheme.Hom.appTop
                (↑((fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
                        (Subtype.mk (p := fun (f : X ⟶ AffineSpace.{v, u} n S) ↦ Scheme.Hom.IsOver f S)
                            (homOfVector (X ↘ S) v) ⋯ :
                          { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
                      ((fun (f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }) (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 : X ⟶ 𝔸(n; S))) :
                                (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
                              (coord S i) :
                            (↑Γ(X, ⊤) : Type (max u v))))
                        f)) :
                  X ⟶ 𝔸(n; S))) :
            (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(X, ⊤) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop (↑f : X ⟶ 𝔸(n; S))) :
            (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
          (coord S i) :
        (↑Γ(X, ⊤) : Type (max u v)))
⊢ (fun (v : n → (↑Γ(X, ⊤) : Type (max u v))) ↦
        (Subtype.mk (p := fun (f : X ⟶ AffineSpace.{v, u} n S) ↦ Scheme.Hom.IsOver f S) (homOfVector (X ↘ S) v) ⋯ :
          { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }))
      ((fun (f : { f : X ⟶ AffineSpace.{v, u} n S // Scheme.Hom.IsOver f S }) (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 : X ⟶ 𝔸(n; S))) :
                (a : (↑Γ(𝔸(n; S), ⊤) : Type (max u v))) → (↑Γ(X, ⊤) : Type (max u v)))
              (coord S i) :
            (↑Γ(X, ⊤) : Type (max u v))))
        f) =
    f

Tactic:
ext : 2