-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
⊢ Eq (α := (↑Γ(Spec (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 := Γ(𝔸(n; Spec S), ⊤)) (Scheme.Hom.app (SpecIso n S).inv ⊤) :
          (a : (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v))) →
            (↑Γ(Spec (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 := Γ(𝔸(n; Spec R), ⊤)) (Scheme.Hom.app (map n (Spec.map φ)) ⊤) :
            (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) → (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v)))
          (coord (Spec R) i)) :
      (↑Γ(Spec (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 := Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤)) (Y :=
              Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤))
              (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤ :
                Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) ⟶
                  Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))),
                    Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ⁻¹ᵁ ⊤)) :
            (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v)) →+*
              (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v))) :
          (a : (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v))) →
            (↑Γ(Spec (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 := Γ(𝔸(n; Spec R), ⊤)) (Scheme.Hom.app (SpecIso n R).inv ⊤) :
            (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) →
              (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v)))
          (coord (Spec R) i)) :
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v)))
have h₂ : Eq (α := (↑Γ(Spec (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 := Γ(𝔸(n; Spec S), ⊤)) (Scheme.Hom.app (SpecIso n S).inv ⊤) :
        (a : (↑Γ(𝔸(n; Spec S), ⊤) : Type (max u v))) →
          (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v)))
      (coord (Spec S) i) :
    (↑Γ(Spec (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 := Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤)) (Y :=
            Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤))
            (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) ⊤ :
              Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) ⟶
                Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))),
                  Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ⁻¹ᵁ ⊤)) :
          (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v)) →+*
            (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v))) :
        (a : (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v))) →
          (↑Γ(Spec (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 := Γ(𝔸(n; Spec R), ⊤)) (Scheme.Hom.app (SpecIso n R).inv ⊤) :
          (a : (↑Γ(𝔸(n; Spec R), ⊤) : Type (max u v))) →
            (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max u v)))
        (coord (Spec R) i)) :
    (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v)))
Tactic: conv_lhs => enter [2]; tactic => exact map_appTop_coord _ _