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
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
hE :
  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)
⊢ IsIso f

Tactic:
⟨⟨ofHom _ ⟨E.symm, hE⟩, ?_, ?_⟩⟩

Premises used: CompHausLike.ofHom, ContinuousMap.mk, And.intro, Exists.intro, Equiv.symm, CategoryTheory.IsIso.mk, DFunLike.coe
-- 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
hE :
  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)
refine_1 :
  Eq (α := X ⟶ X)
    (f ≫
        ofHom P
          {
            toFun :=
              (⇑E.symm :
                (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
            continuous_toFun := hE } :
      X ⟶ X)
    (𝟙 X : X ⟶ X)
refine_2 :
  Eq (α := Y ⟶ Y)
    (ofHom P
          {
            toFun :=
              (⇑E.symm :
                (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
            continuous_toFun := hE } ≫
        f :
      Y ⟶ Y)
    (𝟙 Y : Y ⟶ Y)
⊢ IsIso f

Tactic:
refine ⟨⟨ofHom _ ⟨E.symm, hE⟩, ?_, ?_⟩⟩
-- 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
hE :
  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)
refine_1 :
  ∀ (x : (↑(X.toTop (P := P)) : Type u)),
    Eq (α := (↑(X.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)) (Y := X)
                (f ≫
                    ofHom P
                      {
                        toFun :=
                          (⇑E.symm :
                            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
                        continuous_toFun := hE } :
                  X ⟶ X) :
              C((↑(X.toTop (P := P)) : Type u), (↑(X.toTop (P := P)) : Type u))) :
            (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
          x :
        (↑(X.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)) (𝟙 X) :
            (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
          x :
        (↑(X.toTop (P := P)) : Type u))
⊢ Eq (α := X ⟶ X)
    (f ≫
        ofHom P
          {
            toFun :=
              (⇑E.symm :
                (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
            continuous_toFun := hE } :
      X ⟶ X)
    (𝟙 X : X ⟶ X)

Tactic:
ext x
-- 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
hE :
  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)
x : (↑(X.toTop (P := P)) : Type u)
⊢ Eq (α := (↑(X.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)) (Y := X)
              (f ≫
                  ofHom P
                    {
                      toFun :=
                        (⇑E.symm :
                          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
                      continuous_toFun := hE } :
                X ⟶ X) :
            C((↑(X.toTop (P := P)) : Type u), (↑(X.toTop (P := P)) : Type u))) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑(X.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)) (𝟙 X) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑(X.toTop (P := P)) : Type u))

Tactic:
apply E.symm_apply_apply

Premises used: Equiv.symm_apply_apply
-- 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
hE :
  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)
refine_2 :
  ∀ (x : (↑(Y.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)) (X := Y)
                (ofHom P
                      {
                        toFun :=
                          (⇑E.symm :
                            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
                        continuous_toFun := hE } ≫
                    f :
                  Y ⟶ Y) :
              C((↑(Y.toTop (P := P)) : Type u), (↑(Y.toTop (P := P)) : Type u))) :
            (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
          x :
        (↑(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)) (𝟙 Y) :
            (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
          x :
        (↑(Y.toTop (P := P)) : Type u))
⊢ Eq (α := Y ⟶ Y)
    (ofHom P
          {
            toFun :=
              (⇑E.symm :
                (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
            continuous_toFun := hE } ≫
        f :
      Y ⟶ Y)
    (𝟙 Y : Y ⟶ Y)

Tactic:
ext x
-- 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
hE :
  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)
x : (↑(Y.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)) (X := Y)
              (ofHom P
                    {
                      toFun :=
                        (⇑E.symm :
                          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
                      continuous_toFun := hE } ≫
                  f :
                Y ⟶ Y) :
            C((↑(Y.toTop (P := P)) : Type u), (↑(Y.toTop (P := P)) : Type u))) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑(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)) (𝟙 Y) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑(Y.toTop (P := P)) : Type u))

Tactic:
apply E.apply_symm_apply

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : HasProp P X
A B : CompHausLike P
f : A ⟶ B
hf :
  IsIso (X :=
    Functor.obj
      (forget (CompHausLike P) (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)))
      A)
    (CategoryTheory.Functor.map
      (forget (CompHausLike P) (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)
⊢ Function.Bijective (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (forget (CompHausLike P) (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)))
        A))
    (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (forget (CompHausLike P) (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)))
        B))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget (CompHausLike P) (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 : Type u) ↦ X) ((forget (CompHausLike P)).obj A)) →
        (fun (X : Type u) ↦ X) ((forget (CompHausLike P)).obj B))

Tactic:
rw [isIso_iff_bijective] at hf

Premises used: CategoryTheory.isIso_iff_bijective
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : HasProp P X
A B : CompHausLike P
f : A ⟶ B
hf :
  Function.Bijective (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (forget (CompHausLike P) (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)))
        A))
    (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (forget (CompHausLike P) (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)))
        B))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget (CompHausLike P) (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 : Type u) ↦ X) ((forget (CompHausLike P)).obj A)) →
        (fun (X : Type u) ↦ X) ((forget (CompHausLike P)).obj B))
⊢ IsIso f

Tactic:
isIso_of_bijective _ hf

Premises used: CompHausLike.isIso_of_bijective
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : HasProp P X
A B : CompHausLike P
f : A ⟶ B
hf :
  Function.Bijective (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (forget (CompHausLike P) (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)))
        A))
    (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (forget (CompHausLike P) (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)))
        B))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget (CompHausLike P) (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 : Type u) ↦ X) ((forget (CompHausLike P)).obj A)) →
        (fun (X : Type u) ↦ X) ((forget (CompHausLike P)).obj B))
⊢ IsIso f

Tactic:
exact isIso_of_bijective _ hf

Premises used: CompHausLike.isIso_of_bijective
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
S T U : CompHausLike P
s : (↑(S.toTop (P := P)) : Type u)
g : S ⟶ U
⊢ T.const (P := P) s ≫ g =
    T.const (P := P)
      ((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 :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) S) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) U)
        s)

Tactic:
rfl

Premises used: CategoryTheory.InducedCategory.homMk, CompHausLike.const, ContinuousMap.comp, ContinuousMap.const, rfl
-- Module: Mathlib.Topology.Category.CompHausLike.Cartesian
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
inst : HasProp P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u))
refine :
  ∀ (x : BinaryFan X Y) (x_1 : x.pt ⟶ of P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)))
    (h₁ : x_1 ≫ ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ } = x.fst)
    (h₂ : x_1 ≫ ofHom P { toFun := Prod.snd, continuous_toFun := ⋯ } = x.snd),
    x_1 =
      (fun (s : BinaryFan X Y) ↦
          (ofHom P
              {
                toFun := fun (x : (↑s.1.1 : 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)) s.fst :
                        (a :
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                              (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left })) →
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) ((pair X Y).obj { as := WalkingPair.left }))
                      x,
                    (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)) s.snd :
                        (a :
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                              (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right })) →
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) ((pair X Y).obj { as := WalkingPair.right }))
                      x),
                continuous_toFun := ⋯ } :
            of P (↑s.1.1 : Type u) ⟶ of P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u))))
        x
⊢ IsLimit (X.productCone (P := P) Y)

Tactic:
refine BinaryFan.isLimitMk (fun s ↦ ofHom _ { toFun x := (s.fst x, s.snd x) })
    (by rfl_cat) (by rfl_cat) fun _ _ h₁ h₂ ↦ ?_

Premises used: CategoryTheory.Limits.BinaryFan.isLimitMk, CompHausLike.ofHom, CategoryTheory.Limits.BinaryFan.fst, CategoryTheory.ConcreteCategory.hom, ContinuousMap.mk, Prod.mk, CategoryTheory.Limits.BinaryFan.snd, DFunLike.coe