awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ (↑(of X) : Type u) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X : TopCat
⊢ of (↑X : Type u) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X : TopCat
⊢ Hom.hom (𝟙 X) = ContinuousMap.id (↑X : Type u)

Tactic:
rfl

Premises used: ContinuousMap.id, rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X : TopCat
x : (↑X : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (𝟙 X) :
        (a : (↑X : Type u)) → (↑X : Type u))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X : TopCat
⊢ Eq (α := (a : (↑X : Type u)) → (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (𝟙 X)) :
      (a : (↑X : Type u)) → (↑X : Type u))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type u)
⊢ Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g) :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
              (a : (↑X : Type u)) → (↑Y : Type u))
            x :
          (↑Y : Type u)) :
      (↑Z : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u)) → (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u)) → (↑Z : Type u))
    (Function.comp (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: TopCat.Hom.ext
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u)),
    Eq (α := (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : Type u
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ ofHom (ContinuousMap.id X) = 𝟙 (of X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : Type u
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : Type u
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (ofHom f) :
          (a : (↑(of X) : Type u)) → (↑(of Y) : Type u))
        x :
      (↑(of Y) : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : X ≅ Y
x : (↑X : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.inv :
        (a : (↑Y : Type u)) → (↑X : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.hom :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u)) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : X ≅ Y
y : (↑Y : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.hom :
        (a : (↑X : Type u)) → (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.inv :
            (a : (↑Y : Type u)) → (↑X : Type u))
          y :
        (↑X : Type u)) =
    y

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : Type u
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
x : Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) (of X)
⊢ Eq (α :=
    Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) (of Y))
    ((ofHom f : (a : (forget TopCat).obj (of X)) → (forget TopCat).obj (of Y)) x :
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
        (of Y))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X : Type u
⊢ DiscreteTopology.{u} (↑(discrete.obj X) : Type u)

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : X ≅ Y
x : (↑Y : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.hom :
        (a : (↑X : Type u)) → (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.inv :
            (a : (↑Y : Type u)) → (↑X : Type u))
          x :
        (↑X : Type u)) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : (↑X : Type u) ≃ₜ (↑Y : Type u)
H :
  ∀ (x : (↑X : Type u)),
    Eq (α := (↑Y : Type u)) ((homeoOfIso (isoOfHomeo f) : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
      ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
⊢ homeoOfIso (isoOfHomeo f) = f

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : (↑X : Type u) ≃ₜ (↑Y : Type u)
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u)) ((homeoOfIso (isoOfHomeo f) : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
    ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : X ≅ Y
w :
  ∀ (x : (↑X : Type u)),
    Eq (α := (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (isoOfHomeo (homeoOfIso f)).hom :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.hom :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
⊢ isoOfHomeo (homeoOfIso f) = f

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : X ≅ Y
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (isoOfHomeo (homeoOfIso f)).hom :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.hom :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : X ⟶ Y
hfbij :
  Function.Bijective (α := (↑X : Type u)) (β := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
hfcl :
  IsOpenMap (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
⊢ IsIso f

Tactic:
let e : X ≃ₜ Y :=
    (Equiv.ofBijective f hfbij).toHomeomorphOfContinuousOpen f.hom.continuous hfcl
  inferInstanceAs <| IsIso (TopCat.isoOfHomeo e).hom

Premises used: ContinuousMap.continuous, CategoryTheory.ConcreteCategory.hom, _private.0.TopCat.isIso_of_bijective_of_isOpenMap._proof_1, Equiv.toHomeomorphOfContinuousOpen, TopCat.Hom.hom, Equiv.ofBijective, DFunLike.coe
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : X ⟶ Y
hfbij :
  Function.Bijective (α := (↑X : Type u)) (β := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
hfcl :
  IsClosedMap (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
⊢ IsIso f

Tactic:
let e : X ≃ₜ Y :=
    (Equiv.ofBijective f hfbij).toHomeomorphOfContinuousClosed f.hom.continuous hfcl
  inferInstanceAs <| IsIso (TopCat.isoOfHomeo e).hom

Premises used: ContinuousMap.continuous, CategoryTheory.ConcreteCategory.hom, Equiv.toHomeomorphOfContinuousClosed, TopCat.Hom.hom, Equiv.ofBijective, DFunLike.coe, _private.0.TopCat.isIso_of_bijective_of_isClosedMap._proof_1
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ IsIso f ↔
    IsHomeomorph (X := (↑X : Type u)) (Y := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
⟨fun _ ↦ (homeoOfIso (asIso f)).isHomeomorph,
    fun H ↦ isIso_of_bijective_of_isOpenMap _ H.bijective H.isOpenMap⟩

Premises used: IsHomeomorph.isOpenMap, Homeomorph.isHomeomorph, TopCat.isIso_of_bijective_of_isOpenMap, TopCat.homeoOfIso, IsHomeomorph.bijective, Iff.intro, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso g
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u)) ↔
    IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
(TopCat.homeoOfIso (asIso g)).isOpenEmbedding.of_comp_iff f

Premises used: CategoryTheory.ConcreteCategory.hom, TopCat.homeoOfIso, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.of_comp_iff, DFunLike.coe, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso g
simp :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (Function.comp (β := (↑Y : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))) ↔
    IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (Function.comp (β := (↑Y : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))) ↔
    IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
simp only
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso g
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (Function.comp (β := (↑Y : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))) ↔
    IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
isOpenEmbedding_iff_comp_isIso f g

Premises used: TopCat.isOpenEmbedding_iff_comp_isIso
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso g
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (Function.comp (β := (↑Y : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))) ↔
    IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
exact isOpenEmbedding_iff_comp_isIso f g

Premises used: TopCat.isOpenEmbedding_iff_comp_isIso
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
mp :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u)) →
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
mpr :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u)) →
    IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u))
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u)) ↔
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))

Tactic:
constructor
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
h :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u)) → (↑Z : Type u))
⊢ IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (Function.comp (β := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u))
      (⇑(homeoOfIso (asIso f).symm) : (a : (↑Y : Type u)) → (↑X : Type u)))

Tactic:
h.comp (TopCat.homeoOfIso (asIso f).symm).isOpenEmbedding

Premises used: TopCat.homeoOfIso, CategoryTheory.Iso.symm, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
h :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u)) → (↑Z : Type u))
h₁ :
  Eq (α := (↑Y : Type u) → (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
    (Function.comp (β := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u))
      (⇑(homeoOfIso (asIso f).symm) : (a : (↑Y : Type u)) → (↑X : Type u)))
⊢ IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))

Tactic:
convert! h.comp (TopCat.homeoOfIso (asIso f).symm).isOpenEmbedding

Premises used: TopCat.homeoOfIso, CategoryTheory.Iso.symm, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
h :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u)) → (↑Z : Type u))
⊢ Eq (α := (↑Y : Type u) → (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
    (Function.comp (β := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u))
      (⇑(homeoOfIso (asIso f).symm) : (a : (↑Y : Type u)) → (↑X : Type u)))

Tactic:
congr_arg (DFunLike.coe ∘ ConcreteCategory.hom) (IsIso.inv_hom_id_assoc f g).symm

Premises used: CategoryTheory.ConcreteCategory.hom, Function.comp, congr_arg, CategoryTheory.IsIso.inv_hom_id_assoc, Eq.symm, DFunLike.coe
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
h :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u)) → (↑Z : Type u))
⊢ Eq (α := (↑Y : Type u) → (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
    (Function.comp (β := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u))
      (⇑(homeoOfIso (asIso f).symm) : (a : (↑Y : Type u)) → (↑X : Type u)))

Tactic:
exact congr_arg (DFunLike.coe ∘ ConcreteCategory.hom) (IsIso.inv_hom_id_assoc f g).symm

Premises used: CategoryTheory.ConcreteCategory.hom, Function.comp, congr_arg, CategoryTheory.IsIso.inv_hom_id_assoc, Eq.symm, DFunLike.coe
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
⊢ IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u)) →
    IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u))

Tactic:
fun h => h.comp (TopCat.homeoOfIso (asIso f)).isOpenEmbedding

Premises used: TopCat.homeoOfIso, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
⊢ IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u)) →
    IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u))

Tactic:
exact fun h => h.comp (TopCat.homeoOfIso (asIso f)).isOpenEmbedding
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
simp :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (Function.comp (β := (↑Y : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))) ↔
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (Function.comp (β := (↑Y : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))) ↔
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))

Tactic:
simp only