awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
mp :
  Mono f →
    Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
mpr :
  Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
    Mono f
⊢ Mono f ↔
    Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)

Tactic:
constructor
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (↑(X.toTop (P := P)) : Type u)
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₁ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₂ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
g₁ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₂, continuous_toFun := ⋯ }
h₁ :
  ∀ (a : (↑(X.toTop (P := P)) : Type u)),
    Eq (α := (↑(Y.toTop (P := P)) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) (g₁ ≫ f) :
            (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
          a :
        (↑(Y.toTop (P := P)) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) (g₂ ≫ f) :
            (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
          a :
        (↑(Y.toTop (P := P)) : Type u))
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
ext
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (↑(X.toTop (P := P)) : Type u)
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₁ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₂ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
g₁ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₂, continuous_toFun := ⋯ }
a : (↑(X.toTop (P := P)) : Type u)
⊢ Eq (α := (↑(Y.toTop (P := P)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (g₁ ≫ f) :
          (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
        a :
      (↑(Y.toTop (P := P)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (g₂ ≫ f) :
          (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
        a :
      (↑(Y.toTop (P := P)) : Type u))

Tactic:
h
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (↑(X.toTop (P := P)) : Type u)
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₁ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₂ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
g₁ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₂, continuous_toFun := ⋯ }
a : (↑(X.toTop (P := P)) : Type u)
⊢ Eq (α := (↑(Y.toTop (P := P)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (g₁ ≫ f) :
          (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
        a :
      (↑(Y.toTop (P := P)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (g₂ ≫ f) :
          (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
        a :
      (↑(Y.toTop (P := P)) : Type u))

Tactic:
exact h
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (↑(X.toTop (P := P)) : Type u)
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₁ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₂ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
g₁ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₂, continuous_toFun := ⋯ }
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
have : g₁ ≫ f = g₂ ≫ f := by ext; exact h
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (↑(X.toTop (P := P)) : Type u)
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₁ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₂ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
g₁ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₂, continuous_toFun := ⋯ }
this : g₁ ≫ f = g₂ ≫ f
⊢ x₁ = x₂

Tactic:
CategoryTheory.congr_fun ((cancel_mono _).mp this) x₁

Premises used: CategoryTheory.congr_fun, CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (↑(X.toTop (P := P)) : Type u)
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₁ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₂ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
g₁ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₂, continuous_toFun := ⋯ }
this : g₁ ≫ f = g₂ ≫ f
⊢ x₁ = x₂

Tactic:
exact CategoryTheory.congr_fun ((cancel_mono _).mp this) x₁

Premises used: CategoryTheory.congr_fun, CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
mpr :
  Mono (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)) →
    Mono f
⊢ Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
    Mono f

Tactic:
rw [← CategoryTheory.ofHom_mono_iff_injective]

Premises used: CategoryTheory.ofHom_mono_iff_injective
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)) →
    Mono f

Tactic:
apply (forget (CompHausLike P)).mono_of_mono_map

Premises used: CompHausLike, CategoryTheory.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ IsClosedMap (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)

Tactic:
fun _ hC =>
  (hC.isCompact.image f.hom.hom.continuous).isClosed

Premises used: ContinuousMap.continuous, IsClosedMap, TopCat.Hom.hom, IsClosed.isCompact, CategoryTheory.InducedCategory.Hom.hom, IsCompact.image, IsCompact.isClosed
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
rw :
  ∀ (s : Set ((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)),
    IsClosed s →
      IsClosed (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        ((⇑E.symm :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) ⁻¹'
          s)
⊢ Continuous (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    (⇑E.symm :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)

Tactic:
rw [continuous_iff_isClosed]

Premises used: continuous_iff_isClosed
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
S : Set ((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
hS : IsClosed S
rw :
  IsClosed (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((⇑E :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) ''
      S)
⊢ IsClosed (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((⇑E.symm :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) ⁻¹'
      S)

Tactic:
rw [← E.image_eq_preimage_symm]

Premises used: Equiv.image_eq_preimage_symm
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
S : Set ((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
hS : IsClosed S
⊢ IsClosed (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((⇑E :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) ''
      S)

Tactic:
isClosedMap f S hS

Premises used: CompHausLike.isClosedMap
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
S : Set ((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
hS : IsClosed S
⊢ IsClosed (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((⇑E :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) ''
      S)

Tactic:
exact isClosedMap f S hS

Premises used: CompHausLike.isClosedMap
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
⊢ Continuous (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    (⇑E.symm :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)

Tactic:
have hE : Continuous E.symm := by
    rw [continuous_iff_isClosed]
    intro S hS
    rw [← E.image_eq_preimage_symm]
    exact isClosedMap f S hS