-- 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 𝒜
      (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))))
⊢ IsUnit x
have this₁ : IsLocalHom (R :=
  (↑((Proj 𝒜).presheaf.stalk
        (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
            (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
          p)) :
    Type u))
  (S :=
  (↑(CommRingCat.of
        (AtPrime 𝒜
          (toIdeal (σ := σ) (𝒜 := 𝒜)
            (asHomogeneousIdeal
              (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                  (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                p))))) :
    Type u))
  (F :=
  (↑((Proj 𝒜).presheaf.stalk
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p)) :
      Type u) →+*
    (↑(CommRingCat.of
          (AtPrime 𝒜
            (toIdeal (σ := σ) (𝒜 := 𝒜)
              (asHomogeneousIdeal
                (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                    (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                  p))))) :
      Type u))
  (CommRingCat.Hom.hom
    (Iso.hom
      (stalkIso 𝒜
        (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
            (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
          p))))
Tactic: have : IsLocalHom (stalkIso 𝒜 (p.comap f hf)).hom.hom := isLocalHom_of_isIso _