-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (hypothesis)
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 x
have hx₁ : IsUnit (M := AtPrime ℬ p.asHomogeneousIdeal.toIdeal)
  ((localRingHom f
          (toIdeal (σ := σ) (𝒜 := 𝒜)
            (asHomogeneousIdeal
              (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                  (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                p)))
          p.asHomogeneousIdeal.toIdeal sorry :
        (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
Cleared hypotheses: hx