awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X : LightDiagram
_ :
  ∀ {Y : LightDiagram.{u}} (f : X ⟶ Y),
    Eq (α := (lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj X ⟶ Functor.obj (𝟭 LightDiagram) Y)
      ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).map f ≫
        Iso.hom
          ((fun (x : LightDiagram.{u}) ↦
              lightDiagramToProfinite.preimageIso
                (Iso.refl
                  (lightDiagramToProfinite.obj ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj x))))
            Y))
      (Iso.hom
          ((fun (x : LightDiagram.{u}) ↦
              lightDiagramToProfinite.preimageIso
                (Iso.refl
                  (lightDiagramToProfinite.obj ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj x))))
            X) ≫
        CategoryTheory.Functor.map (𝟭 LightDiagram) f)
⊢ ∀ {Y : LightDiagram.{u}} (f : X ⟶ Y),
    Eq (α := (lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj X ⟶ Functor.obj (𝟭 LightDiagram) Y)
      ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).map f ≫
        Iso.hom
          ((fun (x : LightDiagram.{u}) ↦
              lightDiagramToProfinite.preimageIso
                (Iso.refl
                  (lightDiagramToProfinite.obj ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj x))))
            Y))
      (Iso.hom
          ((fun (x : LightDiagram.{u}) ↦
              lightDiagramToProfinite.preimageIso
                (Iso.refl
                  (lightDiagramToProfinite.obj ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj x))))
            X) ≫
        CategoryTheory.Functor.map (𝟭 LightDiagram) f)

Tactic:
_
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightDiagram
f : X ⟶ Y
dsimp :
  InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
      lightDiagramToProfinite.preimage
        (𝟙
          (of
                (↑(Y.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)).toLightDiagram.toProfinite) =
    lightDiagramToProfinite.preimage
        (𝟙
          (of
                (↑(X.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)).toLightDiagram.toProfinite) ≫
      f
⊢ Eq (α := (lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj X ⟶ Functor.obj (𝟭 LightDiagram) Y)
    ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).map f ≫
      Iso.hom
        ((fun (x : LightDiagram.{u}) ↦
            lightDiagramToProfinite.preimageIso
              (Iso.refl
                (lightDiagramToProfinite.obj ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj x))))
          Y))
    (Iso.hom
        ((fun (x : LightDiagram.{u}) ↦
            lightDiagramToProfinite.preimageIso
              (Iso.refl
                (lightDiagramToProfinite.obj ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj x))))
          X) ≫
      CategoryTheory.Functor.map (𝟭 LightDiagram) f)

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightDiagram
f : X ⟶ Y
a :
  lightDiagramToProfinite.map
      (InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
        lightDiagramToProfinite.preimage
          (𝟙
            (of
                  (↑(Y.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)).toLightDiagram.toProfinite)) =
    lightDiagramToProfinite.map
      (lightDiagramToProfinite.preimage
          (𝟙
            (of
                  (↑(X.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)).toLightDiagram.toProfinite) ≫
        f)
⊢ InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
      lightDiagramToProfinite.preimage
        (𝟙
          (of
                (↑(Y.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)).toLightDiagram.toProfinite) =
    lightDiagramToProfinite.preimage
        (𝟙
          (of
                (↑(X.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)).toLightDiagram.toProfinite) ≫
      f

Tactic:
apply lightDiagramToProfinite.map_injective

Premises used: CategoryTheory.Functor.map_injective, lightDiagramToProfinite
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightDiagram
f : X ⟶ Y
a :
  (lightDiagramToProfinite.map
        (InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
          lightDiagramToProfinite.preimage
            (𝟙
              (of
                    (↑(Y.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                      Type u)).toLightDiagram.toProfinite))).hom =
    (lightDiagramToProfinite.map
        (lightDiagramToProfinite.preimage
            (𝟙
              (of
                    (↑(X.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                      Type u)).toLightDiagram.toProfinite) ≫
          f)).hom
⊢ lightDiagramToProfinite.map
      (InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
        lightDiagramToProfinite.preimage
          (𝟙
            (of
                  (↑(Y.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)).toLightDiagram.toProfinite)) =
    lightDiagramToProfinite.map
      (lightDiagramToProfinite.preimage
          (𝟙
            (of
                  (↑(X.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)).toLightDiagram.toProfinite) ≫
        f)

Tactic:
apply InducedCategory.hom_ext

Premises used: CategoryTheory.InducedCategory.hom_ext
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightDiagram
f : X ⟶ Y
a :
  (lightDiagramToProfinite.map (InducedCategory.homMk (InducedCategory.homMk f.hom.hom)) ≫
        𝟙
          (of
                (↑(Y.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)).toLightDiagram.toProfinite).hom =
    (𝟙
          (of
                (↑(X.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)).toLightDiagram.toProfinite ≫
        lightDiagramToProfinite.map f).hom
⊢ (lightDiagramToProfinite.map
        (InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
          lightDiagramToProfinite.preimage
            (𝟙
              (of
                    (↑(Y.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                      Type u)).toLightDiagram.toProfinite))).hom =
    (lightDiagramToProfinite.map
        (lightDiagramToProfinite.preimage
            (𝟙
              (of
                    (↑(X.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                      Type u)).toLightDiagram.toProfinite) ≫
          f)).hom

Tactic:
simp only [Functor.map_comp, Functor.map_preimage]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightDiagram
f : X ⟶ Y
⊢ (lightDiagramToProfinite.map (InducedCategory.homMk (InducedCategory.homMk f.hom.hom)) ≫
        𝟙
          (of
                (↑(Y.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)).toLightDiagram.toProfinite).hom =
    (𝟙
          (of
                (↑(X.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)).toLightDiagram.toProfinite ≫
        lightDiagramToProfinite.map f).hom

Tactic:
simp
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
x : LightProfinite
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simpa using lightDiagramToProfinite.preimage_id

Premises used: CategoryTheory.Functor.preimage_id
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
⊢ lightProfiniteToLightDiagram.IsEquivalence

Tactic:
show LightProfinite.equivDiagram.functor.IsEquivalence from inferInstance

Premises used: lightProfiniteToLightDiagram, inferInstance
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
⊢ lightDiagramToLightProfinite.IsEquivalence

Tactic:
show LightProfinite.equivDiagram.inverse.IsEquivalence from inferInstance

Premises used: inferInstance, lightDiagramToLightProfinite
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightDiagram'
a₁ a₂ : X ⟶ Y
h : LightDiagram'.toLightFunctor.map a₁ = LightDiagram'.toLightFunctor.map a₂
a :
  Eq (α := X.toProfinite ⟶ Y.toProfinite)
    ((InducedCategory.homEquiv : (a : X ⟶ Y) → X.toProfinite ⟶ Y.toProfinite) a₁ : X.toProfinite ⟶ Y.toProfinite)
    ((InducedCategory.homEquiv : (a : X ⟶ Y) → X.toProfinite ⟶ Y.toProfinite) a₂ : X.toProfinite ⟶ Y.toProfinite)
⊢ a₁ = a₂

Tactic:
apply InducedCategory.homEquiv.injective

Premises used: CategoryTheory.InducedCategory.homEquiv, Equiv.injective
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightDiagram'
a₁ a₂ : X ⟶ Y
h : LightDiagram'.toLightFunctor.map a₁ = LightDiagram'.toLightFunctor.map a₂
⊢ Eq (α := X.toProfinite ⟶ Y.toProfinite)
    ((InducedCategory.homEquiv : (a : X ⟶ Y) → X.toProfinite ⟶ Y.toProfinite) a₁ : X.toProfinite ⟶ Y.toProfinite)
    ((InducedCategory.homEquiv : (a : X ⟶ Y) → X.toProfinite ⟶ Y.toProfinite) a₂ : X.toProfinite ⟶ Y.toProfinite)

Tactic:
apply InducedCategory.homEquiv.symm.injective h

Premises used: CategoryTheory.InducedCategory.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi
Goal:
X Y : LightProfinite
f : X ⟶ Y
⊢ EffectiveEpi f ↔
    Function.Surjective (α :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        X)
      (β :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        Y)
      (⇑(ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
            f) :
        (a :
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              X) →
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            Y)

Tactic:
⟨fun h ↦ ?_, fun h ↦ ⟨⟨effectiveEpiStruct f h⟩⟩⟩

Premises used: Nonempty.intro, Iff.intro, CompHausLike.effectiveEpiStruct, CategoryTheory.EffectiveEpi.mk
-- Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi
Goal:
X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
rw : Epi f
⊢ Function.Surjective (α :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
      X)
    (β :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
      Y)
    (⇑(ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u)))
          (CC :=
          fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          f) :
      (a :
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            X) →
        (fun
              (X :
                CompHausLike fun (X : TopCat) ↦
                  TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
            (↑X.toTop : Type u))
          Y)

Tactic:
rw [← epi_iff_surjective]

Premises used: LightProfinite.epi_iff_surjective
-- Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi
Goal:
X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
⊢ Epi f

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi
Goal:
hs :
  ∀
    ⦃X Y :
      CompHausLike fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)⦄
    (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α :=
        (fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
          X)
        (β :=
        (fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
          Y)
        (⇑(ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  CompHausLike fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                  Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                  Type u)))
              (CC :=
              fun
                (X :
                  CompHausLike fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u))
              f) :
          (a :
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                  (↑X.toTop : Type u))
                X) →
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              Y)
⊢ Preregular LightProfinite

Tactic:
apply CompHausLike.preregular

Premises used: CompHausLike.preregular
-- Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi
Goal:
X Y :
  CompHausLike fun (X : TopCat.{u}) ↦
    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)
f : X ⟶ Y
⊢ EffectiveEpi f →
    Function.Surjective (α :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        X)
      (β :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        Y)
      (⇑(ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
            f) :
        (a :
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              X) →
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            Y)

Tactic:
(effectiveEpi_iff_surjective f).mp

Premises used: LightProfinite.effectiveEpi_iff_surjective, Iff.mp
-- Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi
Goal:
X Y :
  CompHausLike fun (X : TopCat.{u}) ↦
    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)
f : X ⟶ Y
⊢ EffectiveEpi f →
    Function.Surjective (α :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        X)
      (β :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        Y)
      (⇑(ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
            f) :
        (a :
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              X) →
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            Y)

Tactic:
exact (effectiveEpi_iff_surjective f).mp

Premises used: LightProfinite.effectiveEpi_iff_surjective, Iff.mp
-- Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi
Goal:
⊢ Precoherent LightProfinite

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
⊢ functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite =
    Profinite.Extend.functor (lightToProfinite.mapCone c)

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Functor.comp, FintypeCat.toProfinite, CategoryTheory.StructuredArrow.mk, rfl, Profinite.Extend.functor
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
rw : (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial
⊢ (functor c).Initial

Tactic:
rw [initial_iff_comp_equivalence _ (StructuredArrow.post _ _ lightToProfinite)]

Premises used: CategoryTheory.Functor.initial_iff_comp_equivalence, lightToProfinite, CategoryTheory.StructuredArrow.post