awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfiniteᵒᵖ
⊢ HasColimitsOfShape (CostructuredArrow toLightProfinite.op S) (Type u)

Tactic:
hasColimitsOfShape_of_equivalence (asEquivalence (CostructuredArrow.pre Skeleton.incl.op _ S))

Premises used: CategoryTheory.Functor.op, FintypeCat.Skeleton.incl, CategoryTheory.Functor.asEquivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.CostructuredArrow.pre
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
simp :
  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))
⊢ (lanPresheafExt i).hom.app S = colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.hom)

Tactic:
simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt,
    leftKanExtensionUniqueOfIso_hom, pointwiseLeftKanExtension_desc_app]

Premises used: CategoryTheory.Functor.pointwiseLeftKanExtension_obj, LightCondensed.lanPresheaf, LightCondensed.lanPresheafExt, CategoryTheory.Functor.leftKanExtensionUniqueOfIso_hom, CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
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)))
⊢ 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))

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ ∀ (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:
aesop
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
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))
⊢ (lanPresheafExt i).inv.app S = colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.inv)

Tactic:
simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt,
    leftKanExtensionUniqueOfIso_inv, pointwiseLeftKanExtension_desc_app]

Premises used: CategoryTheory.Functor.pointwiseLeftKanExtension_obj, LightCondensed.lanPresheaf, LightCondensed.lanPresheafExt, CategoryTheory.Functor.leftKanExtensionUniqueOfIso_inv, CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
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)))
⊢ 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:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F G : LightProfiniteᵒᵖ ⥤ Type u
S : LightProfiniteᵒᵖ
i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G
⊢ ∀ (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:
aesop
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
⊢ (LightProfinite.Extend.functorOp S.asLimitCone).Final

Tactic:
LightProfinite.Extend.functorOp_final S.asLimitCone S.asLimit

Premises used: LightProfinite.asLimit, LightProfinite.asLimitCone, LightProfinite.Extend.functorOp_final
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
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)))
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F S)

Tactic:
simp [lanPresheafIso, Final.colimitIso]

Premises used: LightCondensed.lanPresheafIso, CategoryTheory.Functor.Final.colimitIso
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ 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:
rfl
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite.{u}) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
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
⊢ lanPresheaf F ≅ F

Tactic:
refine NatIso.ofComponents
    (fun ⟨S⟩ ↦ (lanPresheafIso (hF S))) fun _ ↦ ?_

Premises used: CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite.{u}) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
X Y : LightProfiniteᵒᵖ
x : X ⟶ Y
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 := ⋯ } } :
        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 := ⋯ } })
      (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)
⊢ (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:
simp only [lanPresheaf, pointwiseLeftKanExtension_obj, pointwiseLeftKanExtension_map,
    lanPresheafIso_hom, Opposite.op_unop]

Premises used: LightCondensed.lanPresheafIso_hom, Opposite.op_unop, CategoryTheory.Functor.pointwiseLeftKanExtension_obj, CategoryTheory.Functor.pointwiseLeftKanExtension_map, LightCondensed.lanPresheaf
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite.{u}) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
X Y : LightProfiniteᵒᵖ
x : X ⟶ Y
x_1 : CostructuredArrow toLightProfinite.op X
⊢ Eq (α := (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F).obj x_1 ⟶ F.obj Y)
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F))
      (colimit.ι (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F) x_1)
      (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 := ⋯ } } :
          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 := ⋯ } })
        (colimit.desc (CostructuredArrow.proj toLightProfinite.op Y ⋙ toLightProfinite.op ⋙ F)
          (LightProfinite.Extend.cocone F (Opposite.unop Y)))))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F))
      (colimit.ι (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F) x_1)
      (colimit.desc (CostructuredArrow.proj toLightProfinite.op X ⋙ toLightProfinite.op ⋙ F)
          (LightProfinite.Extend.cocone F (Opposite.unop X)) ≫
        F.map x))

Tactic:
simp
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite.{u}) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
X Y : LightProfiniteᵒᵖ
x : X ⟶ Y
⊢ 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 := ⋯ } } :
        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 := ⋯ } })
      (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:
exact colimit.hom_ext fun _ ↦ (by simp)

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite.{u}) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
⊢ (lanPresheafNatIso hF).hom.app S =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op (Opposite.op (Opposite.unop S)) ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F (Opposite.unop S))

Tactic:
simp [lanPresheafNatIso]

Premises used: LightCondensed.lanPresheafNatIso
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
rw : Presheaf.IsSheaf (coherentTopology LightProfinite) (locallyConstantPresheaf X)
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (lanPresheaf (locallyConstantPresheaf X))

Tactic:
rw [Presheaf.isSheaf_of_iso_iff (lanPresheafNatIso
      fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _)]

Premises used: CategoryTheory.Presheaf.isSheaf_of_iso_iff, LightCondensed.lanPresheafNatIso, LightCondensed.isColimitLocallyConstantPresheafDiagram
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (locallyConstantPresheaf X)

Tactic:
(CompHausLike.LocallyConstant.functor.{u, u}
      (hs := fun _ _ _ ↦ ((LightProfinite.effectiveEpi_iff_surjective _).mp)).obj X).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, LightProfinite.effectiveEpi_iff_surjective, CompHausLike.LocallyConstant.functor, Iff.mp, CategoryTheory.Functor.obj
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (locallyConstantPresheaf X)

Tactic:
exact (CompHausLike.LocallyConstant.functor.{u, u}
      (hs := fun _ _ _ ↦ ((LightProfinite.effectiveEpi_iff_surjective _).mp)).obj X).property