-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B C σ τ ψ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
p : ↥(Proj ℬ)
x :
  (↑((Proj 𝒜).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(Proj ℬ).toPresheafedSpace : TopCat)) (Y := (↑(Proj 𝒜).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (sheafedSpaceMap f hf))) :
            (a : ↥(Proj ℬ)) → ↥(Proj 𝒜))
          p)) :
    Type u)
hx :
  IsUnit (M := (↑((Proj ℬ).presheaf.stalk p) : Type u))
    ((CommRingCat.Hom.hom (stalkIso ℬ p).inv :
          (a : AtPrime ℬ p.asHomogeneousIdeal.toIdeal) → (↑((Proj ℬ).presheaf.stalk p) : Type u))
        ((localRingHom f
                (toIdeal (σ := σ) (𝒜 := 𝒜)
                  (asHomogeneousIdeal
                    (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                        (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                      p)))
                p.asHomogeneousIdeal.toIdeal ⋯ :
              (a :
                  AtPrime 𝒜
                    ((ProjectiveSpectrum.comap f hf : (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                          p).asHomogeneousIdeal.toIdeal) →
                AtPrime ℬ p.asHomogeneousIdeal.toIdeal)
            ((CommRingCat.Hom.hom
                  (Iso.hom
                    (stalkIso 𝒜
                      (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                          (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                        p))) :
                (a :
                    (↑((Proj 𝒜).presheaf.stalk
                          ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base : (a : ↥(Proj ℬ)) → ↥(Proj 𝒜)) p)) :
                      Type u)) →
                  AtPrime 𝒜
                    ((ProjectiveSpectrum.comap f hf : (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                          p).asHomogeneousIdeal.toIdeal)
              x) :
          AtPrime ℬ p.asHomogeneousIdeal.toIdeal) :
      (↑((Proj ℬ).presheaf.stalk p) : Type u))
this :
  IsLocalHom (R := (↑(CommRingCat.of (AtPrime ℬ p.asHomogeneousIdeal.toIdeal)) : Type u)) (S :=
    (↑((Proj ℬ).presheaf.stalk p) : Type u)) (CommRingCat.Hom.hom (stalkIso ℬ p).inv)
⊢ IsUnit (M := AtPrime ℬ p.asHomogeneousIdeal.toIdeal)
    ((localRingHom f
            (toIdeal (σ := σ) (𝒜 := 𝒜)
              (asHomogeneousIdeal
                (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                    (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                  p)))
            p.asHomogeneousIdeal.toIdeal ⋯ :
          (a :
              AtPrime 𝒜
                ((ProjectiveSpectrum.comap f hf : (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                      p).asHomogeneousIdeal.toIdeal) →
            AtPrime ℬ p.asHomogeneousIdeal.toIdeal)
        ((CommRingCat.Hom.hom
              (Iso.hom
                (stalkIso 𝒜
                  (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                      (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                    p))) :
            (a :
                (↑((Proj 𝒜).presheaf.stalk
                      ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base : (a : ↥(Proj ℬ)) → ↥(Proj 𝒜)) p)) :
                  Type u)) →
              AtPrime 𝒜
                ((ProjectiveSpectrum.comap f hf : (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                      p).asHomogeneousIdeal.toIdeal)
          x) :
      AtPrime ℬ p.asHomogeneousIdeal.toIdeal)

Tactic:
replace hx := (isUnit_map_iff _ _).mp hx