awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ (lanPresheafExt i).inv.app S = colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.inv)
have simp : Eq (α :=
  colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) ⟶
    colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F))
  (colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
        (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
        (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S) :
    colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) ⟶
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
          (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
          (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S).pt)
  (colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.inv))
Tactic: simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt,
    leftKanExtensionUniqueOfIso_inv, pointwiseLeftKanExtension_desc_app]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ Eq (α :=
    colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) ⟶
      colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F))
    (colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
        (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
          (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
          (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S) :
      colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) ⟶
        (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
            (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S).pt)
    (colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.inv))
have w : ∀ (j : CostructuredArrow toProfinite.op S),
  Eq (α :=
    (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G).obj j ⟶
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
          (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
          (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S).pt)
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G))
      (colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j)
      (colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
        (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
          (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
          (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S)))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G))
      (colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j)
      (colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.inv)))
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : IsColimit (F.mapCocone S.asLimitCone.op)
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F)
      (Profinite.Extend.cocone F S)
have simp : Eq (α :=
  colimit
      (Profinite.Extend.functorOp S.asLimitCone ⋙
        CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F) ⟶
    F.obj (Opposite.op S))
  (Iso.hom (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (S.diagram.op ⋙ F)) hF))
  (colimit.desc
    (Profinite.Extend.functorOp S.asLimitCone ⋙
      CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F)
    (Cocone.whisker (Profinite.Extend.functorOp S.asLimitCone) (Profinite.Extend.cocone F S)))
Tactic: simp [lanPresheafIso, Final.colimitIso]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Type (u + 1)
⊢ Presheaf.IsSheaf (coherentTopology Profinite) (lanPresheaf (locallyConstantPresheaf X))
have rw : Presheaf.IsSheaf (coherentTopology Profinite) (locallyConstantPresheaf X)
Tactic: rw [Presheaf.isSheaf_of_iso_iff (lanPresheafNatIso
      fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _)]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
S : Profinite
F_1 F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
⊢ (toProfinite.op ⋙ F).map x ≫
      Iso.hom
        ((fun (X : FintypeCatᵒᵖ) ↦
            (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X)) :
              F.obj (Opposite.op (toProfinite.obj (Opposite.unop X))) ≅
                (↑((toProfinite.obj (Opposite.unop X)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u) →
                  F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
          Y) =
    Iso.hom
        ((fun (X : FintypeCatᵒᵖ) ↦
            (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X)) :
              F.obj (Opposite.op (toProfinite.obj (Opposite.unop X))) ≅
                (↑((toProfinite.obj (Opposite.unop X)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u) →
                  F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
          X) ≫
      (finYoneda F).map x
have simp : F.map (toProfinite.map x.unop).op ≫ Iso.hom (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y))) =
  Iso.hom (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X))) ≫ (finYoneda F).map x
Tactic: simp only [comp_obj, op_obj, finYoneda_obj, Functor.comp_map, op_map]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
S : Profinite
F_1 F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
⊢ F.map (toProfinite.map x.unop).op ≫ Iso.hom (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y))) =
    Iso.hom (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X))) ≫ (finYoneda F).map x
have h : ∀ (x_1 : F.obj (Opposite.op (toProfinite.obj (Opposite.unop X)))) (x_2 : (Opposite.unop Y).obj),
  (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: ext
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
⊢ (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
have 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})))
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]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
⊢ (isoLocallyConstantOfIsColimit X hX).inv =
    counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) X
have 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
Tactic: dsimp [isoLocallyConstantOfIsColimit]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
⊢ (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
have 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
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
⊢ 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
have 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
Tactic: rw [Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
⊢ (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
have 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
Tactic: ext S : 2
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
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
have 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
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
⊢ 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)
have 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
Tactic: suffices _ ≫ (isoFinYonedaComponents _ _).inv ≫ X.map g =
    (locallyConstantPresheaf _).map g ≫ counitAppApp (Opposite.unop S) X by
      simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
⊢ (↾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
have 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)
Tactic: erw [(counitApp.{u, u + 1} X).naturality]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
⊢ 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)
have 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)
Tactic: simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
⊢ 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)
have 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))))
Tactic: congr