-- 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)
x : X.obj (op Q)
h :
  Eq (α := X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (CategoryStruct.comp (Y :=
                  op
                    (of P
                      ((a : Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) ×
                        (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
                  (Quiver.Hom.op (Iso.hom (sigmaIso (P := P) r)) :
                    op Q ⟶ op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) r)))
                  (Quiver.Hom.op
                      (ofHom P
                        {
                          toFun :=
                            Sigma.mk (β :=
                              fun
                                (a :
                                  Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z)
                                    (⇑r : (a : (↑Q.toTop : Type u)) → Z)) ↦
                              (↑(↑a : Set (↑Q.toTop : Type u)) : Type u)) a,
                          continuous_toFun := ⋯ }) :
                    op
                        (of P
                          ((a :
                            Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) ×
                            (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))) ⟶
                      op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))) :
            TypeCat.Fun (X.obj (op Q)) (X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))) :
          (a_1 : X.obj (op Q)) → X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
        x :
      X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (sigmaIncl (P := P) r a))) :
            TypeCat.Fun (X.obj (op Q)) (X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))) :
          (a_1 : X.obj (op Q)) → X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
        x :
      X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
⊢ 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))))

Tactic:
simp only [Functor.mapIso_hom, Iso.op_hom, sigmaComparison, TypeCat.Fun.toFun_apply,
    CategoryTheory.comp_apply, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
    ← X.map_comp_apply]

Premises used: CategoryTheory.Iso.op_hom, CompHausLike.sigmaComparison, TypeCat.Fun.coe_mk, CategoryTheory.Functor.map_comp_apply, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply, CategoryTheory.Functor.mapIso_hom, CategoryTheory.ConcreteCategory.hom_ofHom