awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
⊢ IsColimit (F :=
    (K ⋙ uliftFunctor) ⋙
      forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
    (Functor.mapCocone
      (forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
      (uliftFunctor.mapCocone c))

Tactic:
exact isColimitOfPreserves (forget TopCat ⋙ CategoryTheory.uliftFunctor) hc

Premises used: CategoryTheory.Functor.comp, CategoryTheory.uliftFunctor, CategoryTheory.forget, TopCat, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Topology.Category.TopCat.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
Y : Type w'
inst_1 : TopologicalSpace Y
⊢ yonedaPresheaf F Y = F.op ⋙ yonedaPresheaf' Y

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, ContinuousMap.yonedaPresheaf, rfl
-- Module: Mathlib.Topology.Category.TopCat.Yoneda
Goal:
Y : Type w'
inst : TopologicalSpace Y
α : Type
X : α → TopCat
rw :
  (piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x)) ≫
      Iso.hom (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y) =
    (yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      Iso.inv
        ((equivEquivIso :
            (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
              ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
          (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w)))
⊢ Eq (α := (yonedaPresheaf' Y).obj (∏ᶜ fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ (yonedaPresheaf' Y).obj (op (X b)))
    (piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x))
    ((yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      Iso.inv
          ((equivEquivIso :
              (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
                ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
            (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w))) ≫
        Iso.inv (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y))

Tactic:
rw [← Category.assoc, Iso.eq_comp_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.Topology.Category.TopCat.Yoneda
Goal:
Y : Type w'
inst : TopologicalSpace Y
α : Type
X : α → TopCat
h :
  ∀ (x : (yonedaPresheaf' Y).obj (∏ᶜ fun (x : α) ↦ op (X x))) (x_1 : α) (a : (↑(X x_1) : Type w)),
    Eq.{w' + 1} (α := Y)
      ((TypeCat.Fun.toFun
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                ((piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x)) ≫
                  Iso.hom (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y)))
              x x_1 :
            (a : (↑(X x_1) : Type w)) → Y)
          a :
        Y)
      ((TypeCat.Fun.toFun
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                ((yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
                  Iso.inv
                    ((equivEquivIso :
                        (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
                          ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
                      (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w)))))
              x x_1 :
            (a : (↑(X x_1) : Type w)) → Y)
          a :
        Y)
⊢ (piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x)) ≫
      Iso.hom (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y) =
    (yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      Iso.inv
        ((equivEquivIso :
            (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
              ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
          (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w)))

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.Yoneda
Goal:
Y : Type w'
inst : TopologicalSpace Y
α : Type
X : α → TopCat
x : (yonedaPresheaf' Y).obj (∏ᶜ fun (x : α) ↦ op (X x))
x_1 : α
a : (↑(X x_1) : Type w)
h :
  Eq.{w' + 1} (α := Y)
    ((x : (a : (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) → Y)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (X := ∐ X) (Quiver.Hom.unop (Iso.inv (opCoproductIsoProduct X))) :
              (a : (↑(∐ X) : Type w)) → (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC :=
                    TopCat.carrier) (Y := ∐ X) (Sigma.ι X x_1) :
                  (a : (↑(X x_1) : Type w)) → (↑(∐ X) : Type w))
                a :
              (↑(∐ X) : Type w)) :
          (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) :
      Y)
    ((x : (a : (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) → Y)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (X := ∐ X) (Quiver.Hom.unop (Iso.inv (opCoproductIsoProduct X))) :
              (a : (↑(∐ X) : Type w)) → (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC :=
                    TopCat.carrier) (TopCat.sigmaIsoSigma X).inv :
                  (a : (i : α) × (↑(X i) : Type w)) → (↑(∐ X) : Type w))
                (Sigma.mk (β := fun (x : α) ↦ (↑(X x) : Type w)) x_1 a) :
              (↑(∐ X) : Type w)) :
          (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) :
      Y)
⊢ Eq.{w' + 1} (α := Y)
    ((TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x)) ≫
                Iso.hom (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y)))
            x x_1 :
          (a : (↑(X x_1) : Type w)) → Y)
        a :
      Y)
    ((TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
                Iso.inv
                  ((equivEquivIso :
                      (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
                        ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
                    (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w)))))
            x x_1 :
          (a : (↑(X x_1) : Type w)) → Y)
        a :
      Y)

Tactic:
simp [yonedaPresheaf', piComparison, ← opCoproductIsoProduct_inv_comp_ι]

Premises used: CategoryTheory.Limits.piComparison, ContinuousMap.yonedaPresheaf', CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι
-- Module: Mathlib.Topology.Category.TopCat.Yoneda
Goal:
Y : Type w'
inst : TopologicalSpace Y
α : Type
X : α → TopCat
x : (yonedaPresheaf' Y).obj (∏ᶜ fun (x : α) ↦ op (X x))
x_1 : α
a : (↑(X x_1) : Type w)
⊢ Eq.{w' + 1} (α := Y)
    ((x : (a : (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) → Y)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (X := ∐ X) (Quiver.Hom.unop (Iso.inv (opCoproductIsoProduct X))) :
              (a : (↑(∐ X) : Type w)) → (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC :=
                    TopCat.carrier) (Y := ∐ X) (Sigma.ι X x_1) :
                  (a : (↑(X x_1) : Type w)) → (↑(∐ X) : Type w))
                a :
              (↑(∐ X) : Type w)) :
          (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) :
      Y)
    ((x : (a : (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) → Y)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (X := ∐ X) (Quiver.Hom.unop (Iso.inv (opCoproductIsoProduct X))) :
              (a : (↑(∐ X) : Type w)) → (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC :=
                    TopCat.carrier) (TopCat.sigmaIsoSigma X).inv :
                  (a : (i : α) × (↑(X i) : Type w)) → (↑(∐ X) : Type w))
                (Sigma.mk (β := fun (x : α) ↦ (↑(X x) : Type w)) x_1 a) :
              (↑(∐ X) : Type w)) :
          (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) :
      Y)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
Y : Type w'
inst_1 : TopologicalSpace Y
x : ℕ
K : Discrete (Fin x) ⥤ TopCatᵒᵖ
α : Type
X : α → TopCat
rw :
  IsIso (Y := ∏ᶜ fun (b : α) ↦ (yonedaPresheaf' Y).obj ((fun (x : α) ↦ op (X x)) b))
    ((yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      Iso.inv
          ((equivEquivIso :
              (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
                ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
            (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w))) ≫
        Iso.inv (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y))
⊢ IsIso (X := (yonedaPresheaf' Y).obj (∏ᶜ fun (x : α) ↦ op (X x))) (Y :=
    ∏ᶜ fun (b : α) ↦ (yonedaPresheaf' Y).obj ((fun (x : α) ↦ op (X x)) b))
    (piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x))

Tactic:
rw [piComparison_fac]

Premises used: ContinuousMap.piComparison_fac
-- Module: Mathlib.Topology.Category.TopCat.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
Y : Type w'
inst_1 : TopologicalSpace Y
x : ℕ
K : Discrete (Fin x) ⥤ TopCatᵒᵖ
α : Type
X : α → TopCat
⊢ IsIso (Y := ∏ᶜ fun (b : α) ↦ (yonedaPresheaf' Y).obj ((fun (x : α) ↦ op (X x)) b))
    ((yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      Iso.inv
          ((equivEquivIso :
              (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
                ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
            (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w))) ≫
        Iso.inv (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.TopCommRingCat
Goal:
R : TopCommRingCat
dsimp : Continuous (Y := R.α) fun (x : R.α) ↦ x
⊢ Continuous.{u, u} (X := R.α) (Y := R.α)
    (⇑{ toFun := fun (x : R.α) ↦ x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } : (a : R.α) → R.α)

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.TopCommRingCat
Goal:
R : TopCommRingCat
⊢ Continuous (Y := R.α) fun (x : R.α) ↦ x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCommRingCat
Goal:
X Y Z : TopCommRingCat
f : { f : X.α →+* Y.α // Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α) }
g : { f : Y.α →+* Z.α // Continuous (X := Y.α) (Y := Z.α) (⇑f : (a : Y.α) → Z.α) }
mk :
  ∀ (val : X.α →+* Y.α) (property : Continuous (X := X.α) (Y := Y.α) (⇑val : (a : X.α) → Y.α)),
    Continuous (X := X.α) (Y := Z.α)
      (⇑((↑g : Y.α →+* Z.α).comp
            (↑(Subtype.mk (p := fun (f : X.α →+* Y.α) ↦ Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α)) val
                  property) :
              X.α →+* Y.α)) :
        (a : X.α) → Z.α)
⊢ Continuous (X := X.α) (Y := Z.α) (⇑((↑g : Y.α →+* Z.α).comp (↑f : X.α →+* Y.α)) : (a : X.α) → Z.α)

Tactic:
cases f
-- Module: Mathlib.Topology.Category.TopCommRingCat
Goal:
X Y Z : TopCommRingCat
g : { f : Y.α →+* Z.α // Continuous (X := Y.α) (Y := Z.α) (⇑f : (a : Y.α) → Z.α) }
val : X.α →+* Y.α
property : Continuous (X := X.α) (Y := Y.α) (⇑val : (a : X.α) → Y.α)
mk :
  ∀ (val_1 : Y.α →+* Z.α) (property_1 : Continuous (X := Y.α) (Y := Z.α) (⇑val_1 : (a : Y.α) → Z.α)),
    Continuous (X := X.α) (Y := Z.α)
      (⇑((↑(Subtype.mk (p := fun (f : Y.α →+* Z.α) ↦ Continuous (X := Y.α) (Y := Z.α) (⇑f : (a : Y.α) → Z.α)) val_1
                    property_1) :
                Y.α →+* Z.α).comp
            (↑(Subtype.mk (p := fun (f : X.α →+* Y.α) ↦ Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α)) val
                  property) :
              X.α →+* Y.α)) :
        (a : X.α) → Z.α)
⊢ Continuous (X := X.α) (Y := Z.α)
    (⇑((↑g : Y.α →+* Z.α).comp
          (↑(Subtype.mk (p := fun (f : X.α →+* Y.α) ↦ Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α)) val
                property) :
            X.α →+* Y.α)) :
      (a : X.α) → Z.α)

Tactic:
cases g
-- Module: Mathlib.Topology.Category.TopCommRingCat
Goal:
X Y Z : TopCommRingCat
val : X.α →+* Y.α
property : Continuous (X := X.α) (Y := Y.α) (⇑val : (a : X.α) → Y.α)
val_1 : Y.α →+* Z.α
property_1 : Continuous (X := Y.α) (Y := Z.α) (⇑val_1 : (a : Y.α) → Z.α)
mk : Continuous (X := X.α) (Y := Z.α) (Function.comp (β := Y.α) (⇑val_1 : (a : Y.α) → Z.α) (⇑val : (a : X.α) → Y.α))
⊢ Continuous (X := X.α) (Y := Z.α)
    (⇑((↑(Subtype.mk (p := fun (f : Y.α →+* Z.α) ↦ Continuous (X := Y.α) (Y := Z.α) (⇑f : (a : Y.α) → Z.α)) val_1
                  property_1) :
              Y.α →+* Z.α).comp
          (↑(Subtype.mk (p := fun (f : X.α →+* Y.α) ↦ Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α)) val
                property) :
            X.α →+* Y.α)) :
      (a : X.α) → Z.α)

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.TopCommRingCat
Goal:
X Y Z : TopCommRingCat
val : X.α →+* Y.α
property : Continuous (X := X.α) (Y := Y.α) (⇑val : (a : X.α) → Y.α)
val_1 : Y.α →+* Z.α
property_1 : Continuous (X := Y.α) (Y := Z.α) (⇑val_1 : (a : Y.α) → Z.α)
⊢ Continuous (X := X.α) (Y := Z.α) (Function.comp (β := Y.α) (⇑val_1 : (a : Y.α) → Z.α) (⇑val : (a : X.α) → Y.α))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCommRingCat
Goal:
X : Type u
inst : CommRing X
inst_1 : TopologicalSpace X
inst_2 : IsTopologicalRing X
⊢ (of X).α = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCommRingCat
Goal:
R : TopCommRingCat
⊢ IsTopologicalRing.{u_1}
    (↑(Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u_1}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
            fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
          R) :
      Type u_1)

Tactic:
R.isTopologicalRing

Premises used: TopCommRingCat.isTopologicalRing
-- Module: Mathlib.Topology.Category.TopCommRingCat
Goal:
X Y : TopCommRingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
        { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
        fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
      X)
    (CategoryTheory.Functor.map
      (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
        { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
        fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
      f)
i_Top : Functor.obj
    (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
      { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
      fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
    X ≅
  Functor.obj
    (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
      { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
      fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
        { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
        fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
      f)
e_Ring : X.α ≃+* Y.α :=
  let __src := (↑f : X.α →+* Y.α);
  let __src_1 :
    Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier))
        (Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
            fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
          X) ≃
      Functor.obj
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier))
        (Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := α) TopCat (FD :=
            fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := TopCat.carrier))
          Y) :=
    Iso.toEquiv
      (Functor.mapIso
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)) i_Top);
  { toFun := (↑(↑__src : X.α →* Y.α) : OneHom X.α Y.α).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯,
    map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f

Tactic:
exact
      ⟨⟨⟨e_Ring.symm, i_Top.inv.hom.2⟩,
          ⟨by
            ext x
            exact e_Ring.left_inv x, by
            ext x
            exact e_Ring.right_inv x⟩⟩⟩
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X : TopPair
⊢ Topology.IsEmbedding (X := (↑(snd (X := X)) : Type u)) (Y := (↑(fst (X := X)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          snd (X := X)) map) :
      (a : (↑snd : Type u)) → (↑fst : Type u))

Tactic:
X.prop

Premises used: CategoryTheory.MorphismProperty.Comma.prop
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X Y : TopPair
f : X ⟶ Y
⊢ snd f ≫ map = map ≫ fst f

Tactic:
f.hom.w

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.MorphismProperty.Comma.Hom.hom
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X_1 Y_1 X Y Z : TopPair
X_2 Y_2 : TopCat
f : X_2 ⟶ Y_2
w :
  ∀ (x : (↑(snd (X := ofTopCat X_2)) : Type u)),
    Eq (α := (↑(fst (X := ofTopCat Y_2)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (𝟙 (snd (X := ofTopCat X_2)) ≫ map) :
            (a : (↑snd : Type u)) → (↑fst : Type u))
          x :
        (↑(fst (X := ofTopCat Y_2)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              snd (X := ofTopCat X_2)) (Y := fst (X := ofTopCat Y_2)) (map ≫ f) :
            (a : (↑snd : Type u)) → (↑fst : Type u))
          x :
        (↑(fst (X := ofTopCat Y_2)) : Type u))
⊢ 𝟙 (snd (X := ofTopCat X_2)) ≫ map = map ≫ f

Tactic:
ext x
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X_1 Y_1 X Y Z : TopPair
X_2 Y_2 : TopCat
f : X_2 ⟶ Y_2
x : (↑(snd (X := ofTopCat X_2)) : Type u)
⊢ Eq (α := (↑(fst (X := ofTopCat Y_2)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (𝟙 (snd (X := ofTopCat X_2)) ≫ map) :
          (a : (↑snd : Type u)) → (↑fst : Type u))
        x :
      (↑(fst (X := ofTopCat Y_2)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            snd (X := ofTopCat X_2)) (Y := fst (X := ofTopCat Y_2)) (map ≫ f) :
          (a : (↑snd : Type u)) → (↑fst : Type u))
        x :
      (↑(fst (X := ofTopCat Y_2)) : Type u))

Tactic:
induction x
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X_1 Y_1 X_2 Y_2 Z : TopPair
X Y : TopPair
f : X ⟶ Y
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  (CategoryTheory.Functor.map (𝟭 TopPair) f ≫ ofHom (𝟙 (fst (X := Y))) map ⋯).toCommaMorphism (P := isEmbedding) (Q :=
        ⊤) (W := ⊤).right =
    CommaMorphism.right
      (MorphismProperty.Comma.Hom.toCommaMorphism (P := isEmbedding) (Q := ⊤) (W := ⊤)
        (ofHom (𝟙 (fst (X := X))) map ⋯ ≫ (proj₁ ⋙ diag).map f))
⊢ (CategoryTheory.Functor.map (𝟭 TopPair) f ≫ ofHom (𝟙 (fst (X := Y))) map ⋯).toCommaMorphism (P := isEmbedding) (Q :=
        ⊤) (W := ⊤).right =
    CommaMorphism.right
      (MorphismProperty.Comma.Hom.toCommaMorphism (P := isEmbedding) (Q := ⊤) (W := ⊤)
        (ofHom (𝟙 (fst (X := X))) map ⋯ ≫ (proj₁ ⋙ diag).map f))

Tactic:
cat_disch
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X Y : TopPair
f g : X ⟶ Y
H : Homotopy f g
x : (↑(TopPair.snd (X := X)) : Type u)
t : (↑unitInterval : Type)
⊢ Eq (α := (↑(TopPair.fst (X := Y)) : Type u))
    ((H.fst : (a : (↑unitInterval : Type) × (↑TopPair.fst : Type u)) → (↑TopPair.fst : Type u))
        (((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type))
              (x, (I.homeomorph.symm : (a : (↑unitInterval : Type)) → (↑I : Type u)) t).2,
            (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  TopPair.snd (X := X)) map :
                (a : (↑TopPair.snd : Type u)) → (↑TopPair.fst : Type u))
              ((x, (I.homeomorph.symm : (a : (↑unitInterval : Type)) → (↑I : Type u)) t) :
                  (↑(TopPair.snd (X := X)) : Type u) × (↑I : Type u)).1) :
          (↑unitInterval : Type) × (↑(TopPair.fst (X := X)) : Type u)) :
      (↑(TopPair.fst (X := Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            TopPair.snd (X := Y)) map :
          (a : (↑TopPair.snd : Type u)) → (↑TopPair.fst : Type u))
        ((H.snd : (a : (↑unitInterval : Type) × (↑TopPair.snd : Type u)) → (↑TopPair.snd : Type u))
            (((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type))
                  (x, (I.homeomorph.symm : (a : (↑unitInterval : Type)) → (↑I : Type u)) t).2,
                ((x, (I.homeomorph.symm : (a : (↑unitInterval : Type)) → (↑I : Type u)) t) :
                    (↑(TopPair.snd (X := X)) : Type u) × (↑I : Type u)).1) :
              (↑unitInterval : Type) × (↑(TopPair.snd (X := X)) : Type u)) :
          (↑(TopPair.snd (X := Y)) : Type u)) :
      (↑(TopPair.fst (X := Y)) : Type u))

Tactic:
have := w_apply H (x, I.homeomorph.symm t)
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X Y : TopPair
f₀ f₁ : X ⟶ Y
⊢ Function.Bijective.{u + 1, u + 1} (α := Homotopy f₀ f₁) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, TopPair.Homotopy.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X_1 Y_1 X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
w :
  ∀ (fst : (↑(TopPair.snd (X := X)) : Type u)) (snd : (↑I : Type u)),
    Eq (α := (↑(TopPair.fst (X := Y)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (map ▷ I ≫ Homotopy.h (F.fst.trans G.fst)) :
            (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑TopPair.fst : Type u))
          (fst, snd) :
        (↑(TopPair.fst (X := Y)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (Homotopy.h (F.snd.trans G.snd) ≫ map) :
            (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑TopPair.fst : Type u))
          (fst, snd) :
        (↑(TopPair.fst (X := Y)) : Type u))
⊢ map ▷ I ≫ Homotopy.h (F.fst.trans G.fst) = Homotopy.h (F.snd.trans G.snd) ≫ map

Tactic:
ext ⟨_, _⟩