awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
⊢ PreservesLimitsOfShape ℕᵒᵖ
    (forget LightProfinite (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)))

Tactic:
have : PreservesLimitsOfSize.{0, 0} (forget Profinite.{u}) := preservesLimitsOfSize_shrink _
  inferInstanceAs (PreservesLimitsOfShape ℕᵒᵖ (lightToProfinite ⋙ forget Profinite))

Premises used: CategoryTheory.Limits.preservesLimitsOfSize_shrink, Profinite, CategoryTheory.forget, _private.0.LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology._proof_1
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightProfinite
f : X ⟶ Y
⊢ IsClosedMap (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))
      X)
    (Y :=
    (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:
CompHausLike.isClosedMap _

Premises used: CompHausLike.isClosedMap
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightProfinite
f : X ⟶ Y
bij :
  Function.Bijective (α :=
    (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)
⊢ IsIso f

Tactic:
haveI := CompHausLike.isIso_of_bijective (lightProfiniteToCompHaus.map f) bij
  isIso_of_fully_faithful lightProfiniteToCompHaus _

Premises used: CategoryTheory.isIso_of_fully_faithful, lightProfiniteToCompHaus
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
X Y : LightProfinite
f : X ⟶ Y
⊢ Epi (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))
        X)
      (Y :=
      (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)) →
    Epi f

Tactic:
apply (forget LightProfinite).epi_of_epi_map

Premises used: CategoryTheory.forget, CategoryTheory.Functor.epi_of_epi_map, LightProfinite
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
⊢ lightDiagramToProfinite.Faithful

Tactic:
show (inducedFunctor _).Faithful from inferInstance

Premises used: inferInstance, CategoryTheory.InducedCategory, lightDiagramToProfinite
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
⊢ lightDiagramToProfinite.Full

Tactic:
show (inducedFunctor _).Full from inferInstance

Premises used: inferInstance, CategoryTheory.InducedCategory, lightDiagramToProfinite
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightProfinite
rw :
  SecondCountableTopology.{u_1}
    (↑(S.toTop (P := fun (X : TopCat.{u_1}) ↦
          TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
      Type u_1)
⊢ Countable.{u_1 + 1}
    (Clopens
      (↑(S.toTop (P := fun (X : TopCat.{u_1}) ↦
            TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
        Type u_1))

Tactic:
rw [TopologicalSpace.Clopens.countable_iff_secondCountable]

Premises used: TopologicalSpace.Clopens.countable_iff_secondCountable
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightProfinite
⊢ SecondCountableTopology.{u_1}
    (↑(S.toTop (P := fun (X : TopCat.{u_1}) ↦
          TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
      Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightProfinite
⊢ Countable.{u_1 + 1}
    (DiscreteQuotient
      (↑((lightToProfinite.obj S).toTop (P := fun (X : TopCat.{u_1}) ↦
            TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
        Type u_1))

Tactic:
(DiscreteQuotient.finsetClopens_inj S).countable

Premises used: Function.Injective.countable, DiscreteQuotient.finsetClopens_inj, TopCat.carrier, CompHausLike.toTop
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
rw :
  Countable.{u + 1}
    (Clopens (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
⊢ SecondCountableTopology.{u}
    (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)

Tactic:
rw [← TopologicalSpace.Clopens.countable_iff_secondCountable]

Premises used: TopologicalSpace.Clopens.countable_iff_secondCountable
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
⊢ Countable.{u + 1}
    (Clopens (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))

Tactic:
@Countable.of_equiv _ _ ?_ (LocallyConstant.equivClopens (X := S.cone.pt))

Premises used: Countable.of_equiv, LightDiagram.cone, CategoryTheory.Limits.Cone.pt, TopCat.carrier, LocallyConstant.equivClopens, CompHausLike.toTop
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
refine :
  Countable.{u + 1}
    (LocallyConstant
      (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) (Fin 2))
⊢ Countable.{u + 1}
    (Clopens (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))

Tactic:
refine @Countable.of_equiv _ _ ?_ (LocallyConstant.equivClopens (X := S.cone.pt))

Premises used: Countable.of_equiv, LightDiagram.cone, CategoryTheory.Limits.Cone.pt, TopCat.carrier, LocallyConstant.equivClopens, CompHausLike.toTop
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
⊢ Countable.{u + 1}
    (LocallyConstant
      (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) (Fin 2))

Tactic:
@Function.Surjective.countable
    (Σ (n : ℕ), LocallyConstant ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩) (Fin 2)) _ ?_ ?_ ?_

Premises used: Function.Surjective.countable
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
refine_1 :
  Countable.{max (u + 1) 1}
    ((n : ℕ) ×
      LocallyConstant
        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (Fin 2))
refine_2 :
  (n : ℕ) ×
      LocallyConstant
        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (Fin 2) →
    LocallyConstant
      (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) (Fin 2)
refine_3 :
  Function.Surjective (β :=
    LocallyConstant
      (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) (Fin 2))
    fun
      (a :
        (n : ℕ) ×
          LocallyConstant
            (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u)
            (Fin 2)) ↦
    LocallyConstant.comap
      (TopCat.Hom.hom
        (InducedCategory.Hom.hom
          (S.cone.π.app
            (op
              (a.fst (β := fun (n : ℕ) ↦
                LocallyConstant
                  (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)
                  (Fin 2)))))))
      (a.snd (β := fun (n : ℕ) ↦
        LocallyConstant
          (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u))) :
            Type u)
          (Fin 2)))
⊢ Countable.{u + 1}
    (LocallyConstant
      (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) (Fin 2))

Tactic:
refine @Function.Surjective.countable
    (Σ (n : ℕ), LocallyConstant ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩) (Fin 2)) _ ?_ ?_ ?_

Premises used: Function.Surjective.countable
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
apply :
  ∀ (a : ℕ),
    Countable.{u + 1}
      (LocallyConstant
        (↑(((S.diagram ⋙ toProfinite).obj (op a)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (Fin 2))
⊢ Countable.{max (u + 1) 1}
    ((n : ℕ) ×
      LocallyConstant
        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (Fin 2))

Tactic:
apply @instCountableSigma _ _ _ ?_

Premises used: instCountableSigma
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
n : ℕ
⊢ Countable.{u + 1}
    (LocallyConstant
      (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      (Fin 2))

Tactic:
@Finite.to_countable _ ?_

Premises used: Finite.to_countable
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
n : ℕ
refine :
  Finite.{u + 1}
    (LocallyConstant
      (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      (Fin 2))
⊢ Countable.{u + 1}
    (LocallyConstant
      (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      (Fin 2))

Tactic:
refine @Finite.to_countable _ ?_

Premises used: Finite.to_countable
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
n : ℕ
⊢ Finite.{u + 1}
    (LocallyConstant
      (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      (Fin 2))

Tactic:
@Finite.of_injective _ ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩ → (Fin 2)) ?_ _
      LocallyConstant.coe_injective

Premises used: LocallyConstant.coe_injective, Finite.of_injective
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
n : ℕ
refine :
  Finite.{u + 1}
    ((↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u) →
      Fin 2)
⊢ Finite.{u + 1}
    (LocallyConstant
      (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      (Fin 2))

Tactic:
refine @Finite.of_injective _ ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩ → (Fin 2)) ?_ _
      LocallyConstant.coe_injective

Premises used: LocallyConstant.coe_injective, Finite.of_injective
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
n : ℕ
⊢ Finite.{u + 1}
    ((↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u) →
      Fin 2)

Tactic:
@Pi.finite _ _ ?_ _

Premises used: Pi.finite
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
n : ℕ
refine :
  Finite.{u + 1}
    (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
⊢ Finite.{u + 1}
    ((↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u) →
      Fin 2)

Tactic:
refine @Pi.finite _ _ ?_ _

Premises used: Pi.finite
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
n : ℕ
⊢ Finite.{u + 1}
    (↑((toProfinite.obj (S.diagram.obj (op n))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)

Tactic:
show (Finite (S.diagram.obj _)) from inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
n : ℕ
⊢ Finite.{u + 1}
    (↑((toProfinite.obj (S.diagram.obj (op n))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)

Tactic:
exact show (Finite (S.diagram.obj _)) from inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
⊢ (n : ℕ) ×
      LocallyConstant
        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (Fin 2) →
    LocallyConstant
      (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) (Fin 2)

Tactic:
exact fun a ↦ a.snd.comap (S.cone.π.app ⟨a.fst⟩).hom.hom
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
a :
  LocallyConstant (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
    (Fin 2)
n : ℕᵒᵖ
g :
  LocallyConstant
    (↑(((S.diagram ⋙ toProfinite).obj n).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    (Fin 2)
h : a = LocallyConstant.comap (TopCat.Hom.hom (S.cone.π.app n).hom) g
⊢ ∃ (a_1 :
    (n : ℕ) ×
      LocallyConstant
        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (Fin 2)),
    (fun
            (a :
              (n : ℕ) ×
                LocallyConstant
                  (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)
                  (Fin 2)) ↦
          LocallyConstant.comap
            (TopCat.Hom.hom
              (InducedCategory.Hom.hom
                (S.cone.π.app
                  (op
                    (a.fst (β := fun (n : ℕ) ↦
                      LocallyConstant
                        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                          Type u)
                        (Fin 2)))))))
            (a.snd (β := fun (n : ℕ) ↦
              LocallyConstant
                (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)
                (Fin 2))))
        a_1 =
      a

Tactic:
⟨⟨unop n, g⟩, h.symm⟩

Premises used: Exists.intro, Sigma.mk, Eq.symm, Opposite.unop
-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
a :
  LocallyConstant (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
    (Fin 2)
n : ℕᵒᵖ
g :
  LocallyConstant
    (↑(((S.diagram ⋙ toProfinite).obj n).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    (Fin 2)
h : a = LocallyConstant.comap (TopCat.Hom.hom (S.cone.π.app n).hom) g
⊢ ∃ (a_1 :
    (n : ℕ) ×
      LocallyConstant
        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (Fin 2)),
    (fun
            (a :
              (n : ℕ) ×
                LocallyConstant
                  (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)
                  (Fin 2)) ↦
          LocallyConstant.comap
            (TopCat.Hom.hom
              (InducedCategory.Hom.hom
                (S.cone.π.app
                  (op
                    (a.fst (β := fun (n : ℕ) ↦
                      LocallyConstant
                        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                          Type u)
                        (Fin 2)))))))
            (a.snd (β := fun (n : ℕ) ↦
              LocallyConstant
                (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)
                (Fin 2))))
        a_1 =
      a

Tactic:
exact ⟨⟨unop n, g⟩, h.symm⟩