awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
w :
  ∀ (j : CostructuredArrow toProfinite.op S),
    Eq (α :=
      (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F).obj j ⟶
        (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S).pt)
      (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F))
        (colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j)
        (colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S)))
      (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F))
        (colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j)
        (colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom)))
⊢ Eq (α :=
    (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F)).obj S ⟶
      (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G)).obj S)
    (colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
        (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
          (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
          (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S) :
      colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) ⟶
        (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S).pt)
    (colimMap ((CostructuredArrow.proj toProfinite.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 : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    Eq (α :=
      (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F).obj j ⟶
        (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S).pt)
      (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F))
        (colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j)
        (colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S)))
      (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F))
        (colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j)
        (colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom)))

Tactic:
aesop
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
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))
⊢ (lanPresheafExt i).inv.app S = colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.inv)

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

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

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

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

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

Tactic:
simp [lanPresheafIso, Final.colimitIso]

Premises used: Condensed.lanPresheafIso, CategoryTheory.Functor.Final.colimitIso
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : IsColimit (F.mapCocone S.asLimitCone.op)
⊢ 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:
rfl
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite.{u}) → IsColimit (F.mapCocone S.asLimitCone.op)
X Y : Profiniteᵒᵖ
x : X ⟶ Y
x_1 : CostructuredArrow toProfinite.op X
⊢ Eq (α := (CostructuredArrow.proj toProfinite.op X ⋙ toProfinite.op ⋙ F).obj x_1 ⟶ F.obj Y)
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op X ⋙ toProfinite.op ⋙ F))
      (colimit.ι (CostructuredArrow.proj toProfinite.op X ⋙ toProfinite.op ⋙ F) x_1)
      (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op Y ⋙ toProfinite.op ⋙ F))
        (colimit.desc (CostructuredArrow.proj toProfinite.op X ⋙ toProfinite.op ⋙ F)
            { pt := colimit (CostructuredArrow.proj toProfinite.op Y ⋙ toProfinite.op ⋙ F),
              ι :=
                {
                  app := fun (g : CostructuredArrow toProfinite.op X) ↦
                    colimit.ι (CostructuredArrow.proj toProfinite.op Y ⋙ toProfinite.op ⋙ F)
                      (obj (CostructuredArrow.map x) g),
                  naturality := ⋯ } } :
          colimit (CostructuredArrow.proj toProfinite.op X ⋙ toProfinite.op ⋙ F) ⟶
            Cocone.pt (J := CostructuredArrow toProfinite.op X) (F :=
              CostructuredArrow.proj toProfinite.op X ⋙ toProfinite.op ⋙ F)
              { pt := colimit (CostructuredArrow.proj toProfinite.op Y ⋙ toProfinite.op ⋙ F),
                ι :=
                  {
                    app := fun (g : CostructuredArrow toProfinite.op X) ↦
                      colimit.ι (CostructuredArrow.proj toProfinite.op Y ⋙ toProfinite.op ⋙ F)
                        (obj (CostructuredArrow.map x) g),
                    naturality := ⋯ } })
        (colimit.desc (CostructuredArrow.proj toProfinite.op Y ⋙ toProfinite.op ⋙ F)
          (Profinite.Extend.cocone F (Opposite.unop Y)))))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op X ⋙ toProfinite.op ⋙ F))
      (colimit.ι (CostructuredArrow.proj toProfinite.op X ⋙ toProfinite.op ⋙ F) x_1)
      (colimit.desc (CostructuredArrow.proj toProfinite.op X ⋙ toProfinite.op ⋙ F)
          (Profinite.Extend.cocone F (Opposite.unop X)) ≫
        F.map x))

Tactic:
simp
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite.{u}) → IsColimit (F.mapCocone S.asLimitCone.op)
X Y : Profiniteᵒᵖ
x : X ⟶ Y
⊢ (lanPresheaf F).map x ≫
      Iso.hom
        ((fun (x : Profiniteᵒᵖ) ↦
            (match (motive := (x : Profiniteᵒᵖ) → (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 : Profiniteᵒᵖ) ↦
            (match (motive := (x : Profiniteᵒᵖ) → (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:
simpa using colimit.hom_ext fun _ ↦ (by simp)

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

Tactic:
simp [lanPresheafNatIso]

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

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

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

Tactic:
((CompHausLike.LocallyConstant.functor.{u, u + 1}
      (hs := fun _ _ _ ↦ ((Profinite.effectiveEpi_tfae _).out 0 2).mp)).obj X).property

Premises used: Profinite.effectiveEpi_tfae, CategoryTheory.ObjectProperty.FullSubcategory.property, List.TFAE.out, CompHausLike.LocallyConstant.functor, Iff.mp, OfNat.ofNat, CategoryTheory.Functor.obj
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Type (u + 1)
⊢ Presheaf.IsSheaf (coherentTopology Profinite) (locallyConstantPresheaf X)

Tactic:
exact ((CompHausLike.LocallyConstant.functor.{u, u + 1}
      (hs := fun _ _ _ ↦ ((Profinite.effectiveEpi_tfae _).out 0 2).mp)).obj X).property
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : Profinite
F_1 F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts F
X : Profinite
inst_1 :
  Finite.{u_1 + 1}
    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)
⊢ PreservesLimitsOfShape.{u_1, u_1, u, u + 1, u + 1, u + 2}
    (Discrete (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)) 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' := .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.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.equivalence, TopCat.carrier, Exists.choose, Equiv.symm, CompHausLike.toTop
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts F
X : Profinite
inst_1 : Finite.{u + 1} (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ (isoFinYonedaComponents F X).hom =
    ↾fun (y : (fun (X : Type (u + 1)) ↦ X) (F.obj (Opposite.op X)))
        (x : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{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))
                  (Profinite.of PUnit.{u + 1}) x).op) :
          (a : (fun (X : Type (u + 1)) ↦ X) (F.obj (Opposite.op X))) →
            (fun (X : Type (u + 1)) ↦ X) (F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
        y

Tactic:
rfl

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

Tactic:
rfl

Premises used: CompHausLike.const, CategoryTheory.Limits.Cofan.inj, rfl
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts F
X Y : Profinite
inst_1 : Finite.{u + 1} (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
inst_2 : Finite.{u + 1} (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
f :
  (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →
    F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ (f ∘
        (⇑(ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) g) :
          (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (CompHausLike.const (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
                (Profinite.of PUnit.{u + 1}) x).op) :
        (a : (fun (X : Type (u + 1)) ↦ X) (F.obj (Opposite.op X))) →
          (fun (X : Type (u + 1)) ↦ X) (F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) : (a : F.obj (Opposite.op Y)) → F.obj (Opposite.op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F Y).inv :
            (a : (↑Y.toTop : Type u) → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) → F.obj (Opposite.op Y))
          f))

Tactic:
simp only [← Functor.map_comp_apply, ← op_comp, CompHausLike.const_comp,
    ← isoFinYonedaComponents_hom_apply, Iso.inv_hom_id_apply, Function.comp_apply]

Premises used: CategoryTheory.op_comp, Condensed.isoFinYonedaComponents_hom_apply, CategoryTheory.Functor.map_comp_apply, CompHausLike.const_comp, Function.comp_apply, CategoryTheory.Iso.inv_hom_id_apply
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : Profinite
F_1 F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
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
⊢ (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

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

Premises used: Condensed.finYoneda_obj, CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.op_obj, CategoryTheory.Functor.op_map
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : Profinite
F_1 F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts F
X Y : FintypeCatᵒᵖ
x : X ⟶ Y
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
⊢ 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:
ext