awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.AsLimit
Goal:
X : Profinite
a b :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    X.asLimitCone.pt
h :
  Eq (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (limitCone X.diagram).pt)
    ((ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
            X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X.asLimitCone.pt) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              (limitCone X.diagram).pt)
        a :
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        (limitCone X.diagram).pt)
    ((ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
            X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X.asLimitCone.pt) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              (limitCone X.diagram).pt)
        b :
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        (limitCone X.diagram).pt)
⊢ a = b

Tactic:
DiscreteQuotient.eq_of_forall_proj_eq fun S => ?_

Premises used: DiscreteQuotient.eq_of_forall_proj_eq
-- Module: Mathlib.Topology.Category.Profinite.AsLimit
Goal:
X : Profinite
a b :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    X.asLimitCone.pt
S :
  DiscreteQuotient
    ((fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      X.asLimitCone.pt)
h :
  Eq.{u + 1} (α := (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj S) : Type u))
    ((↑((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
                X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    X.asLimitCone.pt) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (limitCone X.diagram).pt)
            a) :
        (j : DiscreteQuotient (↑X.toTop : Type u)) →
          (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
      S)
    ((↑((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
                X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    X.asLimitCone.pt) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (limitCone X.diagram).pt)
            b) :
        (j : DiscreteQuotient (↑X.toTop : Type u)) →
          (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
      S)
⊢ S.proj a = S.proj b

Tactic:
h

Premises used: DiscreteQuotient.proj, Quotient
-- Module: Mathlib.Topology.Category.Profinite.AsLimit
Goal:
X : Profinite
a b :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    X.asLimitCone.pt
S :
  DiscreteQuotient
    ((fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      X.asLimitCone.pt)
h :
  Eq.{u + 1} (α := (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj S) : Type u))
    ((↑((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
                X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    X.asLimitCone.pt) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (limitCone X.diagram).pt)
            a) :
        (j : DiscreteQuotient (↑X.toTop : Type u)) →
          (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
      S)
    ((↑((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
                X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    X.asLimitCone.pt) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (limitCone X.diagram).pt)
            b) :
        (j : DiscreteQuotient (↑X.toTop : Type u)) →
          (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
      S)
⊢ S.proj a = S.proj b

Tactic:
exact h
-- Module: Mathlib.Topology.Category.Profinite.AsLimit
Goal:
X : Profinite
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone X.diagram).pt
b : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hb :
  ∀
    (Q :
      DiscreteQuotient (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    Q.proj b =
      (↑a :
          (j : DiscreteQuotient (↑X.toTop : Type u)) →
            (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
        Q
h :
  (ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
          X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              X.asLimitCone.pt) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
            (limitCone X.diagram).pt)
      b =
    a
⊢ ∃ (a_1 :
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      X.asLimitCone.pt),
    (ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
            X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X.asLimitCone.pt) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              (limitCone X.diagram).pt)
        a_1 =
      a

Tactic:
use b
-- Module: Mathlib.Topology.Category.Profinite.AsLimit
Goal:
X : Profinite
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone X.diagram).pt
b : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hb :
  ∀
    (Q :
      DiscreteQuotient (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    Q.proj b =
      (↑a :
          (j : DiscreteQuotient (↑X.toTop : Type u)) →
            (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
        Q
h :
  (↑((ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
              X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  X.asLimitCone.pt) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                (limitCone X.diagram).pt)
          b) :
      (j : DiscreteQuotient (↑X.toTop : Type u)) →
        (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) =
    (↑a :
      (j : DiscreteQuotient (↑X.toTop : Type u)) →
        (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
⊢ (ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
          X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              X.asLimitCone.pt) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
            (limitCone X.diagram).pt)
      b =
    a

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Category.Profinite.AsLimit
Goal:
X : Profinite
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone X.diagram).pt
b : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hb :
  ∀
    (Q :
      DiscreteQuotient (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    Q.proj b =
      (↑a :
          (j : DiscreteQuotient (↑X.toTop : Type u)) →
            (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
        Q
S : DiscreteQuotient (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ (↑((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
                X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    X.asLimitCone.pt) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (limitCone X.diagram).pt)
            b) :
        (j : DiscreteQuotient (↑X.toTop : Type u)) →
          (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
      S =
    (↑a :
        (j : DiscreteQuotient (↑X.toTop : Type u)) →
          (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
      S

Tactic:
apply hb
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
⊢ HasProp (fun (Y : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑Y : Type u_1)) X

Tactic:
⟨(inferInstance : TotallyDisconnectedSpace X)⟩

Premises used: inferInstance, CompHausLike.HasProp.mk
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X : Profinite
⊢ TotallyDisconnectedSpace.{u_1}
    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)

Tactic:
X.prop

Premises used: CompHausLike.prop
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X : Profinite
⊢ TotallyDisconnectedSpace.{u_1} (↑((profiniteToCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)

Tactic:
X.prop

Premises used: CompHausLike.prop
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X : CompHaus
Y : Profinite
f : X.toProfiniteObj ⟶ Y
y : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
⊢ Eq (α := (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
            TopCat.carrier _ _
            (X.toProfiniteObj.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)))
            (Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)))
            (InducedCategory.Hom.hom
              ((fun (g : X ⟶ profiniteToCompHaus.obj Y) ↦
                  (ConcreteCategory.ofHom (FC :=
                      fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                      C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                        (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                          Type u)))
                      (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
                      { toFun := ⋯.connectedComponentsLift, continuous_toFun := ⋯ :
                        C((↑(X.toProfiniteObj.toTop (P := fun (X : TopCat.{u}) ↦
                                TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u),
                          (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u)) } :
                    X.toProfiniteObj ⟶ Y))
                ((fun (f : X.toProfiniteObj ⟶ Y) ↦
                    (ofHom (fun (x : TopCat.{u}) ↦ True)
                        ((TopCat.Hom.hom f.hom).comp { toFun := Quotient.mk'', continuous_toFun := ⋯ }) :
                      Quiver.Hom (V := CompHausLike fun (x : TopCat.{u}) ↦ True)
                        (CompHausLike.of (fun (x : TopCat.{u}) ↦ True) (↑X.1 : Type u))
                        (CompHausLike.of (fun (x : TopCat.{u}) ↦ True)
                          (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u))))
                  f))) :
          (a : (↑X.toProfiniteObj.toTop : Type u)) → (↑Y.toTop : Type u))
        (ConnectedComponents.mk y) :
      (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.hom :
          (a : (↑X.toProfiniteObj.toTop : Type u)) → (↑Y.toTop : Type u))
        (ConnectedComponents.mk y) :
      (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X : CompHaus
⊢ (↑((toProfinite.obj X).toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
      Type u_1) =
    ConnectedComponents (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)

Tactic:
rfl

Premises used: Quotient, ConnectedComponents, rfl
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
A : FintypeCat
⊢ DiscreteTopology.{u_1} A.obj

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X Y : FintypeCat
f : X ⟶ Y
⊢ Continuous (X := X.obj) (Y := Y.obj)
    (⇑(@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ f) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
⊢ FintypeCat.toProfinite.Faithful

Tactic:
FintypeCat.toProfiniteFullyFaithful.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, FintypeCat.toProfiniteFullyFaithful
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
⊢ FintypeCat.toProfinite.Full

Tactic:
FintypeCat.toProfiniteFullyFaithful.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, FintypeCat.toProfiniteFullyFaithful
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X : FintypeCat
⊢ Finite.{u_1 + 1}
    (↑((FintypeCat.toProfinite.obj X).toTop (P := fun (X : TopCat.{u_1}) ↦
          TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
      Type u_1)

Tactic:
inferInstanceAs (Finite X)

Premises used: _private.0.instFiniteCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite._proof_1
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X : FintypeCat
⊢ Finite.{u_1 + 1}
    (↑((Profinite.of X.obj).toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
      Type u_1)

Tactic:
inferInstanceAs (Finite X)

Premises used: _private.0.instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj._proof_1