awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 := ⋯ })
    (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)))))))
⊢ 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))))

Tactic:
rw [← opCoproductIsoProduct_inv_comp_ι]

Premises used: CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι
-- 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 := ⋯ })
    (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)))))))
⊢ 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)))))))

Tactic:
simp only [Opposite.unop_op, unop_comp, Quiver.Hom.unop_op, Category.assoc]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.unop_comp, Opposite.unop_op
-- 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 := ⋯ })
    (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)))))))
⊢ 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)))))))

Tactic:
simp only [opCoproductIsoProduct, ← unop_comp, opCoproductIsoProduct'_comp_self]

Premises used: CategoryTheory.Limits.opCoproductIsoProduct'_comp_self, CategoryTheory.unop_comp, CategoryTheory.Limits.opCoproductIsoProduct
-- 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 := ⋯ })
    (NatTrans.app (Cocone.ι (finiteCoproduct.cofan (P := P) fun (a : α) ↦ of P (σ a))) { as := 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)))))))

Tactic:
erw [IsColimit.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- 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))))
⊢ Eq (α := of P (σ a) ⟶ of P (Sigma σ)) (ofHom P { toFun := Sigma.mk (β := σ) a, continuous_toFun := ⋯ })
    (NatTrans.app (Cocone.ι (finiteCoproduct.cofan (P := P) fun (a : α) ↦ of P (σ a))) { as := a })

Tactic:
rfl
-- 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)
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))))
⊢ 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))))

Tactic:
rw [sigmaComparison_eq_comp_isos]

Premises used: CompHausLike.sigmaComparison_eq_comp_isos
-- 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)
⊢ 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:
infer_instance
-- Module: Mathlib.Topology.Category.CompactlyGenerated
Goal:
X : Type w
inst : TopologicalSpace X
inst_1 : UCompactlyGeneratedSpace X
⊢ compactlyGeneratedToTop.Full

Tactic:
fullyFaithfulCompactlyGeneratedToTop.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CompactlyGenerated.fullyFaithfulCompactlyGeneratedToTop
-- Module: Mathlib.Topology.Category.CompactlyGenerated
Goal:
X : Type w
inst : TopologicalSpace X
inst_1 : UCompactlyGeneratedSpace X
⊢ compactlyGeneratedToTop.Faithful

Tactic:
fullyFaithfulCompactlyGeneratedToTop.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CompactlyGenerated.fullyFaithfulCompactlyGeneratedToTop
-- Module: Mathlib.Topology.Category.CompactlyGenerated
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)
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 := ⋯ })
                (ofHom
                  { toFun := (⇑f.symm : (a : (↑Y.toTop : Type w)) → (↑X.toTop : Type w)), continuous_toFun := ⋯ })) :
            (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))
⊢ 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

Tactic:
ext x
-- Module: Mathlib.Topology.Category.CompactlyGenerated
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)
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 := ⋯ })
              (ofHom { toFun := (⇑f.symm : (a : (↑Y.toTop : Type w)) → (↑X.toTop : Type w)), continuous_toFun := ⋯ })) :
          (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:
f.symm_apply_apply x

Premises used: Homeomorph.symm_apply_apply
-- Module: Mathlib.Topology.Category.CompactlyGenerated
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)
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 := ⋯ })
              (ofHom { toFun := (⇑f.symm : (a : (↑Y.toTop : Type w)) → (↑X.toTop : Type w)), continuous_toFun := ⋯ })) :
          (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:
exact f.symm_apply_apply x

Premises used: Homeomorph.symm_apply_apply
-- Module: Mathlib.Topology.Category.CompactlyGenerated
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)
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 := ⋯ })
                (ofHom { toFun := (⇑f : (a : (↑X.toTop : Type w)) → (↑Y.toTop : Type w)), continuous_toFun := ⋯ })) :
            (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))
⊢ 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

Tactic:
ext x
-- Module: Mathlib.Topology.Category.CompactlyGenerated
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)
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 := ⋯ })
              (ofHom { toFun := (⇑f : (a : (↑X.toTop : Type w)) → (↑Y.toTop : Type w)), continuous_toFun := ⋯ })) :
          (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:
f.apply_symm_apply x

Premises used: Homeomorph.apply_symm_apply
-- Module: Mathlib.Topology.Category.CompactlyGenerated
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)
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 := ⋯ })
              (ofHom { toFun := (⇑f : (a : (↑X.toTop : Type w)) → (↑Y.toTop : Type w)), continuous_toFun := ⋯ })) :
          (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:
exact f.apply_symm_apply x

Premises used: Homeomorph.apply_symm_apply
-- Module: Mathlib.Topology.Category.Compactum
Goal:
⊢ forget.Faithful

Tactic:
show (Monad.forget _).Faithful from inferInstance

Premises used: Compactum.forget, inferInstance, Compactum