awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.SigmaComparison (hypothesis)
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))))
    (((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))))
have 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))))
Tactic: have := ConcreteCategory.congr_hom (piComparison_comp_π X (fun a ↦ ⟨of P (σ a)⟩) 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 : α
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))))
⊢ 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))))
have 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 := sorry })))
  (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: apply ConcreteCategory.congr_hom
-- 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 : α
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))))
⊢ 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)))
have h : Eq (α := of P (σ a) ⟶ of P (Sigma σ))
  (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := sorry } : 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))))
Tactic: congr 2
-- 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 : α
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))))
⊢ 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))))
have h : Eq (α := of P (σ a) ⟶ of P (Sigma σ)) (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := sorry })
  (CategoryStruct.comp (Y := Opposite.unop (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x))))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := Opposite.op (∐ fun (a : α) ↦ of P (σ a)))
        (Iso.inv (opCoproductIsoProduct fun (a : α) ↦ of P (σ a)))
        (Quiver.Hom.op (Sigma.ι (C := CompHausLike P) (fun (a : α) ↦ 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)))))))
Tactic: rw [← opCoproductIsoProduct_inv_comp_ι]
-- 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 : α
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))))
⊢ Eq (α := of P (σ a) ⟶ of P (Sigma σ)) (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := ⋯ })
    (CategoryStruct.comp (Y := Opposite.unop (∏ᶜ fun (x : α) ↦ Opposite.op (of P (σ x))))
      (Quiver.Hom.unop
        (CategoryStruct.comp (Y := Opposite.op (∐ fun (a : α) ↦ of P (σ a)))
          (Iso.inv (opCoproductIsoProduct fun (a : α) ↦ of P (σ a)))
          (Quiver.Hom.op (Sigma.ι (C := CompHausLike P) (fun (a : α) ↦ 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)))))))
have h : Eq (α := of P (σ a) ⟶ of P (Sigma σ)) (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := sorry })
  (CategoryStruct.comp (Y := ∐ fun (a : α) ↦ of P (σ a)) (Sigma.ι (C := CompHausLike P) (fun (a : α) ↦ of P (σ a)) a)
    (Quiver.Hom.unop (Iso.inv (opCoproductIsoProduct fun (a : α) ↦ of P (σ a))) ≫
      Quiver.Hom.unop
        (Iso.hom
          (opCoproductIsoProduct' (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
            (productIsProduct fun (x : α) ↦ Opposite.op (of P (σ x)))))))
Tactic: simp only [Opposite.unop_op, unop_comp, Quiver.Hom.unop_op, Category.assoc]
-- 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 : α
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))))
⊢ Eq (α := of P (σ a) ⟶ of P (Sigma σ)) (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := ⋯ })
    (CategoryStruct.comp (Y := ∐ fun (a : α) ↦ of P (σ a)) (Sigma.ι (C := CompHausLike P) (fun (a : α) ↦ of P (σ a)) a)
      (Quiver.Hom.unop (Iso.inv (opCoproductIsoProduct fun (a : α) ↦ of P (σ a))) ≫
        Quiver.Hom.unop
          (Iso.hom
            (opCoproductIsoProduct' (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
              (productIsProduct fun (x : α) ↦ Opposite.op (of P (σ x)))))))
have h : Eq (α := of P (σ a) ⟶ of P (Sigma σ)) (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := sorry })
  (CategoryStruct.comp (Y := ∐ fun (a : α) ↦ of P (σ a)) (Sigma.ι (C := CompHausLike P) (fun (a : α) ↦ of P (σ a)) a)
    (Quiver.Hom.unop
      (Iso.inv
        (Iso.op
          (IsColimit.coconePointUniqueUpToIso (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
            (coproductIsCoproduct fun (a : α) ↦ of P (σ a)))))))
Tactic: simp only [opCoproductIsoProduct, ← unop_comp, opCoproductIsoProduct'_comp_self]
-- 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 : α
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))))
⊢ Eq (α := of P (σ a) ⟶ of P (Sigma σ)) (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := ⋯ })
    (CategoryStruct.comp (Y := ∐ fun (a : α) ↦ of P (σ a)) (Sigma.ι (C := CompHausLike P) (fun (a : α) ↦ of P (σ a)) a)
      (Quiver.Hom.unop
        (Iso.inv
          (Iso.op
            (IsColimit.coconePointUniqueUpToIso (finiteCoproduct.isColimit (P := P) fun (a : α) ↦ of P (σ a))
              (coproductIsCoproduct fun (a : α) ↦ of P (σ a)))))))
have h : Eq (α := of P (σ a) ⟶ of P (Sigma σ)) (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := sorry })
  (NatTrans.app (Cocone.ι (finiteCoproduct.cofan (P := P) fun (a : α) ↦ of P (σ a))) { as := a })
Tactic: erw [IsColimit.fac]
-- 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)
⊢ IsIso (X := X.obj (Opposite.op (of P ((a : α) × σ a)))) (Y := (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))))
have rw : IsIso (X := X.obj (Opposite.op (of P ((a : α) × σ a)))) (Y := (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: rw [sigmaComparison_eq_comp_isos]
-- Lean 4 proof step from Mathlib.Topology.Category.CompactlyGenerated (goal)
Goal:
X_1 : Type w
inst : TopologicalSpace X_1
inst_1 : UCompactlyGeneratedSpace X_1
X Y : CompactlyGenerated
f : (↑X.toTop : Type w) ≃ₜ (↑Y.toTop : Type w)
⊢ CategoryStruct.comp (Y := Y)
      (ofHom { toFun := (⇑f : (a : (↑X.toTop : Type w)) → (↑Y.toTop : Type w)), continuous_toFun := ⋯ })
      (ofHom { toFun := (⇑f.symm : (a : (↑Y.toTop : Type w)) → (↑X.toTop : Type w)), continuous_toFun := ⋯ }) =
    𝟙 X
have h : ∀ (x : (↑X.toTop : Type w)),
  Eq (α := (↑X.toTop : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompactlyGenerated.{u, w}) ↦
            C((↑x1.toTop : Type w), (↑x2.toTop : Type w))) (CC := fun (X : CompactlyGenerated.{u, w}) ↦
            (↑X.toTop : Type w)) (X := X) (Y := X)
            (CategoryStruct.comp (Y := Y)
              (ofHom { toFun := (⇑f : (a : (↑X.toTop : Type w)) → (↑Y.toTop : Type w)), continuous_toFun := sorry })
              (ofHom { toFun := (⇑f.symm : (a : (↑Y.toTop : Type w)) → (↑X.toTop : Type w)), continuous_toFun := sorry })) :
          (a : (↑X.toTop : Type w)) → (↑X.toTop : Type w))
        x :
      (↑X.toTop : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompactlyGenerated.{u, w}) ↦
            C((↑x1.toTop : Type w), (↑x2.toTop : Type w))) (CC := fun (X : CompactlyGenerated.{u, w}) ↦
            (↑X.toTop : Type w)) (𝟙 X) :
          (a : (↑X.toTop : Type w)) → (↑X.toTop : Type w))
        x :
      (↑X.toTop : Type w))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.CompactlyGenerated (goal)
Goal:
X_1 : Type w
inst : TopologicalSpace X_1
inst_1 : UCompactlyGeneratedSpace X_1
X Y : CompactlyGenerated
f : (↑X.toTop : Type w) ≃ₜ (↑Y.toTop : Type w)
⊢ CategoryStruct.comp (Y := X)
      (ofHom { toFun := (⇑f.symm : (a : (↑Y.toTop : Type w)) → (↑X.toTop : Type w)), continuous_toFun := ⋯ })
      (ofHom { toFun := (⇑f : (a : (↑X.toTop : Type w)) → (↑Y.toTop : Type w)), continuous_toFun := ⋯ }) =
    𝟙 Y
have h : ∀ (x : (↑Y.toTop : Type w)),
  Eq (α := (↑Y.toTop : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompactlyGenerated.{u, w}) ↦
            C((↑x1.toTop : Type w), (↑x2.toTop : Type w))) (CC := fun (X : CompactlyGenerated.{u, w}) ↦
            (↑X.toTop : Type w)) (X := Y) (Y := Y)
            (CategoryStruct.comp (Y := X)
              (ofHom { toFun := (⇑f.symm : (a : (↑Y.toTop : Type w)) → (↑X.toTop : Type w)), continuous_toFun := sorry })
              (ofHom { toFun := (⇑f : (a : (↑X.toTop : Type w)) → (↑Y.toTop : Type w)), continuous_toFun := sorry })) :
          (a : (↑Y.toTop : Type w)) → (↑Y.toTop : Type w))
        x :
      (↑Y.toTop : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompactlyGenerated.{u, w}) ↦
            C((↑x1.toTop : Type w), (↑x2.toTop : Type w))) (CC := fun (X : CompactlyGenerated.{u, w}) ↦
            (↑X.toTop : Type w)) (𝟙 Y) :
          (a : (↑Y.toTop : Type w)) → (↑Y.toTop : Type w))
        x :
      (↑Y.toTop : Type w))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
x : X.A
⊢ X.str (X.incl x) = x
have change : (ConcreteCategory.hom (FC := TypeCat.Fun) (β.η.app X.A ≫ X.a) :
      (a : (fun (X : Type u_1) ↦ X) ((𝟭 (Type u_1)).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
    x =
  x
Tactic: change ((β).η.app _ ≫ X.a) _ = _
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
x : X.A
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.η.app X.A ≫ X.a) :
        (a : (fun (X : Type u_1) ↦ X) ((𝟭 (Type u_1)).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      x =
    x
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X.A) :
      (a : (fun (X : Type u_1) ↦ X) ((𝟭 (Type u_1)).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
    x =
  x
Tactic: rw [Monad.Algebra.unit]