-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
R S : CommRingCat
φ : R ⟶ S
i : n
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 v u)) →+* (↑S : Type (max v u))) (CC :=
              CommRingCat.carrier) (X := CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))
              (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))))) :
            (a : (↑(CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))) : Type (max v u))) →
              (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), ⊤) : Type (max v u)))
          (X i)) :
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑S : Type (max u v)))), ⊤) : Type (max u v)))
⊢ 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_rhs => enter [2]; tactic => exact SpecIso_inv_appTop_coord _ _

Premises used: AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord