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

Tactic:
simp only [toProfinite_obj, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
    ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, counitApp_app]

Premises used: CompHausLike.LocallyConstant.counitApp_app, TypeCat.Fun.coe_mk, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply, FintypeCat.toProfinite_obj, CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ obj (fromPUnit S) right
f :
  LocallyConstant
    (↑((toProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    (X.obj
      (Opposite.op (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})))
x :
  Function.Fiber (Y :=
    (↑((toProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (Z :=
    X.obj
      (Opposite.op (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})))
    (⇑f :
      (a : (↑(toProfinite.obj (Opposite.unop Y)).toTop : Type u)) →
        X.obj (Opposite.op (CompHausLike.of (fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) PUnit.{u + 1})))
⊢ Finite.{u + 1}
    (↑((fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x).toTop (P :=
          fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)

Tactic:
have : Finite (fiber.{u, u + 1} f x) :=
    Finite.of_injective (sigmaIncl.{u, u + 1} f x).1 Subtype.val_injective
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
f :
  LocallyConstant
    (↑(c.pt.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
j : ℕᵒᵖ
h :
  ∃ (g :
    LocallyConstant
      (↑((((F ⋙ toLightProfinite) ⋙ lightToProfinite).obj j).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      X),
    f = LocallyConstant.comap (TopCat.Hom.hom ((lightToProfinite.mapCone c).π.app j).hom) g
⊢ ∃ (i : ℕᵒᵖᵒᵖ) (xi : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app i) :
          (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i)) →
            (fun (X : Type u) ↦ X) (((const ℕᵒᵖᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj i))
        xi

Tactic:
⟨⟨j⟩, h⟩

Premises used: Opposite.op, Exists.intro
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
f :
  LocallyConstant
    (↑(c.pt.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
j : ℕᵒᵖ
h :
  ∃ (g :
    LocallyConstant
      (↑((((F ⋙ toLightProfinite) ⋙ lightToProfinite).obj j).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      X),
    f = LocallyConstant.comap (TopCat.Hom.hom ((lightToProfinite.mapCone c).π.app j).hom) g
⊢ ∃ (i : ℕᵒᵖᵒᵖ) (xi : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app i) :
          (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i)) →
            (fun (X : Type u) ↦ X) (((const ℕᵒᵖᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj i))
        xi

Tactic:
exact ⟨⟨j⟩, h⟩
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi :
  LocallyConstant
    (↑(((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
fj :
  LocallyConstant
    (↑(((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h_1 : True
⊢ ∃ (k : ℕᵒᵖᵒᵖ) (f : Opposite.op i ⟶ k) (g : Opposite.op j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f) :
            (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
              (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fi :
        (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g) :
            (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
              (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fj :
        (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))

Tactic:
⟨⟨k⟩, ki.op, kj.op, ?_⟩

Premises used: Quiver.Hom.op, Opposite.op, Exists.intro
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi :
  LocallyConstant
    (↑(((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
fj :
  LocallyConstant
    (↑(((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h_1 : True
refine_2 :
  Eq (α := (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map ki.op) :
          (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
            (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
        fi :
      (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map kj.op) :
          (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
            (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
        fj :
      (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
⊢ ∃ (k : ℕᵒᵖᵒᵖ) (f : Opposite.op i ⟶ k) (g : Opposite.op j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f) :
            (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
              (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fi :
        (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g) :
            (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
              (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fj :
        (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))

Tactic:
refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi :
  LocallyConstant
    (↑(((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
fj :
  LocallyConstant
    (↑(((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h_1 : True
x_1 :
  (↑((toLightProfinite.obj (F.obj k)).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
    Type u)
x :
  (↑((obj (obj (const ℕᵒᵖ) c.pt) k).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
    Type u)
hx :
  (ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u)))
          (CC :=
          fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          (c.π.app k) :
        (a :
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              (((const ℕᵒᵖ).obj c.pt).obj k)) →
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            ((F ⋙ toLightProfinite).obj k))
      x =
    x_1
⊢ Eq (α := X)
    ((LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi :
          (a : (↑(((const ℕᵒᵖ).obj c.pt).obj i).toTop : Type u)) → X)
        x :
      X)
    ((LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj :
          (a : (↑(((const ℕᵒᵖ).obj c.pt).obj i).toTop : Type u)) → X)
        x :
      X)

Tactic:
have h := LocallyConstant.congr_fun h x
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)
n : ℕᵒᵖ
f :
  LocallyConstant
    (↑((toLightProfinite.obj (F.obj n)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
change :
  Eq (α := (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op n) ≫
              (isColimitLocallyConstantPresheaf c X hc).desc s) :
          (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op n))) →
            (fun (X : Type u) ↦ X) s.pt)
        f :
      (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op n)) :
          (a : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop : Type u) X) → s.pt)
        f :
      s.pt)
⊢ Eq (α := s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isColimitLocallyConstantPresheaf c X hc).desc s) :
          (a : LocallyConstant (↑c.pt.toTop : Type u) X) → s.pt)
        (LocallyConstant.comap (TopCat.Hom.hom (c.π.app n).hom) f) :
      s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op n)) :
          (a : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop : Type u) X) → s.pt)
        f :
      s.pt)

Tactic:
change ((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨n⟩) ≫
    (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Cocone.ι, LightCondensed.isColimitLocallyConstantPresheaf, Opposite.op, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp, LightCondensed.locallyConstantPresheaf, CategoryTheory.Limits.Cone.op, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)
n : ℕᵒᵖ
f :
  LocallyConstant
    (↑((toLightProfinite.obj (F.obj n)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
rw :
  Eq (α := (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op n)) :
          (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op n))) →
            (fun (X : Type u) ↦ X) s.pt)
        f :
      (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op n)) :
          (a : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop : Type u) X) → s.pt)
        f :
      s.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op n) ≫
              (isColimitLocallyConstantPresheaf c X hc).desc s) :
          (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op n))) →
            (fun (X : Type u) ↦ X) s.pt)
        f :
      (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op n)) :
          (a : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop : Type u) X) → s.pt)
        f :
      s.pt)

Tactic:
rw [(isColimitLocallyConstantPresheaf c X hc).fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, LightCondensed.isColimitLocallyConstantPresheaf
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)
n : ℕᵒᵖ
f :
  LocallyConstant
    (↑((toLightProfinite.obj (F.obj n)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
⊢ Eq (α := (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op n)) :
          (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op n))) →
            (fun (X : Type u) ↦ X) s.pt)
        f :
      (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op n)) :
          (a : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop : Type u) X) → s.pt)
        f :
      s.pt)

Tactic:
rfl
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f :
  LocallyConstant
    (↑((S.diagram.obj (Opposite.op n)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
change :
  Eq (α := (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n ≫
              (isColimitLocallyConstantPresheafDiagram X S).desc s) :
          (a : (fun (X : Type u) ↦ X) ((S.diagram.rightOp ⋙ locallyConstantPresheaf X).obj n)) →
            (fun (X : Type u) ↦ X) s.pt)
        f :
      (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app n) :
          (a : LocallyConstant (↑(toLightProfinite.obj (S.fintypeDiagram.obj (Opposite.op n))).toTop : Type u) X) →
            s.pt)
        f :
      s.pt)
⊢ Eq (α := s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isColimitLocallyConstantPresheafDiagram X S).desc s) :
          (a : LocallyConstant (↑S.asLimitCone.pt.toTop : Type u) X) → s.pt)
        (LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (S.asLimitCone.π.app (Opposite.op n)))) f) :
      s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app n) :
          (a : LocallyConstant (↑(toLightProfinite.obj (S.fintypeDiagram.obj (Opposite.op n))).toTop : Type u) X) →
            s.pt)
        f :
      s.pt)

Tactic:
change ((((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n) ≫
    (isColimitLocallyConstantPresheafDiagram X S).desc s) _ = _

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.coconeRightOpOfCone, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp, LightCondensed.locallyConstantPresheaf, LightProfinite.asLimitCone, DFunLike.coe, CategoryTheory.NatTrans.app, LightCondensed.isColimitLocallyConstantPresheafDiagram
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f :
  LocallyConstant
    (↑((S.diagram.obj (Opposite.op n)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
rw :
  Eq (α := (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app n) :
          (a : (fun (X : Type u) ↦ X) ((S.diagram.rightOp ⋙ locallyConstantPresheaf X).obj n)) →
            (fun (X : Type u) ↦ X) s.pt)
        f :
      (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app n) :
          (a : LocallyConstant (↑(toLightProfinite.obj (S.fintypeDiagram.obj (Opposite.op n))).toTop : Type u) X) →
            s.pt)
        f :
      s.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n ≫
              (isColimitLocallyConstantPresheafDiagram X S).desc s) :
          (a : (fun (X : Type u) ↦ X) ((S.diagram.rightOp ⋙ locallyConstantPresheaf X).obj n)) →
            (fun (X : Type u) ↦ X) s.pt)
        f :
      (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app n) :
          (a : LocallyConstant (↑(toLightProfinite.obj (S.fintypeDiagram.obj (Opposite.op n))).toTop : Type u) X) →
            s.pt)
        f :
      s.pt)

Tactic:
rw [(isColimitLocallyConstantPresheafDiagram X S).fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, LightCondensed.isColimitLocallyConstantPresheafDiagram
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f :
  LocallyConstant
    (↑((S.diagram.obj (Opposite.op n)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
⊢ Eq (α := (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app n) :
          (a : (fun (X : Type u) ↦ X) ((S.diagram.rightOp ⋙ locallyConstantPresheaf X).obj n)) →
            (fun (X : Type u) ↦ X) s.pt)
        f :
      (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app n) :
          (a : LocallyConstant (↑(toLightProfinite.obj (S.fintypeDiagram.obj (Opposite.op n))).toTop : Type u) X) →
            s.pt)
        f :
      s.pt)

Tactic:
rfl