-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
inst :
  IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  f.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom' (f.stalkMap x))
inst₁ :
  IsLocalHom (R :=
    (↑(Z.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (F :=
    (↑(Z.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  f.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u))
    (CommRingCat.Hom.hom'
      (g.stalkMap
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x)))
⊢ IsLocalHom (R :=
    (↑(Z.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Z.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom
      (g.stalkMap
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x) ≫
        f.stalkMap x))

Tactic:
apply +allowSynthFailures RingHom.isLocalHom_comp

Premises used: RingHom.isLocalHom_comp