awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : Profinite
F_1 F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
x_1 : F.obj (Opposite.op (toProfinite.obj (Opposite.unop X)))
x_2 : (Opposite.unop Y).obj
h :
  Eq (α := F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              ((toProfinite.map x.unop).op ≫
                Quiver.Hom.op
                  (CompHausLike.const (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
                    (Profinite.of PUnit.{u + 1}) x_2))) :
          (a : F.obj (Opposite.op (Profinite.of (Opposite.unop X).obj))) →
            F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
        x_1 :
      F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((finYoneda F).map x) :
          (a : (Opposite.unop X).obj → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) →
            (Opposite.unop Y).obj → F.obj (Opposite.op (Profinite.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))
                      (Profinite.of PUnit.{u + 1}) x))) :
              (a : F.obj (Opposite.op (Profinite.of (Opposite.unop X).obj))) →
                F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
            x_1)
        x_2 :
      F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map (toProfinite.map x.unop).op ≫
            Iso.hom (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y))))).toFun
      x_1 x_2 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom (isoFinYonedaComponents F (toProfinite.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, toProfinite_obj,
      ← Functor.map_comp_apply]

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

Tactic:
rfl
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
dsimp :
  (Iso.inv
          (lanPresheafNatIso fun (x : Profinite.{u}) ↦
            isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.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)) X
⊢ (isoLocallyConstantOfIsColimit X hX).inv =
    counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) X

Tactic:
dsimp [isoLocallyConstantOfIsColimit]

Premises used: Condensed.isoLocallyConstantOfIsColimit
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
simp :
  Iso.inv
        (lanPresheafNatIso fun (x : Profinite.{u}) ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.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)) X
⊢ (Iso.inv
          (lanPresheafNatIso fun (x : Profinite.{u}) ↦
            isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.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)) X

Tactic:
simp only [Category.assoc]

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

Tactic:
rw [Iso.inv_comp_eq]

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

Tactic:
ext S : 2
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
w :
  ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι
          (CostructuredArrow.proj toProfinite.op S ⋙
            toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
          S =
      colimit.ι
          (CostructuredArrow.proj toProfinite.op S ⋙
            toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
          j ≫
        NatTrans.app
          (Iso.hom
              (lanPresheafNatIso fun (x : Profinite.{u}) ↦
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x) ≫
            counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{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 : Profinite.{u}) ↦
            isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x) ≫
        counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{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 : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ obj (fromPUnit S) right
this :
  (↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))) ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
                  PUnit.{u + 1})))).map
        g ≫
      counitAppApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) (Opposite.unop S) X
⊢ Eq (α :=
    (CostructuredArrow.proj toProfinite.op S ⋙
            toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))).obj
        { left := Y, right := right, hom := g : Comma toProfinite.op (fromPUnit S) } ⟶
      X.obj S)
    (colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.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 toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
        { left := Y, right := right, hom := g } ≫
      NatTrans.app
        (Iso.hom
            (lanPresheafNatIso fun (x : Profinite.{u}) ↦
              isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x) ≫
          counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) X)
        S)

Tactic:
simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]

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

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

Tactic:
simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.op_obj, CompHausLike.LocallyConstant.functorToPresheaves_obj_obj
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ obj (fromPUnit S) right
w :
  Eq (α :=
    LocallyConstant
        (↑((toProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (X.obj
          (Opposite.op
            (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1}))) ⟶
      X.obj (Opposite.op (toProfinite.obj (Opposite.unop Y))))
    ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))))
    (NatTrans.app (counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) X)
      (Opposite.op (toProfinite.obj (Opposite.unop Y))))
⊢ Eq (α :=
    LocallyConstant
        (↑((toProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (X.obj
          (Opposite.op
            (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1}))) ⟶
      X.obj (obj (fromPUnit S) right))
    (((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ↦
          (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ≫
        Iso.inv (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y)))) ≫
      X.map g)
    (NatTrans.app (counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) X)
        (Opposite.op (toProfinite.obj (Opposite.unop Y))) ≫
      X.map g)

Tactic:
congr
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ obj (fromPUnit S) right
w :
  ∀
    (f :
      LocallyConstant
        (↑((toProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (X.obj
          (Opposite.op
            (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ↦
              (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ≫
            Iso.inv (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y)))))
        f =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) X)
            (Opposite.op (toProfinite.obj (Opposite.unop Y)))))
        f
⊢ Eq (α :=
    LocallyConstant
        (↑((toProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (X.obj
          (Opposite.op
            (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1}))) ⟶
      X.obj (Opposite.op (toProfinite.obj (Opposite.unop Y))))
    ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))))
    (NatTrans.app (counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) X)
      (Opposite.op (toProfinite.obj (Opposite.unop Y))))

Tactic:
ext f