awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
P' : TopCat.{u} → Prop
h : ∀ (X : CompHausLike P), P (X.toTop (P := P)) → P' (X.toTop (P := P))
this : PreservesLimit (cospan f g) (toCompHausLike (P := P) (P' := P') h ⋙ compHausLikeToTop P')
⊢ PreservesLimit (cospan f g) (toCompHausLike (P := P) (P' := P') h)

Tactic:
preservesLimit_of_reflects_of_preserves (toCompHausLike h) (compHausLikeToTop P')

Premises used: CompHausLike.toCompHausLike, CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves, CompHausLike.compHausLikeToTop
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
P' : TopCat.{u} → Prop
h : ∀ (X : CompHausLike P), P (X.toTop (P := P)) → P' (X.toTop (P := P))
this : PreservesLimit (cospan f g) (toCompHausLike (P := P) (P' := P') h ⋙ compHausLikeToTop P')
⊢ PreservesLimit (cospan f g) (toCompHausLike (P := P) (P' := P') h)

Tactic:
exact preservesLimit_of_reflects_of_preserves (toCompHausLike h) (compHausLikeToTop P')

Premises used: CompHausLike.toCompHausLike, CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves, CompHausLike.compHausLikeToTop
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) →
      HasExplicitPullback (P := P) f g
X : CompHausLike P
_ : ∀ {Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), HasExplicitPullback (P := P) coprod.inl f
⊢ ∀ {Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), HasExplicitPullback (P := P) coprod.inl f

Tactic:
_
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) →
      HasExplicitPullback (P := P) f g
X Y : CompHausLike P
_ : ∀ {Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), HasExplicitPullback (P := P) coprod.inl f
⊢ ∀ {Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), HasExplicitPullback (P := P) coprod.inl f

Tactic:
_
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) →
      HasExplicitPullback (P := P) f g
X Y Z : CompHausLike P
f : Z ⟶ X ⨿ Y
x :
  IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (X ⨿ Y))
    (⇑(@ConcreteCategory.hom _ (category P)
          (fun (x1 x2 : CompHausLike P) ↦ C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u)))
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) _ _ X (X ⨿ Y) coprod.inl) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (X ⨿ Y))
⊢ HasExplicitPullback (P := P) coprod.inl f

Tactic:
apply hP'
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) →
      HasExplicitPullback (P := P) f g
X Y Z : CompHausLike P
f : Z ⟶ X ⨿ Y
⊢ IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (X ⨿ Y))
    (⇑(@ConcreteCategory.hom _ (category P)
          (fun (x1 x2 : CompHausLike P) ↦ C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u)))
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) _ _ X (X ⨿ Y) coprod.inl) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (X ⨿ Y))

Tactic:
Sigma.isOpenEmbedding_ι _ _

Premises used: CompHausLike.Sigma.isOpenEmbedding_ι, CategoryTheory.Limits.pair
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) →
      HasExplicitPullback (P := P) f g
X Y Z : CompHausLike P
f : Z ⟶ X ⨿ Y
⊢ IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (X ⨿ Y))
    (⇑(@ConcreteCategory.hom _ (category P)
          (fun (x1 x2 : CompHausLike P) ↦ C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u)))
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) _ _ X (X ⨿ Y) coprod.inl) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (X ⨿ Y))

Tactic:
exact Sigma.isOpenEmbedding_ι _ _

Premises used: CompHausLike.Sigma.isOpenEmbedding_ι
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
inst_1 : HasExplicitPullbacksOfInclusions P
X Y Z : CompHausLike P
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
inst_1 : HasExplicitPullbacksOfInclusions P
⊢ FinitaryExtensive.{u, u + 1} (CompHausLike P)

Tactic:
finitaryExtensive_of_preserves_and_reflects (compHausLikeToTop P)

Premises used: CategoryTheory.finitaryExtensive_of_preserves_and_reflects, CompHausLike.compHausLikeToTop
-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) →
      HasExplicitPullback (P := P) f g
⊢ FinitaryExtensive.{u, u + 1} (CompHausLike P)

Tactic:
have := hasPullbacksOfInclusions hP'
  finitaryExtensive_of_preserves_and_reflects (compHausLikeToTop P)

Premises used: CompHausLike.hasPullbacksOfInclusions, CategoryTheory.finitaryExtensive_of_preserves_and_reflects, CompHausLike.compHausLikeToTop
-- 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)
⊢ HasProp P ((a : α) × σ a)

Tactic:
HasExplicitFiniteCoproducts.hasProp (fun a ↦ of P (σ a))

Premises used: CompHausLike.HasExplicitFiniteCoproducts.hasProp, CompHausLike.of
-- 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)
h :
  ∀ (x : X.obj (Opposite.op (of P ((a : α) × σ a)))) (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))))
⊢ Eq (α := X.obj (Opposite.op (of P ((a : α) × σ a))) ⟶ (a : α) → X.obj (Opposite.op (of P (σ a))))
    (sigmaComparison.{u, w} (P := P) X σ :
      X.obj (Opposite.op (of P ((a : α) × σ a))) ⟶ (a : α) → X.obj (Opposite.op (of P (σ a))))
    (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.obj
          (Opposite.op
            (Cocone.pt (J := Discrete α) (F := Discrete.functor fun (a : α) ↦ of P (σ a))
              (finiteCoproduct.cofan (P := P) fun (a : α) ↦ of P (σ a)))) ⟶
        (j : α) → X.obj (Opposite.op (of P (σ j))))

Tactic:
ext x a
-- 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 : α
⊢ ∀ (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)
              (CategoryStruct.comp (Y := ∏ᶜ fun (b : α) ↦ X.obj (Opposite.op (of P (σ b))))
                (piComparison X fun (a : α) ↦ Opposite.op (of P (σ a)))
                (Pi.π (fun (b : α) ↦ X.obj (Opposite.op (of P (σ b)))) 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))))
      ((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))))

Tactic:
have := ConcreteCategory.congr_hom (piComparison_comp_π X (fun a ↦ ⟨of P (σ a)⟩) a)
-- 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)
              (CategoryStruct.comp (Y := ∏ᶜ fun (b : α) ↦ X.obj (Opposite.op (of P (σ b))))
                (piComparison X fun (a : α) ↦ Opposite.op (of P (σ a)))
                (Pi.π (fun (b : α) ↦ X.obj (Opposite.op (of P (σ b)))) 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))))
      ((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))))
⊢ ∀ (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))))

Tactic:
simp only [comp_apply] at this

Premises used: CategoryTheory.comp_apply
-- 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 (Sigma σ))) ⟶ X.obj (Opposite.op (of P (σ a))))
    (X.map (Quiver.Hom.op (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := ⋯ })))
    (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)))
⊢ 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))))

Tactic:
apply ConcreteCategory.congr_hom

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- 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 (α := of P (σ a) ⟶ of P (Sigma σ))
    (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := ⋯ } : of P (σ a) ⟶ of P (Sigma σ))
    (CategoryStruct.comp (Y := Opposite.unop (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x))))
        (Quiver.Hom.unop (Pi.π (fun (a : α) ↦ Opposite.op (of P (σ a))) a))
        (Quiver.Hom.unop
          (Iso.hom
            (opCoproductIsoProduct' (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
              (productIsProduct fun (x : α) ↦ Opposite.op (of P (σ x)))))) :
      Opposite.unop (Opposite.op (of P (σ a))) ⟶
        Opposite.unop (Opposite.op (finiteCoproduct (P := P) fun (a : α) ↦ of P (σ a))))
⊢ Eq (α := X.obj (Opposite.op (of P (Sigma σ))) ⟶ X.obj (Opposite.op (of P (σ a))))
    (X.map (Quiver.Hom.op (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := ⋯ })))
    (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)))

Tactic:
congr 2