-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
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)
⊢ 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))))
have 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 := sorry }) :
                  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))))
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]