awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (hypothesis)
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
B : CompHausLike P
f g : finiteCoproduct.{w, u} (P := P) X ⟶ B
h : ∀ (a : α), ι (P := P) X a ≫ f = ι (P := P) X a ≫ g
a : α
x : (↑((X a).toTop (P := P)) : Type (max u w))
⊢ Eq (α := (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) f :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) g :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))
have h₁ : ι (P := P) X a ≫ f = ι (P := P) X a ≫ g
Tactic: specialize h a
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (hypothesis)
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
B : CompHausLike P
f g : finiteCoproduct.{w, u} (P := P) X ⟶ B
a : α
x : (↑((X a).toTop (P := P)) : Type (max u w))
h : ι (P := P) X a ≫ f = ι (P := P) X a ≫ g
⊢ Eq (α := (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) f :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) g :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))
have h₁ : Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
          fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (ι (P := P) X a ≫ f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
      x :
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
          fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (ι (P := P) X a ≫ g) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
      x :
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
Tactic: apply_fun (fun q ↦ q x) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (goal)
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
⊢ IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (∐ X))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
          fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := ∐ X) (Sigma.ι X a)) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (∐ X))
have refine : IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)) (Y :=
  (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)))
  (Function.comp (β := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (∐ X))
    (⇑(homeoOfIso (P := P)
          (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
            (finiteCoproduct.isColimit (P := P) X))) :
      (a : (↑(colimit.cocone (Discrete.functor X)).pt.toTop : Type (max u w))) →
        (↑(finiteCoproduct.cofan X).pt.toTop : Type (max u w)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
          fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := ∐ X) (Sigma.ι X a)) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (∐ X)))
Tactic: refine IsOpenEmbedding.of_comp _ (homeoOfIso ((colimit.isColimit _).coconePointUniqueUpToIso
    (finiteCoproduct.isColimit X))).isOpenEmbedding ?_
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (goal)
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
⊢ IsOpenEmbedding (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)) (Y :=
    (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)))
    (Function.comp (β := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (∐ X))
      (⇑(homeoOfIso (P := P)
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
              (finiteCoproduct.isColimit (P := P) X))) :
        (a : (↑(colimit.cocone (Discrete.functor X)).pt.toTop : Type (max u w))) →
          (↑(finiteCoproduct.cofan X).pt.toTop : Type (max u w)))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := ∐ X) (Sigma.ι X a)) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (∐ X)))
have h : (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)) =
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X) →
  Eq (α :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a) →
      (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)))
    (Function.comp (β := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (∐ X))
      (⇑(homeoOfIso (P := P)
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
              (finiteCoproduct.isColimit (P := P) X))) :
        (a : (↑(colimit.cocone (Discrete.functor X)).pt.toTop : Type (max u w))) →
          (↑(finiteCoproduct.cofan X).pt.toTop : Type (max u w)))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := ∐ X) (Sigma.ι X a)) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (∐ X)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
          fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
          (finiteCoproduct.ι (P := P) X a)) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
Tactic: convert! finiteCoproduct.isOpenEmbedding_ι X a
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (goal)
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P_2 : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P_2
P : TopCat.{u_1} → Prop
inst_3 : HasExplicitFiniteCoproducts P
⊢ PreservesFiniteCoproducts (compHausLikeToTop P)
have refine : ∀ (n : ℕ) {F : Discrete (Fin n) ⥤ CompHausLike P}, PreservesColimit F (compHausLikeToTop P)
Tactic: refine ⟨fun n ↦ ⟨fun {F} ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (goal)
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P_2 : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P_2
P : TopCat.{u_1} → Prop
inst_3 : HasExplicitFiniteCoproducts P
n : ℕ
F : Discrete (Fin n) ⥤ CompHausLike P
⊢ PreservesColimit F (compHausLikeToTop P)
have suffices : PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P)
Tactic: suffices PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P) from
    preservesColimit_of_iso_diagram _ Discrete.natIsoFunctor.symm
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (hypothesis)
Goal:
P_1 : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P_1
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P_1) X
P : TopCat.{u} → Prop
inst_2 : HasExplicitFiniteCoproducts P
P' : TopCat.{u} → Prop
h : ∀ (X : CompHausLike P), P (X.toTop (P := P)) → P' (X.toTop (P := P))
⊢ PreservesFiniteCoproducts (toCompHausLike (P := P) (P' := P') h)
have this : PreservesFiniteCoproducts (toCompHausLike (P := P) (P' := P') h ⋙ compHausLikeToTop P')
Tactic: have : PreservesFiniteCoproducts (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesFiniteCoproducts (compHausLikeToTop _))
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (goal)
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a b : Z ⟶ pullback (P := P) f g
hfst : a ≫ fst (P := P) f g = b ≫ fst (P := P) f g
hsnd : a ≫ snd (P := P) f g = b ≫ snd (P := P) f g
⊢ a = b
have h : ∀ (z : (↑(Z.toTop (P := P)) : Type u)),
  Eq (α := (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
    ((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)) a :
          (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
        z :
      (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
    ((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)) b :
          (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
        z :
      (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
Tactic: ext z
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (hypothesis)
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a b : Z ⟶ pullback (P := P) f g
hfst : a ≫ fst (P := P) f g = b ≫ fst (P := P) f g
hsnd : a ≫ snd (P := P) f g = b ≫ snd (P := P) f g
z : (↑(Z.toTop (P := P)) : Type u)
⊢ Eq (α := (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
    ((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)) a :
          (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
        z :
      (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
    ((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)) b :
          (a : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
        z :
      (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
have hfst₁ : Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
  ((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)) (a ≫ fst (P := P) f g) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
      z :
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
  ((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)) (b ≫ fst (P := P) f g) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
      z :
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
Tactic: apply_fun (fun q ↦ q z) at hfst hsnd
Cleared hypotheses: hfst, hsnd
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (hypothesis)
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))
⊢ PreservesLimit (cospan f g) (toCompHausLike (P := P) (P' := P') h)
have this : PreservesLimit (cospan f g) (toCompHausLike (P := P) (P' := P') h ⋙ compHausLikeToTop P')
Tactic: have : PreservesLimit (cospan f g) (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesLimit _ (compHausLikeToTop _))
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (goal)
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
⊢ HasExplicitPullback (P := P) coprod.inl f
have 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))
Tactic: apply hP'
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.SigmaComparison (goal)
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)
⊢ 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))))
have 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))))
Tactic: ext x a
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.SigmaComparison (goal)
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 : α
⊢ 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))))
have 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))))
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]