-- 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)
⊢ 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)))
have 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))))
Tactic: ext