-- 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)
inst_1 : HasProp P PUnit.{u + 1}
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)
S : CompHausLike P
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) X
this : Preregular.{u, u + 1} (CompHausLike P)
a :
  Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z :=
    (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)))).obj
      (op (of P PUnit.{u + 1})))
    (⇑(map
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
            (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
              (fun (X : Type (max u w)) ↦ X)
                ((functor P hs ⋙
                      (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                        (op (of P PUnit.{u + 1}))).obj
                  X))
          f) :
      (a : (↑S.toTop : Type u)) → ((functor P hs).obj X).obj.obj (op (of P PUnit.{u + 1})))
⊢ Eq (α :=
    (fun (X : 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)))).obj
        (op
          (fiber.{u, w} (P := P)
            (map
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
                (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                  (fun (X : Type (max u w)) ↦ X)
                    ((functor P hs ⋙
                          (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                            (op (of P PUnit.{u + 1}))).obj
                      X))
              f)
            a))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((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)))).map
              (Quiver.Hom.op
                (sigmaIncl (P := P)
                  (map
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
                      (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                        (fun (X : Type (max u w)) ↦ X)
                          ((functor P hs ⋙
                                (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                                  (op (of P PUnit.{u + 1}))).obj
                            X))
                    f)
                  a))) :
          (a_1 : (fun (X : Type (max u w)) ↦ X) (((functor P hs).obj X).obj.obj (op S))) →
            (fun (X : Type (max u w)) ↦ X)
              (((functor P hs).obj X).obj.obj
                (op
                  (fiber
                    (map
                      (⇑(ConcreteCategory.hom ((unit P hs).app X)) :
                        (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                          (fun (X : Type (max u w)) ↦ X)
                            ((functor P hs ⋙
                                  (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                                    (op (of P PUnit.{u + 1}))).obj
                              X))
                      f)
                    a))))
        (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (NatTrans.app
                  (InducedCategory.Hom.hom
                    (ObjectProperty.homMk (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                      (counitApp (P := P)
                        (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)))))))
                  (op S)) :
              TypeCat.Fun (LocallyConstant (↑(S.toTop (P := P)) : Type u) (LocallyConstant PUnit.{u + 1} X))
                (LocallyConstant (↑(S.toTop (P := P)) : Type u) X)) :
            (a : LocallyConstant (↑S.toTop : Type u) (LocallyConstant PUnit.{u + 1} X)) →
              LocallyConstant (↑S.toTop : Type u) X)
          (map (fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x) f)) :
      (fun (X : 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)))).obj
          (op
            (fiber.{u, w} (P := P)
              (map
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
                  (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                    (fun (X : Type (max u w)) ↦ X)
                      ((functor P hs ⋙
                            (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                              (op (of P PUnit.{u + 1}))).obj
                        X))
                f)
              a))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((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)))).map
              (Quiver.Hom.op
                (sigmaIncl (P := P)
                  (map
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
                      (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                        (fun (X : Type (max u w)) ↦ X)
                          ((functor P hs ⋙
                                (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                                  (op (of P PUnit.{u + 1}))).obj
                            X))
                    f)
                  a))) :
          (a_1 : (fun (X : Type (max u w)) ↦ X) (((functor P hs).obj X).obj.obj (op S))) →
            (fun (X : Type (max u w)) ↦ X)
              (((functor P hs).obj X).obj.obj
                (op
                  (fiber
                    (map
                      (⇑(ConcreteCategory.hom ((unit P hs).app X)) :
                        (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                          (fun (X : Type (max u w)) ↦ X)
                            ((functor P hs ⋙
                                  (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                                    (op (of P PUnit.{u + 1}))).obj
                              X))
                      f)
                    a))))
        f :
      (fun (X : 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)))).obj
          (op
            (fiber.{u, w} (P := P)
              (map
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
                  (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                    (fun (X : Type (max u w)) ↦ X)
                      ((functor P hs ⋙
                            (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                              (op (of P PUnit.{u + 1}))).obj
                        X))
                f)
              a))))
have w : Eq (α :=
  (fun (X : 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)))).obj
      (op
        (fiber.{u, w} (P := P)
          (map
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
              (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                (fun (X : Type (max u w)) ↦ X)
                  ((functor P hs ⋙
                        (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                          (op (of P PUnit.{u + 1}))).obj
                    X))
            f)
          a))))
  (counitAppAppImage (P := P)
    (map
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
        (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
          (fun (X : Type (max u w)) ↦ X)
            ((functor P hs ⋙
                  (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                    (op (of P PUnit.{u + 1}))).obj
              X))
      f)
    a)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
        ((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)))).map
          (Quiver.Hom.op
            (sigmaIncl (P := P)
              (map
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
                  (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                    (fun (X : Type (max u w)) ↦ X)
                      ((functor P hs ⋙
                            (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                              (op (of P PUnit.{u + 1}))).obj
                        X))
                f)
              a))) :
      (a_1 : (fun (X : Type (max u w)) ↦ X) (((functor P hs).obj X).obj.obj (op S))) →
        (fun (X : Type (max u w)) ↦ X)
          (((functor P hs).obj X).obj.obj
            (op
              (fiber
                (map
                  (⇑(ConcreteCategory.hom ((unit P hs).app X)) :
                    (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
                      (fun (X : Type (max u w)) ↦ X)
                        ((functor P hs ⋙
                              (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                                (op (of P PUnit.{u + 1}))).obj
                          X))
                  f)
                a))))
    f)
Tactic: erw [incl_of_counitAppApp]