-- Module: Mathlib.Condensed.Discrete.LocallyConstant
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
w :
  ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              (InducedCategory.Hom.hom
                (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)))
              (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) =
    f
⊢ Eq (α :=
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
          (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)))).obj
      (op S))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CategoryStruct.comp (Y :=
            Functor.obj (functorToPresheaves.{u, w} (P := P))
              ((Functor.comp (D := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                    (functor.{u, w} P hs :
                      Type (max u w) ⥤ 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))).obj
                X))
            (CategoryTheory.Functor.map (functorToPresheaves.{u, w} (P := P)) (NatTrans.app (unit P hs) X))
            (InducedCategory.Hom.hom
              (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))))
          (op S)))
      f)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app (𝟙 (Functor.obj (functorToPresheaves.{u, w} (P := P)) X)) (op S)))
      f)

Tactic:
simp only [Functor.id_obj, functor_obj_obj_obj, functorToPresheaves_obj_obj, Functor.comp_obj,
    Functor.flip_obj_obj, ObjectProperty.ι_obj, unit_app, NatTrans.comp_app,
    functorToPresheaves_map_app, ConcreteCategory.hom_ofHom, TypeCat.Fun.toFun_apply,
    CategoryTheory.comp_apply, TypeCat.Fun.coe_mk, NatTrans.id_app, id_apply]

Premises used: CategoryTheory.Functor.comp_obj, TypeCat.Fun.coe_mk, CategoryTheory.ObjectProperty.ι_obj, CompHausLike.LocallyConstant.functorToPresheaves_map_app, TypeCat.Fun.toFun_apply, CategoryTheory.id_apply, CategoryTheory.comp_apply, CategoryTheory.Functor.flip_obj_obj, CategoryTheory.Functor.id_obj, CategoryTheory.NatTrans.id_app, CompHausLike.LocallyConstant.unit_app, CategoryTheory.NatTrans.comp_app, CompHausLike.LocallyConstant.functor_obj_obj_obj, CategoryTheory.ConcreteCategory.hom_ofHom, CompHausLike.LocallyConstant.functorToPresheaves_obj_obj