-- 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)
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 : Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))
this_1 : Preregular.{u, u + 1} (CompHausLike P)
this : PreservesFiniteProducts (Functor.obj (sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))) X) :=
  ⋯
a :
  Fiber (Y := (↑((of P PUnit.{u + 1}).toTop (P := P)) : Type u)) (Z :=
    X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))
    (⇑((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (unit P hs)
                  (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1}))))) →
                (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.obj.obj (op (of P PUnit.{u + 1})))))
            x :
          (fun (X : Type (max u w)) ↦ X)
            ((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.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))))) :
      (a : (↑(of P PUnit.{u + 1}).toTop : Type u)) → X.obj.obj (op (of P PUnit.{u + 1})))
h :
  Eq (α :=
    X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
      (op
        (fiber.{u, w} (P := P)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾fun
                    (x :
                      Functor.obj (𝟭 (Type (max u w)))
                        (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
                          (op (of P PUnit.{u + 1})))) ↦
                  LocallyConstant.const PUnit.{u + 1} x) :
              (a : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) →
                (functor P hs ⋙
                      (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                        (op (of P PUnit.{u + 1}))).obj
                  (X.obj.obj (op (of P PUnit.{u + 1}))))
            x)
          a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).map
              (Quiver.Hom.op
                (IsTerminal.from (isTerminalPUnit (P := P))
                  (fiber.{u, w} (P := P)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun)
                          (↾fun
                              (x :
                                Functor.obj (𝟭 (Type (max u w)))
                                  (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
                                    (op (of P PUnit.{u + 1})))) ↦
                            LocallyConstant.const PUnit.{u + 1} x) :
                        (a : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) →
                          (functor P hs ⋙
                                (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                                  (op (of P PUnit.{u + 1}))).obj
                            (X.obj.obj (op (of P PUnit.{u + 1}))))
                      x)
                    a)))) :
          (a_1 : X.obj.obj (op (of P PUnit.{u + 1}))) →
            X.obj.obj
              (op
                (fiber
                  ((ConcreteCategory.hom
                        (↾fun (x : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) ↦
                          LocallyConstant.const PUnit.{u + 1} x) :
                      (a : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) →
                        (functor P hs ⋙
                              (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                                (op (of P PUnit.{u + 1}))).obj
                          (X.obj.obj (op (of P PUnit.{u + 1}))))
                    x)
                  a)))
        (Fiber.image
          (⇑((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (↾fun
                          (x :
                            Functor.obj (𝟭 (Type (max u w)))
                              (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
                                (op (of P PUnit.{u + 1})))) ↦
                        LocallyConstant.const PUnit.{u + 1} x) :
                    (a : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) →
                      (functor P hs ⋙
                            (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                              (op (of P PUnit.{u + 1}))).obj
                        (X.obj.obj (op (of P PUnit.{u + 1}))))
                  x :
                (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.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))) :
            (a : PUnit.{u + 1}) → X.obj.obj (op (of P PUnit.{u + 1})))
          a) :
      X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
        (op
          (fiber.{u, w} (P := P)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (↾fun
                      (x :
                        Functor.obj (𝟭 (Type (max u w)))
                          (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
                            (op (of P PUnit.{u + 1})))) ↦
                    LocallyConstant.const PUnit.{u + 1} x) :
                (a : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) →
                  (functor P hs ⋙
                        (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                          (op (of P PUnit.{u + 1}))).obj
                    (X.obj.obj (op (of P PUnit.{u + 1}))))
              x)
            a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).map
              (Quiver.Hom.op
                (sigmaIncl (P := P)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (↾fun
                            (x :
                              Functor.obj (𝟭 (Type (max u w)))
                                (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
                                  (op (of P PUnit.{u + 1})))) ↦
                          LocallyConstant.const PUnit.{u + 1} x) :
                      (a : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) →
                        (functor P hs ⋙
                              (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                                (op (of P PUnit.{u + 1}))).obj
                          (X.obj.obj (op (of P PUnit.{u + 1}))))
                    x)
                  a))) :
          (a_1 : X.obj.obj (op (of P PUnit.{u + 1}))) →
            X.obj.obj
              (op
                (fiber
                  ((ConcreteCategory.hom
                        (↾fun (x : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) ↦
                          LocallyConstant.const PUnit.{u + 1} x) :
                      (a : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) →
                        (functor P hs ⋙
                              (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                                (op (of P PUnit.{u + 1}))).obj
                          (X.obj.obj (op (of P PUnit.{u + 1}))))
                    x)
                  a)))
        x :
      X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
        (op
          (fiber.{u, w} (P := P)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (↾fun
                      (x :
                        Functor.obj (𝟭 (Type (max u w)))
                          (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
                            (op (of P PUnit.{u + 1})))) ↦
                    LocallyConstant.const PUnit.{u + 1} x) :
                (a : (𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1})))) →
                  (functor P hs ⋙
                        (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                          (op (of P PUnit.{u + 1}))).obj
                    (X.obj.obj (op (of P PUnit.{u + 1}))))
              x)
            a)))
⊢ Eq (α :=
    (fun (X : Type (max u w)) ↦ X)
      (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
        (op
          (fiber.{u, w} (P := P)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app (unit P hs)
                    (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))) :
                (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1}))))) →
                  (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.obj.obj (op (of P PUnit.{u + 1})))))
              x)
            a))))
    (counitAppAppImage (P := P)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (unit P hs)
              (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))) :
          (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1}))))) →
            (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.obj.obj (op (of P PUnit.{u + 1})))))
        x)
      a)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).map
            (Quiver.Hom.op
              (sigmaIncl (P := P)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (NatTrans.app (unit P hs)
                        (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj
                          (op (of P PUnit.{u + 1})))) :
                    (a :
                        (fun (X : Type (max u w)) ↦ X)
                          ((𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1}))))) →
                      (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.obj.obj (op (of P PUnit.{u + 1})))))
                  x)
                a))) :
        (a_1 : (fun (X : Type (max u w)) ↦ X) (X.obj.obj (op (of P PUnit.{u + 1})))) →
          (fun (X : Type (max u w)) ↦ X)
            (X.obj.obj
              (op
                (fiber
                  ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1})))) :
                      (a :
                          (fun (X : Type (max u w)) ↦ X)
                            ((𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1}))))) →
                        (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.obj.obj (op (of P PUnit.{u + 1})))))
                    x)
                  a))))
      x)

Tactic:
simp only [unit_app, counitAppAppImage]

Premises used: CompHausLike.LocallyConstant.counitAppAppImage, CompHausLike.LocallyConstant.unit_app