-- 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)
Q : CompHausLike P
Z : Type (max u w)
r : LocallyConstant (↑(Q.toTop (P := P)) : Type u) Z
a : Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)
inst_1 : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
h :
  ∀ (x : X.obj (op Q)),
    Eq (α := X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))))
      (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) r))))
              (Iso.hom (X.mapIso (Iso.op (sigmaIso (P := P) r))) :
                X.obj (op Q) ⟶ X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) r))))
              (CategoryStruct.comp (Y :=
                  (a : Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) →
                    X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))))
                  (sigmaComparison.{u, w} (P := P) X
                    fun
                      (a : Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) ↦
                    (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))
                  (↾fun
                      (g :
                        (a :
                            Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) →
                          X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u)))) ↦
                    g a) :
                X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) r))) ⟶
                  X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))))))
          x :
        X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))))
      (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (sigmaIncl (P := P) r a)))) x :
        X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))))
⊢ Eq (α := X.obj (op Q) ⟶ X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))))
    (CategoryStruct.comp (Y := X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) r))))
        (Iso.hom (X.mapIso (Iso.op (sigmaIso (P := P) r))) :
          X.obj (op Q) ⟶ X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) r))))
        (CategoryStruct.comp (Y :=
            (a : Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) →
              X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))))
            (sigmaComparison.{u, w} (P := P) X
              fun (a : Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) ↦
              (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))
            (↾fun
                (g :
                  (a : Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) →
                    X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u)))) ↦
              g a) :
          X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) r))) ⟶
            X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u)))) :
      X.obj (op Q) ⟶ X.obj (op (of P (↑((fiber.{u, w} (P := P) r a).toTop (P := P)) : Type u))))
    (X.map (Quiver.Hom.op (sigmaIncl (P := P) r a)) : X.obj (op Q) ⟶ X.obj (op (fiber.{u, w} (P := P) r a)))

Tactic:
ext