-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n₁ n₂ n₃ : Type v
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
h₁ :
  Eq (α := AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₃) S ⟶ S)
    (reindex
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (i ≫ j)) :
          (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₃)
        S ≫
      AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₁) S ↘ S)
    (CategoryStruct.comp (Y := AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₂) S)
        (reindex
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) j) : (a : (fun (X : Type v) ↦ X) n₂) → (fun (X : Type v) ↦ X) n₃)
          S)
        (reindex
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) i) : (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₂)
          S) ≫
      AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₁) S ↘ S)
h₂ :
  ∀ (k : (fun (X : Type v) ↦ X) n₁),
    Eq (α := (↑Γ(𝔸((fun (X : Type v) ↦ X) 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 := Γ(𝔸((fun (X : Type v) ↦ X) n₁; S), ⊤)) (Y :=
              Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤))
              (Scheme.Hom.appTop
                (reindex
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (i ≫ j)) :
                    (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₃)
                  S)) :
            (a : (↑Γ(𝔸((fun (X : Type v) ↦ X) n₁; S), ⊤) : Type (max u v))) →
              (↑Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤) : Type (max u v)))
          (coord S k) :
        (↑Γ(𝔸((fun (X : Type v) ↦ X) 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 := Γ(𝔸((fun (X : Type v) ↦ X) n₁; S), ⊤)) (Y :=
              Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤))
              (Scheme.Hom.appTop
                (CategoryStruct.comp (Y := AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₂) S)
                  (reindex
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) j) :
                      (a : (fun (X : Type v) ↦ X) n₂) → (fun (X : Type v) ↦ X) n₃)
                    S)
                  (reindex
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) i) :
                      (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₂)
                    S))) :
            (a : (↑Γ(𝔸((fun (X : Type v) ↦ X) n₁; S), ⊤) : Type (max u v))) →
              (↑Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤) : Type (max u v)))
          (coord S k) :
        (↑Γ(𝔸((fun (X : Type v) ↦ X) n₃; S), ⊤) : Type (max u v)))
⊢ Eq (α := AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₃) S ⟶ AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₁) S)
    (reindex
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (i ≫ j)) :
        (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₃)
      S)
    (CategoryStruct.comp (Y := AffineSpace.{v, u} ((fun (X : Type v) ↦ X) n₂) S)
      (reindex
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) j) : (a : (fun (X : Type v) ↦ X) n₂) → (fun (X : Type v) ↦ X) n₃) S)
      (reindex
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) i) : (a : (fun (X : Type v) ↦ X) n₁) → (fun (X : Type v) ↦ X) n₂)
        S))

Tactic:
ext k