awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ obj (fromPUnit S) right
⊢ Eq (α :=
    LocallyConstant
        (↑((toProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (X.obj
          (Opposite.op
            (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1}))) ⟶
      X.obj (Opposite.op (toProfinite.obj (Opposite.unop Y))))
    ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))))
    (NatTrans.app (counitApp (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) X)
      (Opposite.op (toProfinite.obj (Opposite.unop Y))))
have w : ∀
  (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})))),
  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: ext f
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ obj (fromPUnit S) right
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})))
⊢ 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
have 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)))
Tactic: simp only [toProfinite_obj, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
    ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, counitApp_app]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)
have refine_1 : ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
  ∃ (i : ℕᵒᵖᵒᵖ) (xi : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
    x =
      (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: refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
refine_1 :
  ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
    ∃ (i : ℕᵒᵖᵒᵖ) (xi : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
      x =
        (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
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)
have refine_2 : ∀ (i j : ℕᵒᵖᵒᵖ) (xi : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i))
  (xj : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
  Eq (α := (fun (X : Type u) ↦ X) (obj (obj (const ℕᵒᵖᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) i))
      ((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 :
        (fun (X : Type u) ↦ X) (obj (obj (const ℕᵒᵖᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app j) :
            (a : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj j)) →
              (fun (X : Type u) ↦ X) (((const ℕᵒᵖᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj j))
          xj :
        (fun (X : Type u) ↦ X) (obj (obj (const ℕᵒᵖᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) j)) →
    ∃ (k : ℕᵒᵖᵒᵖ) (f : i ⟶ k) (g : 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 i)) →
                (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
            xi :
          (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 j)) →
                (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
            xj :
          (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
Tactic: refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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 : ℕᵒᵖᵒᵖ) (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))
have refine_2 : ∀ (k : ℕᵒᵖ) (ki : k ⟶ i) (kj : k ⟶ j),
  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: obtain ⟨k, ki, kj, _⟩ := IsCofilteredOrEmpty.cone_objs i j
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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))
have 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)))
Tactic: refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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 (α := 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)
have 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)
Tactic: change ((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨n⟩) ≫
    (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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)
            (((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)
have 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)
Tactic: rw [(isColimitLocallyConstantPresheaf c X hc).fac]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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 (α := 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)
have 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)
Tactic: change ((((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n) ≫
    (isColimitLocallyConstantPresheafDiagram X S).desc s) _ = _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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)
            (((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)
have 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)
Tactic: rw [(isColimitLocallyConstantPresheafDiagram X S).fac]
-- 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).hom.app S = colimMap ((CostructuredArrow.proj toLightProfinite.op S).whiskerLeft i.hom)
have 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))
Tactic: simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt,
    leftKanExtensionUniqueOfIso_hom, pointwiseLeftKanExtension_desc_app]