awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.CompHaus.Frm
Goal:
⊢ (compHausToTop.op ⋙ topCatOpToFrm).Faithful

Tactic:
⟨fun {X _ _ _} h =>  Quiver.Hom.unop_inj <| ConcreteCategory.ext <|
    Opens.comap_injective (β := (unop X).toTop) <| FrameHom.ext <|
      CategoryTheory.congr_fun h⟩

Premises used: FrameHom.ext, CategoryTheory.congr_fun, CategoryTheory.ConcreteCategory.ext, CategoryTheory.Functor.Faithful.mk, Quiver.Hom.unop_inj, TopologicalSpace.Opens.comap_injective
-- Module: Mathlib.Topology.Category.CompHaus.Limits
Goal:
⊢ FinitaryExtensive CompHaus

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.CompHaus.Limits
Goal:
⊢ PreservesFiniteCoproducts compHausToTop

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.CompHaus.Projective
Goal:
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Epi g
⊢ Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)

Tactic:
rw [epi_iff_surjective] at hg

Premises used: CompHaus.epi_iff_surjective
-- Module: Mathlib.Topology.Category.CompHaus.Projective
Goal:
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg :
  Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
obtain :
  ∀
    (g' :
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
          Z →
        (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
          Y)
    (hg' :
      RightInverse g'
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
                (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
              (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)),
    ∃ (f' : of (Ultrafilter X) ⟶ Y), f' ≫ g = f
⊢ ∃ (f' : of (Ultrafilter X) ⟶ Y), f' ≫ g = f

Tactic:
obtain ⟨g', hg'⟩ := hg.hasRightInverse

Premises used: Function.Surjective.hasRightInverse
-- Module: Mathlib.Topology.Category.CompHaus.Projective
Goal:
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg :
  Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
g' :
  (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z →
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y
hg' :
  RightInverse g'
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
t : X → (↑(Y.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) :=
  g' ∘
    comp (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
        (of (Ultrafilter X)))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
              (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) (of (Ultrafilter X))) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
      pure
h : Ultrafilter X → (↑(Y.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) := Ultrafilter.extend t
⊢ Continuous h

Tactic:
have hh : Continuous h := continuous_ultrafilter_extend _
-- Module: Mathlib.Topology.Category.CompHaus.Projective
Goal:
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg :
  Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
g' :
  (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z →
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y
hg' :
  RightInverse g'
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
t : X → (↑(Y.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) :=
  g' ∘
    comp (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
        (of (Ultrafilter X)))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
              (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) (of (Ultrafilter X))) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
      pure
h : Ultrafilter X → (↑(Y.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) := Ultrafilter.extend t
hh : Continuous h
h₁ : CompHausLike.ofHom (fun (x : TopCat.{u_1}) ↦ True) { toFun := h, continuous_toFun := hh } ≫ g = f
⊢ ∃ (f' : of (Ultrafilter X) ⟶ Y), f' ≫ g = f

Tactic:
use CompHausLike.ofHom _ ⟨h, hh⟩

Premises used: CompHausLike.ofHom, ContinuousMap.mk
-- Module: Mathlib.Topology.Category.CompHaus.Projective
Goal:
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg :
  Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
g' :
  (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z →
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y
hg' :
  RightInverse g'
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
t : X → (↑(Y.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) :=
  g' ∘
    comp (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
        (of (Ultrafilter X)))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
              (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) (of (Ultrafilter X))) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
      pure
h : Ultrafilter X → (↑(Y.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) := Ultrafilter.extend t
hh : Continuous h
⊢ (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            g.hom) :
        (a : (↑Y.toTop : Type u_1)) → (↑Z.toTop : Type u_1)) ∘
      g' =
    id

Tactic:
have : g.hom ∘ g' = id := hg'.comp_eq_id
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : CompactSpace X_1
inst_2 : T2Space X_1
X : CompHausLike P
⊢ HasProp P (↑(X.toTop (P := P)) : Type u)

Tactic:
⟨X.4⟩

Premises used: CompHausLike.prop, CompHausLike.HasProp.mk
-- 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
⊢ (↑((of P X).toTop (P := P)) : Type u) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X : CompHausLike P
⊢ Eq (α :=
    (a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) →
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) 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)) (𝟙 X)) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y Z : CompHausLike P
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) →
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Z)
    (⇑(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 ≫ g)) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z)
    (Function.comp (β := (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)) g) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z)
      (⇑(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:
rfl

Premises used: rfl
-- 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
Y : Type u
inst_4 : TopologicalSpace Y
inst_5 : CompactSpace Y
inst_6 : T2Space Y
inst_7 : HasProp P Y
f : C(X, 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)) (X := of P X) (Y := of P Y) (ofHom P f) =
    f

Tactic:
rfl

Premises used: rfl
-- 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
⊢ ofHom P (ContinuousMap.id X) = 𝟙 (of P X)

Tactic:
rfl

Premises used: CategoryTheory.InducedCategory.homMk, rfl
-- 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
Y : Type u
inst_4 : TopologicalSpace Y
inst_5 : CompactSpace Y
inst_6 : T2Space Y
inst_7 : HasProp P Y
Z : Type u
inst_8 : TopologicalSpace Z
inst_9 : CompactSpace Z
inst_10 : T2Space Z
inst_11 : HasProp P Z
f : C(X, Y)
g : C(Y, Z)
⊢ Eq (α := of P X ⟶ of P Z) (ofHom P (g.comp f)) (CategoryStruct.comp (Y := of P Y) (ofHom P f) (ofHom P g))

Tactic:
rfl

Premises used: CategoryTheory.InducedCategory.homMk, rfl
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P_1 : TopCat.{u} → Prop
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : HasProp P_1 X
P P' : TopCat.{u_1} → Prop
h : ∀ (X : CompHausLike P), P (X.toTop (P := P)) → P' (X.toTop (P := P))
⊢ (toCompHausLike (P := P) (P' := P') h).Full

Tactic:
(fullyFaithfulToCompHausLike h).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CompHausLike.fullyFaithfulToCompHausLike
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P_1 : TopCat.{u} → Prop
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : HasProp P_1 X
P P' : TopCat.{u_1} → Prop
h : ∀ (X : CompHausLike P), P (X.toTop (P := P)) → P' (X.toTop (P := P))
⊢ (toCompHausLike (P := P) (P' := P') h).Faithful

Tactic:
(fullyFaithfulToCompHausLike h).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CompHausLike.fullyFaithfulToCompHausLike
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P_1 : TopCat.{u} → Prop
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : HasProp P_1 X
P P' : TopCat.{u_1} → Prop
h : ∀ (X : CompHausLike P), P (X.toTop (P := P)) → P' (X.toTop (P := P))
⊢ toCompHausLike (P := P) (P' := P') h ⋙ compHausLikeToTop P' = compHausLikeToTop P

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.inducedFunctor, CategoryTheory.InducedCategory, CompHausLike.compHausLikeToTop, rfl
-- 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
⊢ (compHausLikeToTop P).Full

Tactic:
inferInstanceAs (inducedFunctor _).Full

Premises used: _private.0.CompHausLike.instFullTopCatCompHausLikeToTop._proof_1
-- 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
⊢ (compHausLikeToTop P).Faithful

Tactic:
inferInstanceAs (inducedFunctor _).Faithful

Premises used: _private.0.CompHausLike.instFaithfulTopCatCompHausLikeToTop._proof_1
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : CompactSpace X_1
inst_2 : T2Space X_1
inst_3 : HasProp P X_1
X : CompHausLike P
⊢ CompactSpace.{u} (↑((compHausLikeToTop P).obj X) : Type u)

Tactic:
inferInstanceAs (CompactSpace X.toTop)

Premises used: _private.0.CompHausLike.instCompactSpaceCarrierObjTopCatCompHausLikeToTop._proof_1
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : CompactSpace X_1
inst_2 : T2Space X_1
inst_3 : HasProp P X_1
X : CompHausLike P
⊢ T2Space.{u} (↑((compHausLikeToTop P).obj X) : Type u)

Tactic:
inferInstanceAs (T2Space X.toTop)

Premises used: _private.0.CompHausLike.instT2SpaceCarrierObjTopCatCompHausLikeToTop._proof_1
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf :
  Function.Surjective (α := (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)
⊢ Epi (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:
rw [← CategoryTheory.ofHom_epi_iff_surjective] at hf

Premises used: CategoryTheory.ofHom_epi_iff_surjective
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf :
  Epi (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))
⊢ Epi f

Tactic:
(forget (CompHausLike P)).epi_of_epi_map hf

Premises used: CompHausLike, CategoryTheory.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.Topology.Category.CompHausLike.Basic
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf :
  Epi (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))
⊢ Epi f

Tactic:
exact (forget (CompHausLike P)).epi_of_epi_map hf

Premises used: CompHausLike, CategoryTheory.forget, CategoryTheory.Functor.epi_of_epi_map