-- 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
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})))
w :
  ∀ (x : (↑(↑a : Set (↑S.toTop : Type u)) : Type u)),
    Eq (α := X)
      (((({
                    toFun := fun (g : LocallyConstant PUnit.{u + 1} X) ↦
                      comap
                        (TopCat.Hom.hom
                          (InducedCategory.Hom.hom
                            (IsTerminal.from (isTerminalPUnit (P := P))
                              (fiber.{u, w} (P := P)
                                (map
                                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                                        (↾fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x)) :
                                    (a : X) → LocallyConstant PUnit.{u + 1} X)
                                  f)
                                a))))
                        g } :
                  (a_1 : LocallyConstant PUnit.{u + 1} X) →
                    LocallyConstant (↑(↑a : Set (↑S.toTop : Type u)) : Type u) X)
                (Fiber.image
                  (⇑(map
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                              (↾fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x)) :
                          (a : X) → LocallyConstant PUnit.{u + 1} X)
                        f) :
                    (a : (↑S.toTop : Type u)) → LocallyConstant PUnit.{u + 1} X)
                  a) :
              LocallyConstant (↑(↑a : Set (↑S.toTop : Type u)) : Type u) X) :
            (a : (↑(↑a : Set (↑S.toTop : Type u)) : Type u)) → X)
          x :
        X)
      (((({
                    toFun := fun (g : LocallyConstant (↑(S.toTop (P := P)) : Type u) X) ↦
                      comap
                        (TopCat.Hom.hom
                          (InducedCategory.Hom.hom
                            (sigmaIncl (P := P)
                              (map
                                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                                      (↾fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x)) :
                                  (a : X) → LocallyConstant PUnit.{u + 1} X)
                                f)
                              a)))
                        g } :
                  (a_1 : LocallyConstant (↑S.toTop : Type u) X) →
                    LocallyConstant (↑(↑a : Set (↑S.toTop : Type u)) : Type u) X)
                f :
              LocallyConstant (↑(↑a : Set (↑S.toTop : Type u)) : Type u) X) :
            (a : (↑(↑a : Set (↑S.toTop : Type u)) : Type u)) → X)
          x :
        X)
⊢ Eq (α := LocallyConstant (↑(↑a : Set (↑S.toTop : Type u)) : Type u) X)
    (({
            toFun := fun (g : LocallyConstant PUnit.{u + 1} X) ↦
              comap
                (TopCat.Hom.hom
                  (InducedCategory.Hom.hom
                    (IsTerminal.from (isTerminalPUnit (P := P))
                      (fiber.{u, w} (P := P)
                        (map
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                                (↾fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x)) :
                            (a : X) → LocallyConstant PUnit.{u + 1} X)
                          f)
                        a))))
                g } :
          (a_1 : LocallyConstant PUnit.{u + 1} X) → LocallyConstant (↑(↑a : Set (↑S.toTop : Type u)) : Type u) X)
        (Fiber.image
          (⇑(map
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x)) :
                  (a : X) → LocallyConstant PUnit.{u + 1} X)
                f) :
            (a : (↑S.toTop : Type u)) → LocallyConstant PUnit.{u + 1} X)
          a) :
      LocallyConstant (↑(↑a : Set (↑S.toTop : Type u)) : Type u) X)
    (({
            toFun := fun (g : LocallyConstant (↑(S.toTop (P := P)) : Type u) X) ↦
              comap
                (TopCat.Hom.hom
                  (InducedCategory.Hom.hom
                    (sigmaIncl (P := P)
                      (map
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                              (↾fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x)) :
                          (a : X) → LocallyConstant PUnit.{u + 1} X)
                        f)
                      a)))
                g } :
          (a_1 : LocallyConstant (↑S.toTop : Type u) X) → LocallyConstant (↑(↑a : Set (↑S.toTop : Type u)) : Type u) X)
        f :
      LocallyConstant (↑(↑a : Set (↑S.toTop : Type u)) : Type u) X)

Tactic:
ext x