-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
inst : Algebra (↑R : Type u) (↑S : Type u)
x : (↑R : Type u)
hx : x ∈ p.asIdeal.primeCompl
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h₁ : IsUnit (M :=
  (↑(Functor.obj (C :=
        TopCat.Presheaf CommRingCat (↑(Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
        (TopCat.Presheaf.stalkFunctor CommRingCat p)
        (Functor.obj
          (TopCat.Presheaf.pushforward CommRingCat
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom
                (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))))
          (Spec.sheafedSpaceObj (CommRingCat.of (↑S : Type u))).presheaf)) :
    Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X :=
          Functor.obj (TopCat.Presheaf.stalkFunctor CommRingCat p)
            (Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).presheaf)
          (Y :=
          Functor.obj (C :=
            TopCat.Presheaf CommRingCat
              (↑(Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
            (TopCat.Presheaf.stalkFunctor CommRingCat p)
            (Functor.obj
              (TopCat.Presheaf.pushforward CommRingCat
                (PresheafedSpace.Hom.base
                  (InducedCategory.Hom.hom
                    (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))))
              (Spec.sheafedSpaceObj (CommRingCat.of (↑S : Type u))).presheaf))
          (CategoryTheory.Functor.map (TopCat.Presheaf.stalkFunctor CommRingCat p)
            (PresheafedSpace.Hom.c
              (InducedCategory.Hom.hom
                (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))) :
        (a :
            (↑((TopCat.Presheaf.stalkFunctor CommRingCat p).obj
                  (Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).presheaf) :
              Type u)) →
          (↑((TopCat.Presheaf.stalkFunctor CommRingCat p).obj
                ((TopCat.Presheaf.pushforward CommRingCat
                      (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))).hom.base).obj
                  (Spec.sheafedSpaceObj (CommRingCat.of (↑S : Type u))).presheaf)) :
            Type u))
      (((toStalk (↑R : Type u) p).hom' :
            (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) →
              (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk p) : Type u))
          x :
        (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u)) p) : Type u)) :
    (↑(Functor.obj (C :=
          TopCat.Presheaf CommRingCat
            (↑(Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
          (TopCat.Presheaf.stalkFunctor CommRingCat p)
          (Functor.obj
            (TopCat.Presheaf.pushforward CommRingCat
              (PresheafedSpace.Hom.base
                (InducedCategory.Hom.hom
                  (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))))
            (Spec.sheafedSpaceObj (CommRingCat.of (↑S : Type u))).presheaf)) :
      Type u))
Tactic: change IsUnit ((TopCat.Presheaf.stalkFunctor CommRingCat p).map
      (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap ↑R ↑S))).hom.c _)