awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ LightProfinite
⊢ TotallyDisconnectedSpace
    (↑((CompHaus.limitCone.{v, u} (F ⋙ lightProfiniteToCompHaus)).pt.toTop (P := fun (x : TopCat) ↦ True)) :
      Type (max u v))
have change : TotallyDisconnectedSpace
  (↑{u :
        (j : J) →
          (↑((F.obj j).toTop (P := fun (X : TopCat) ↦
                TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
            Type (max u v)) |
        ∀ {i j : J} (f : i ⟶ j),
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                  TopCat.carrier) (((F ⋙ lightProfiniteToCompHaus) ⋙ compHausToTop).map f) :
                (a : (↑(((F ⋙ lightProfiniteToCompHaus) ⋙ compHausToTop).obj i) : Type (max u v))) →
                  (↑(((F ⋙ lightProfiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v)))
              (u i) =
            u j} :
    Type (max u v))
Tactic: change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type _)
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : CountableCategory J
F : J ⥤ LightProfinite
S : Cone F
x : S.pt ⟶ (limitCone.{v, u} F).pt
h : ∀ (j : J), x ≫ (limitCone.{v, u} F).π.app j = S.π.app j
⊢ x =
    ConcreteCategory.ofHom (FC :=
      fun
        (x1 x2 :
          CompHausLike fun (X : TopCat) ↦
            TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v))) ↦
      C((↑(x1.toTop (P := fun (X : TopCat) ↦
              TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
          Type (max u v)),
        (↑(x2.toTop (P := fun (X : TopCat) ↦
              TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
          Type (max u v))))
      (CC :=
      fun
        (X :
          CompHausLike fun (X : TopCat) ↦
            TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v))) ↦
      (↑(X.toTop (P := fun (X : TopCat) ↦
            TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
        Type (max u v)))
      (TopCat.Hom.hom
        (InducedCategory.Hom.hom
          ((CompHaus.limitConeIsLimit (F ⋙ lightProfiniteToCompHaus)).lift (lightProfiniteToCompHaus.mapCone S))))
have a : lightProfiniteToCompHaus.map x =
  lightProfiniteToCompHaus.map
    (ConcreteCategory.ofHom (FC :=
      fun
        (x1 x2 :
          CompHausLike fun (X : TopCat) ↦
            TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v))) ↦
      C((↑(x1.toTop (P := fun (X : TopCat) ↦
              TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
          Type (max u v)),
        (↑(x2.toTop (P := fun (X : TopCat) ↦
              TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
          Type (max u v))))
      (CC :=
      fun
        (X :
          CompHausLike fun (X : TopCat) ↦
            TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v))) ↦
      (↑(X.toTop (P := fun (X : TopCat) ↦
            TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
        Type (max u v)))
      (TopCat.Hom.hom
        (InducedCategory.Hom.hom
          ((CompHaus.limitConeIsLimit (F ⋙ lightProfiniteToCompHaus)).lift (lightProfiniteToCompHaus.mapCone S)))))
Tactic: apply lightProfiniteToCompHaus.map_injective
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : CountableCategory J
F : J ⥤ LightProfinite
S : Cone F
x : S.pt ⟶ (limitCone.{v, u} F).pt
h : ∀ (j : J), x ≫ (limitCone.{v, u} F).π.app j = S.π.app j
⊢ lightProfiniteToCompHaus.map x =
    lightProfiniteToCompHaus.map
      (ConcreteCategory.ofHom (FC :=
        fun
          (x1 x2 :
            CompHausLike fun (X : TopCat) ↦
              TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v))) ↦
        C((↑(x1.toTop (P := fun (X : TopCat) ↦
                TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
            Type (max u v)),
          (↑(x2.toTop (P := fun (X : TopCat) ↦
                TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
            Type (max u v))))
        (CC :=
        fun
          (X :
            CompHausLike fun (X : TopCat) ↦
              TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v))) ↦
        (↑(X.toTop (P := fun (X : TopCat) ↦
              TotallyDisconnectedSpace (↑X : Type (max u v)) ∧ SecondCountableTopology (↑X : Type (max u v)))) :
          Type (max u v)))
        (TopCat.Hom.hom
          (InducedCategory.Hom.hom
            ((CompHaus.limitConeIsLimit (F ⋙ lightProfiniteToCompHaus)).lift (lightProfiniteToCompHaus.mapCone S)))))
have a : ∀ (j : J),
  lightProfiniteToCompHaus.map x ≫ (CompHaus.limitCone.{v, u} (F ⋙ lightProfiniteToCompHaus)).π.app j =
    (lightProfiniteToCompHaus.mapCone S).π.app j
Tactic: apply (CompHaus.limitConeIsLimit.{v, u} _).uniq (lightProfiniteToCompHaus.mapCone S)
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : CountableCategory J
F : J ⥤ LightProfinite
S : Cone F
x : S.pt ⟶ (limitCone.{v, u} F).pt
h : ∀ (j : J), x ≫ (limitCone.{v, u} F).π.app j = S.π.app j
j : J
⊢ lightProfiniteToCompHaus.map x ≫ (CompHaus.limitCone.{v, u} (F ⋙ lightProfiniteToCompHaus)).π.app j =
    (lightProfiniteToCompHaus.mapCone S).π.app j
have a : Eq (α := lightProfiniteToCompHaus.obj S.pt ⟶ lightProfiniteToCompHaus.obj (F.obj j))
  (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
      C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
        (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
      (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
      (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (TopCat.Hom.hom x.hom) ≫
    (CompHaus.limitCone.{v, u} (F ⋙ lightProfiniteToCompHaus)).π.app j)
  (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    (TopCat.Hom.hom (x ≫ (limitCone.{v, u} F).π.app j).hom))
Tactic: simp [← h]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
S : LightProfinite
⊢ 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))
have 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)
Tactic: rw [TopologicalSpace.Clopens.countable_iff_secondCountable]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
S : LightDiagram
⊢ SecondCountableTopology.{u}
    (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
have rw : Countable.{u + 1}
  (Clopens (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
Tactic: rw [← TopologicalSpace.Clopens.countable_iff_secondCountable]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
S : LightDiagram
⊢ Countable.{u + 1}
    (Clopens (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
have refine : Countable.{u + 1}
  (LocallyConstant
    (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) (Fin 2))
Tactic: refine @Countable.of_equiv _ _ ?_ (LocallyConstant.equivClopens (X := S.cone.pt))
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
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))
have 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))
Tactic: refine @Function.Surjective.countable
    (Σ (n : ℕ), LocallyConstant ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩) (Fin 2)) _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
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))
⊢ Countable.{u + 1}
    (LocallyConstant
      (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) (Fin 2))
have 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)
Tactic: refine @Function.Surjective.countable
    (Σ (n : ℕ), LocallyConstant ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩) (Fin 2)) _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
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)
⊢ Countable.{u + 1}
    (LocallyConstant
      (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) (Fin 2))
have 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)))
Tactic: refine @Function.Surjective.countable
    (Σ (n : ℕ), LocallyConstant ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩) (Fin 2)) _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
S : LightDiagram
⊢ 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))
have 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))
Tactic: apply @instCountableSigma _ _ _ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
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))
have 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))
Tactic: refine @Finite.to_countable _ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
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))
have 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)
Tactic: refine @Finite.of_injective _ ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩ → (Fin 2)) ?_ _
      LocallyConstant.coe_injective
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
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)
have refine : Finite.{u + 1}
  (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
Tactic: refine @Pi.finite _ _ ?_ _
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
X Y : LightDiagram
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)
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
X Y : LightDiagram
f : X ⟶ Y
⊢ 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
have 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)
Tactic: apply lightDiagramToProfinite.map_injective
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
X Y : LightDiagram
f : X ⟶ Y
⊢ 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)
have 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
Tactic: apply InducedCategory.hom_ext
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
X Y : LightDiagram
f : X ⟶ Y
⊢ (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
have 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
Tactic: simp only [Functor.map_comp, Functor.map_preimage]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
X Y : LightDiagram'
a₁ a₂ : X ⟶ Y
h : LightDiagram'.toLightFunctor.map a₁ = LightDiagram'.toLightFunctor.map a₂
⊢ a₁ = a₂
have 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.injective
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.EffectiveEpi (goal)
Goal:
X Y : LightProfinite
f : X ⟶ Y
h : 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)
have rw : Epi f
Tactic: rw [← epi_iff_surjective]