awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ Eq (α :=
    colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) ⟶
      colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G))
    (colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F)
        (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
          (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
          (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S) :
      colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) ⟶
        (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
            (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S).pt)
    (colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.hom))
have w : ∀ (j : CostructuredArrow toLightProfinite.op S),
  Eq (α :=
    (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F).obj j ⟶
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
          (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
          (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S).pt)
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F))
      (colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) j)
      (colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F)
        (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ F)
          (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ G))
          (i.hom ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ G)) S)))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F))
      (colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F) j)
      (colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.hom)))
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ (lanPresheafExt i).inv.app S = colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.inv)
have simp : Eq (α :=
  colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) ⟶
    colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F))
  (colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
        (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
        (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S) :
    colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) ⟶
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
          (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
          (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S).pt)
  (colimMap ((CostructuredArrow.proj toLightProfinite.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 : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ Eq (α :=
    colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) ⟶
      colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ F))
    (colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
        (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
          (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
          (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S) :
      colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) ⟶
        (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
            (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
            (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S).pt)
    (colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.inv))
have w : ∀ (j : CostructuredArrow toLightProfinite.op S),
  Eq (α :=
    (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G).obj j ⟶
      (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
          (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
          (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S).pt)
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G))
      (colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j)
      (colimit.desc (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G)
        (toLightProfinite.op.costructuredArrowMapCocone (toLightProfinite.op ⋙ G)
          (toLightProfinite.op.pointwiseLeftKanExtension (toLightProfinite.op ⋙ F))
          (i.inv ≫ toLightProfinite.op.pointwiseLeftKanExtensionUnit (toLightProfinite.op ⋙ F)) S)))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G))
      (colimit.ι (CostructuredArrow.proj toLightProfinite.op S ⋙ toLightProfinite.op ⋙ G) j)
      (colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.inv)))
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F S)
have simp : Eq (α :=
  colimit
      (LightProfinite.Extend.functorOp S.asLimitCone ⋙
        CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F) ⟶
    F.obj (Opposite.op S))
  (Iso.hom (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (S.diagram.rightOp ⋙ F)) hF))
  (colimit.desc
    (LightProfinite.Extend.functorOp S.asLimitCone ⋙
      CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F)
    (Cocone.whisker (LightProfinite.Extend.functorOp S.asLimitCone) (LightProfinite.Extend.cocone F S)))
Tactic: simp [lanPresheafIso, Final.colimitIso]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite.{u}) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ lanPresheaf F ≅ F
have refine : ∀ {X Y : LightProfiniteᵒᵖ} (x : X ⟶ Y),
  (lanPresheaf F).map x ≫
      Iso.hom
        ((fun (x : LightProfiniteᵒᵖ) ↦
            (match (motive := (x : LightProfiniteᵒᵖ) → (lanPresheaf F).obj x ≅ F.obj x) x with
              | Opposite.op S => lanPresheafIso (hF S) :
              (lanPresheaf F).obj x ≅ F.obj x))
          Y) =
    Iso.hom
        ((fun (x : LightProfiniteᵒᵖ) ↦
            (match (motive := (x : LightProfiniteᵒᵖ) → (lanPresheaf F).obj x ≅ F.obj x) x with
              | Opposite.op S => lanPresheafIso (hF S) :
              (lanPresheaf F).obj x ≅ F.obj x))
          X) ≫
      F.map x
Tactic: refine NatIso.ofComponents
    (fun ⟨S⟩ ↦ (lanPresheafIso (hF S))) fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite.{u}) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
X Y : LightProfiniteᵒᵖ
x : X ⟶ Y
⊢ (lanPresheaf F).map x ≫
      Iso.hom
        ((fun (x : LightProfiniteᵒᵖ) ↦
            (match (motive := (x : LightProfiniteᵒᵖ) → (lanPresheaf F).obj x ≅ F.obj x) x with
              | Opposite.op S => lanPresheafIso (hF S) :
              (lanPresheaf F).obj x ≅ F.obj x))
          Y) =
    Iso.hom
        ((fun (x : LightProfiniteᵒᵖ) ↦
            (match (motive := (x : LightProfiniteᵒᵖ) → (lanPresheaf F).obj x ≅ F.obj x) x with
              | Opposite.op S => lanPresheafIso (hF S) :
              (lanPresheaf F).obj x ≅ F.obj x))
          X) ≫
      F.map x
have simp : Eq (α := colimit (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F) ⟶ F.obj Y)
  (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toLightProfinite.op Y ⋙ toLightProfinite.op ⋙ F))
    (colimit.desc (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F)
        { pt := colimit (CostructuredArrow.proj toLightProfinite.op Y ⋙ toLightProfinite.op ⋙ F),
          ι :=
            {
              app := fun (g : CostructuredArrow toLightProfinite.op X) ↦
                colimit.ι (CostructuredArrow.proj toLightProfinite.op Y ⋙ toLightProfinite.op ⋙ F)
                  (obj (CostructuredArrow.map x) g),
              naturality := sorry } } :
      colimit (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F) ⟶
        Cocone.pt (J := CostructuredArrow toLightProfinite.op X) (F :=
          CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F)
          { pt := colimit (CostructuredArrow.proj toLightProfinite.op Y ⋙ toLightProfinite.op ⋙ F),
            ι :=
              {
                app := fun (g : CostructuredArrow toLightProfinite.op X) ↦
                  colimit.ι (CostructuredArrow.proj toLightProfinite.op Y ⋙ toLightProfinite.op ⋙ F)
                    (obj (CostructuredArrow.map x) g),
                naturality := sorry } })
    (colimit.desc (CostructuredArrow.proj toLightProfinite.op Y ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F (Opposite.unop Y))))
  (colimit.desc (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F (Opposite.unop X)) ≫
    F.map x)
Tactic: simp only [lanPresheaf, pointwiseLeftKanExtension_obj, pointwiseLeftKanExtension_map,
    lanPresheafIso_hom, Opposite.op_unop]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (lanPresheaf (locallyConstantPresheaf X))
have rw : Presheaf.IsSheaf (coherentTopology LightProfinite) (locallyConstantPresheaf X)
Tactic: rw [Presheaf.isSheaf_of_iso_iff (lanPresheafNatIso
      fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _)]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
S : LightProfinite
F_1 F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
⊢ (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
have 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
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 : LightProfinite
F_1 F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
⊢ (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
have 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})))
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]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (isoLocallyConstantOfIsColimit X hX).inv =
    counitApp (P := fun (X : TopCat.{u}) ↦
      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X
have 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
Tactic: dsimp [isoLocallyConstantOfIsColimit]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (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
have 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
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ 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
have 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
Tactic: rw [Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (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
have 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
Tactic: ext S : 2
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
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
have 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
Tactic: apply colimit.hom_ext