-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X_1 : TopCat
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
X : Type (max u w)
⊢ Eq (α :=
    Quiver.Hom (V := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
      (Functor.obj
          (functor.{u, w} P hs :
            Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
          X :
        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
      (Functor.obj
          (functor.{u, w} P hs :
            Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
          X :
        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
    (CategoryStruct.comp (Y :=
        Functor.obj
          (functor.{u, w} P hs :
            Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
          (Functor.obj (C := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w)))
                (op (of P PUnit.{u + 1})) :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)) ⥤ Type (max u w))
            (Functor.obj
                (functor.{u, w} P hs :
                  Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                X :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))))
        (CategoryTheory.Functor.map (functor.{u, w} P hs) (NatTrans.app (unit P hs) X) :
          Quiver.Hom (V := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj
                (functor.{u, w} P hs :
                  Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                X :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj
                (functor.{u, w} P hs :
                  Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                (Functor.obj (C := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                  (Functor.obj (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w)))
                      (op (of P PUnit.{u + 1})) :
                    Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)) ⥤ Type (max u w))
                  (Functor.obj
                      (functor.{u, w} P hs :
                        Type (max u w) ⥤
                          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                      X :
                    Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))) :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
        (NatTrans.app (counit P hs)
            (Functor.obj
              (functor.{u, w} P hs :
                Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
              X) :
          Quiver.Hom (V := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj (C := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                (Functor.obj (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w)))
                      (op (of P PUnit.{u + 1})) ⋙
                    functor.{u, w} P hs :
                  Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)) ⥤
                    Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                (Functor.obj
                    (functor.{u, w} P hs :
                      Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                    X :
                  Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))) :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj (𝟭 (Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
                (Functor.obj
                  (functor.{u, w} P hs :
                    Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                  X) :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))) :
      Quiver.Hom (V := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
        (Functor.obj
            (functor.{u, w} P hs :
              Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            X :
          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
        (Functor.obj
            (functor.{u, w} P hs :
              Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            X :
          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
    (𝟙
        (Functor.obj
          (functor.{u, w} P hs :
            Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
          X) :
      Quiver.Hom (V := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
        (Functor.obj
            (functor.{u, w} P hs :
              Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            X :
          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
        (Functor.obj
            (functor.{u, w} P hs :
              Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            X :
          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
have h : Eq (α :=
  ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
      (Functor.obj
          (functor.{u, w} P hs :
            Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
          X :
        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))) ⟶
    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
      (Functor.obj
          (functor.{u, w} P hs :
            Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
          X :
        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
  (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj
          (functor.{u, w} P hs :
            Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
          (Functor.obj (C := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w)))
                (op (of P PUnit.{u + 1})) :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)) ⥤ Type (max u w))
            (Functor.obj
                (functor.{u, w} P hs :
                  Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                X :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))))
        (CategoryTheory.Functor.map (functor.{u, w} P hs) (NatTrans.app (unit P hs) X) :
          Quiver.Hom (V := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj
                (functor.{u, w} P hs :
                  Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                X :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj
                (functor.{u, w} P hs :
                  Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                (Functor.obj (C := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                  (Functor.obj (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w)))
                      (op (of P PUnit.{u + 1})) :
                    Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)) ⥤ Type (max u w))
                  (Functor.obj
                      (functor.{u, w} P hs :
                        Type (max u w) ⥤
                          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                      X :
                    Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))) :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
        (NatTrans.app (counit P hs)
            (Functor.obj
              (functor.{u, w} P hs :
                Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
              X) :
          Quiver.Hom (V := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj (C := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                (Functor.obj (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w)))
                      (op (of P PUnit.{u + 1})) ⋙
                    functor.{u, w} P hs :
                  Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)) ⥤
                    Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                (Functor.obj
                    (functor.{u, w} P hs :
                      Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                    X :
                  Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))) :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            (Functor.obj (𝟭 (Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
                (Functor.obj
                  (functor.{u, w} P hs :
                    Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                  X) :
              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))) :
    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
        (Functor.obj
            (functor.{u, w} P hs :
              Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            X :
          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))) ⟶
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
        (Functor.obj
            (functor.{u, w} P hs :
              Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            X :
          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
  (InducedCategory.Hom.hom
      (𝟙
        (Functor.obj
          (functor.{u, w} P hs :
            Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
          X)) :
    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
        (Functor.obj
            (functor.{u, w} P hs :
              Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            X :
          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))) ⟶
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
        (Functor.obj
            (functor.{u, w} P hs :
              Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
            X :
          Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
Tactic: ext : 1