-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
⊢ (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
have 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) sorry :
                        { 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)))
Tactic: ext : 2