awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F_1 F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X : FintypeCat
⊢ PreservesLimitsOfShape (Discrete X.obj) F

Tactic:
let X' := (Countable.toSmall.{0} X).equiv_small.choose
  let e : X ≃ X' := (Countable.toSmall X).equiv_small.choose_spec.some
  have : Finite X' := Finite.of_equiv X e
  preservesLimitsOfShape_of_equiv (Discrete.equivalence e.symm) F

Premises used: Finite.of_equiv, Exists.choose_spec, Small.equiv_small, Nonempty.some, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.equivalence, Exists.choose, Equiv.symm
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X : LightProfinite
inst_1 :
  Finite.{u + 1}
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
⊢ (isoFinYonedaComponents F X).hom =
    ↾fun (y : (fun (X : Type u) ↦ X) (F.obj (Opposite.op X)))
        (x :
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u)) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  (LightProfinite.of PUnit.{u + 1}) x).op) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op X))) →
            (fun (X : Type u) ↦ X) (F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        y

Tactic:
rfl

Premises used: CompHausLike.const, CategoryTheory.Limits.Cofan.inj, rfl
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X : LightProfinite
inst_1 :
  Finite.{u + 1}
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
y : F.obj (Opposite.op X)
x :
  (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
    Type u)
⊢ Eq (α := F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F X).hom :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op X))) →
            (fun (X : Type u) ↦ X) ((↑X.toTop : Type u) → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        y x :
      F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  (LightProfinite.of PUnit.{u + 1}) x).op) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op X))) →
            (fun (X : Type u) ↦ X) (F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        y :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))

Tactic:
rfl

Premises used: CompHausLike.const, CategoryTheory.Limits.Cofan.inj, rfl
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F_1 F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
simp :
  F.map (toLightProfinite.map x.unop).op ≫ Iso.hom (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y))) =
    Iso.hom (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X))) ≫ (finYoneda F).map x
⊢ (toLightProfinite.op ⋙ F).map x ≫
      Iso.hom
        ((fun (X : FintypeCatᵒᵖ) ↦
            (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X)) :
              F.obj (Opposite.op (toLightProfinite.obj (Opposite.unop X))) ≅
                (↑((toLightProfinite.obj (Opposite.unop X)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                    Type u) →
                  F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          Y) =
    Iso.hom
        ((fun (X : FintypeCatᵒᵖ) ↦
            (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X)) :
              F.obj (Opposite.op (toLightProfinite.obj (Opposite.unop X))) ≅
                (↑((toLightProfinite.obj (Opposite.unop X)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                    Type u) →
                  F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          X) ≫
      (finYoneda F).map x

Tactic:
simp only [comp_obj, op_obj, finYoneda_obj, Functor.comp_map, op_map]

Premises used: CategoryTheory.Functor.comp_obj, LightCondensed.finYoneda_obj, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.op_obj, CategoryTheory.Functor.op_map
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F_1 F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
h :
  ∀ (x_1 : F.obj (Opposite.op (toLightProfinite.obj (Opposite.unop X)))) (x_2 : (Opposite.unop Y).obj),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map (toLightProfinite.map x.unop).op ≫
              Iso.hom (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y))))).toFun
        x_1 x_2 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X))) ≫ (finYoneda F).map x))
        x_1 x_2
⊢ F.map (toLightProfinite.map x.unop).op ≫ Iso.hom (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y))) =
    Iso.hom (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X))) ≫ (finYoneda F).map x

Tactic:
ext
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F_1 F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
x_1 : F.obj (Opposite.op (toLightProfinite.obj (Opposite.unop X)))
x_2 : (Opposite.unop Y).obj
h :
  Eq (α := F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              ((toLightProfinite.map x.unop).op ≫
                Quiver.Hom.op
                  (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                    (LightProfinite.of PUnit.{u + 1}) x_2))) :
          (a : F.obj (Opposite.op (LightProfinite.of (Opposite.unop X).obj))) →
            F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
        x_1 :
      F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((finYoneda F).map x) :
          (a : (Opposite.unop X).obj → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) →
            (Opposite.unop Y).obj → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
        (fun (x : (Opposite.unop X).obj) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.map
                  (Quiver.Hom.op
                    (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                      (LightProfinite.of PUnit.{u + 1}) x))) :
              (a : F.obj (Opposite.op (LightProfinite.of (Opposite.unop X).obj))) →
                F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
            x_1)
        x_2 :
      F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map (toLightProfinite.map x.unop).op ≫
            Iso.hom (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y))))).toFun
      x_1 x_2 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X))) ≫ (finYoneda F).map x))
      x_1 x_2

Tactic:
simp only [isoFinYonedaComponents_hom, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
      ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, toLightProfinite_obj,
      ← Functor.map_comp_apply]

Premises used: LightCondensed.isoFinYonedaComponents_hom, TypeCat.Fun.coe_mk, CategoryTheory.Functor.map_comp_apply, FintypeCat.toLightProfinite_obj, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply, CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F_1 F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
x_1 : F.obj (Opposite.op (toLightProfinite.obj (Opposite.unop X)))
x_2 : (Opposite.unop Y).obj
⊢ Eq (α := F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              ((toLightProfinite.map x.unop).op ≫
                Quiver.Hom.op
                  (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                    (LightProfinite.of PUnit.{u + 1}) x_2))) :
          (a : F.obj (Opposite.op (LightProfinite.of (Opposite.unop X).obj))) →
            F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
        x_1 :
      F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((finYoneda F).map x) :
          (a : (Opposite.unop X).obj → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) →
            (Opposite.unop Y).obj → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
        (fun (x : (Opposite.unop X).obj) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.map
                  (Quiver.Hom.op
                    (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                      (LightProfinite.of PUnit.{u + 1}) x))) :
              (a : F.obj (Opposite.op (LightProfinite.of (Opposite.unop X).obj))) →
                F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
            x_1)
        x_2 :
      F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))

Tactic:
rfl
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
dsimp :
  (Iso.inv
          (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
            isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
        (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv) ≫
      (lanPresheafNatIso hX).hom =
    counitApp (P := fun (X : TopCat.{u}) ↦
      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X
⊢ (isoLocallyConstantOfIsColimit X hX).inv =
    counitApp (P := fun (X : TopCat.{u}) ↦
      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X

Tactic:
dsimp [isoLocallyConstantOfIsColimit]

Premises used: LightCondensed.isoLocallyConstantOfIsColimit
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
simp :
  Iso.inv
        (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
      (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    counitApp (P := fun (X : TopCat.{u}) ↦
      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X
⊢ (Iso.inv
          (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
            isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
        (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv) ≫
      (lanPresheafNatIso hX).hom =
    counitApp (P := fun (X : TopCat.{u}) ↦
      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
rw :
  (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    Iso.hom
        (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
      counitApp (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X
⊢ Iso.inv
        (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
      (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    counitApp (P := fun (X : TopCat.{u}) ↦
      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X

Tactic:
rw [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
w :
  ∀ (S : LightProfiniteᵒᵖ),
    ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app S =
      NatTrans.app
        (Iso.hom
            (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
              isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
          counitApp (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
        S
⊢ (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    Iso.hom
        (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
      counitApp (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X

Tactic:
ext S : 2
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
w :
  ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι
          (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
          S =
      colimit.ι
          (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          j ≫
        NatTrans.app
          (Iso.hom
              (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
            counitApp (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
          S
⊢ ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app S =
    NatTrans.app
      (Iso.hom
          (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
            isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
        counitApp (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
      S

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ obj (fromPUnit S) right
this :
  (↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of
                  (fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  PUnit.{u + 1})))).map
        g ≫
      counitAppApp (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) (Opposite.unop S) X
⊢ Eq (α :=
    (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))).obj
        { left := Y, right := right, hom := g : Comma toLightProfinite.op (fromPUnit S) } ⟶
      X.obj S)
    (colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S)
    (colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right, hom := g } ≫
      NatTrans.app
        (Iso.hom
            (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
              isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
          counitApp (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
        S)

Tactic:
simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]

Premises used: CompHausLike.LocallyConstant.counitApp, LightCondensed.locallyConstantIsoFinYoneda, LightCondensed.isoFinYoneda
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ obj (fromPUnit S) right
w :
  (↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of
                  (fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  PUnit.{u + 1})))).map
        g ≫
      counitAppApp (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) (Opposite.unop S) X
⊢ Eq (α :=
    (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))).obj
        { left := Y, right := right, hom := g : Comma toLightProfinite.op (fromPUnit S) } ⟶
      X.obj S)
    (colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S)
    (colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right, hom := g } ≫
      NatTrans.app
        (Iso.hom
            (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
              isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
          counitApp (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
        S)

Tactic:
suffices _ ≫ (isoFinYonedaComponents _ _).inv ≫ X.map g =
    (locallyConstantPresheaf _).map g ≫ counitAppApp (Opposite.unop S) X by
      simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ obj (fromPUnit S) right
w :
  Eq (α :=
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of
                  (fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  PUnit.{u + 1})))).obj
        (toLightProfinite.op.obj Y) ⟶
      X.obj (obj (fromPUnit S) right))
    ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g)
    (NatTrans.app
        (counitApp (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
        (toLightProfinite.op.obj Y) ≫
      X.map g)
⊢ (↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of
                  (fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  PUnit.{u + 1})))).map
        g ≫
      counitAppApp (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) (Opposite.unop S) X

Tactic:
erw [(counitApp.{u, u} X).naturality]