-- 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)
this :
  IsLocalHom (R := (↑(CommRingCat.of (AtPrime ℬ p.asHomogeneousIdeal.toIdeal)) : Type u)) (S :=
    (↑((Proj ℬ).presheaf.stalk p) : Type u)) (CommRingCat.Hom.hom (stalkIso ℬ p).inv)
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 ⋯ :
          (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)
⊢ IsUnit x
have hx₁ : IsUnit (M :=
  AtPrime 𝒜
    (toIdeal (σ := σ) (𝒜 := 𝒜)
      (asHomogeneousIdeal
        (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
            (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
          p))))
  ((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 𝒜
      (toIdeal (σ := σ) (𝒜 := 𝒜)
        (asHomogeneousIdeal
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p))))
Tactic: replace hx := IsLocalHom.map_nonunit _ hx
Cleared hypotheses: hx