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