-- Module: Mathlib.Topology.Category.CompHausLike.SigmaComparison
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : PreservesFiniteProducts X
α : Type u
inst_2 : Finite α
σ : α → Type u
inst_3 : (a : α) → TopologicalSpace (σ a)
inst_4 : ∀ (a : α), CompactSpace.{u} (σ a)
inst_5 : ∀ (a : α), T2Space.{u} (σ a)
inst_6 : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
h :
  Eq (α := X.obj (Opposite.op (of P (σ a))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (sigmaComparison.{u, w} (P := P) X σ) :
            TypeCat.Fun (X.obj (Opposite.op (of P ((a : α) × σ a)))) ((a : α) → X.obj (Opposite.op (of P (σ a))))) :
          (a : X.obj (Opposite.op (of P ((a : α) × σ a)))) → (a : α) → X.obj (Opposite.op (of P (σ a))))
        x a :
      X.obj (Opposite.op (of P (σ a))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (a : α) ↦ X.obj (Opposite.op (of P (σ a)))) a) :
          (a_1 : ∏ᶜ fun (a : α) ↦ X.obj (Opposite.op (of P (σ a)))) → X.obj (Opposite.op (of P (σ a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (piComparison X fun (a : α) ↦ Opposite.op (of P (σ a))) :
            (a : X.obj (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x)))) → ∏ᶜ fun (j : α) ↦ X.obj (Opposite.op (of P (σ j))))
          (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (X.map
                    (Iso.hom
                      (opCoproductIsoProduct' (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
                        (productIsProduct fun (x : α) ↦ Opposite.op (of P (σ x)))))) :
                TypeCat.Fun (X.obj (Opposite.op (of P ((a : α) × σ a))))
                  (X.obj (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x))))) :
              (a : X.obj (Opposite.op (of P ((a : α) × σ a)))) → X.obj (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x))))
            x)) :
      X.obj (Opposite.op (of P (σ a))))
⊢ Eq (α := X.obj (Opposite.op (of P (σ a))))
    (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (sigmaComparison.{u, w} (P := P) X σ)) x a :
      X.obj (Opposite.op (of P (σ a))))
    (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (CategoryStruct.comp (Y :=
            X.obj
              (Cone.pt (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ Opposite.op (of P (σ x)))
                (Fan.mk (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x))) (Pi.π fun (x : α) ↦ Opposite.op (of P (σ x))))))
            (Iso.hom
              (X.mapIso
                (opCoproductIsoProduct' (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
                  (productIsProduct fun (x : α) ↦ Opposite.op (of P (σ x))))))
            (Iso.hom (PreservesProduct.iso X fun (a : α) ↦ Opposite.op (of P (σ a))) ≫
              Iso.hom (Types.productIso fun (a : α) ↦ X.obj (Opposite.op (of P (σ a)))))))
        x a :
      X.obj (Opposite.op (of P (σ a))))

Tactic:
simp only [TypeCat.Fun.toFun_apply, Cofan.mk_pt, Fan.mk_pt, Functor.mapIso_hom,
    PreservesProduct.iso_hom, comp_apply, Types.productIso_hom_comp_eval_apply]

Premises used: CategoryTheory.Limits.PreservesProduct.iso_hom, TypeCat.Fun.toFun_apply, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.comp_apply, CategoryTheory.Functor.mapIso_hom