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