-- 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 : α
this :
  ∀ (x : ToType (FC := TypeCat.Fun) (X.obj (∏ᶜ fun (a : α) ↦ Opposite.op (of P (σ a))))),
    Eq (α := X.obj (Opposite.op (of P (σ a))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (b : α) ↦ X.obj (Opposite.op (of P (σ b)))) a) :
            (a_1 : ∏ᶜ fun (b : α) ↦ X.obj (Opposite.op (of P (σ b)))) → 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 (a : α) ↦ Opposite.op (of P (σ a)))) →
                ∏ᶜ fun (b : α) ↦ X.obj (Opposite.op (of P (σ b))))
            x) :
        X.obj (Opposite.op (of P (σ a))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Pi.π (fun (a : α) ↦ Opposite.op (of P (σ a))) a)) :
            (a_1 : X.obj (∏ᶜ fun (a : α) ↦ Opposite.op (of P (σ a)))) → X.obj (Opposite.op (of P (σ a))))
          x :
        X.obj (Opposite.op (of P (σ a))))
h :
  Eq (α := X.obj (Opposite.op (of P (σ a))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := ⋯ : C(σ a, Sigma σ) }))) :
          (a_1 : X.obj (Opposite.op (of P (Sigma σ)))) → X.obj (Opposite.op (of P (σ a))))
        x :
      X.obj (Opposite.op (of P (σ a))))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (X.map
                (CategoryStruct.comp (Y := ∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x)))
                  (Iso.hom
                    (opCoproductIsoProduct' (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
                      (productIsProduct fun (x : α) ↦ Opposite.op (of P (σ x)))))
                  (Pi.π (fun (a : α) ↦ Opposite.op (of P (σ a))) a))) :
            TypeCat.Fun (X.obj (Opposite.op (of P ((a : α) × σ a)))) (X.obj (Opposite.op (of P (σ a))))) :
          (a_1 : X.obj (Opposite.op (of P ((a : α) × σ a)))) → X.obj (Opposite.op (of P (σ a))))
        x :
      X.obj (Opposite.op (of P (σ a))))
⊢ 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 _ types TypeCat.Fun _ _ _ _ _
              (X.map
                (CategoryStruct.comp (Y := ∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x)))
                  (Iso.hom
                    (opCoproductIsoProduct' (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
                      (productIsProduct fun (x : α) ↦ Opposite.op (of P (σ x)))))
                  (Pi.π (fun (a : α) ↦ Opposite.op (of P (σ a))) a))) :
            TypeCat.Fun (X.obj (Opposite.op (of P ((a : α) × σ a)))) (X.obj (Opposite.op (of P (σ a))))) :
          (a_1 : X.obj (Opposite.op (of P ((a : α) × σ a)))) → X.obj (Opposite.op (of P (σ a))))
        x :
      X.obj (Opposite.op (of P (σ a))))

Tactic:
simp only [sigmaComparison, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]

Premises used: CompHausLike.sigmaComparison, TypeCat.Fun.coe_mk, CategoryTheory.ConcreteCategory.hom_ofHom