-- Mathlib/Condensed/Discrete/Colimit.lean
lemma isoLocallyConstantOfIsColimit_inv (X : Profinite.{u}ᵒᵖ ⥤ Type (u+1))
    [PreservesFiniteProducts X]
    (hX : ∀ S : Profinite.{u}, (IsColimit <| X.mapCocone S.asLimitCone.op)) :
    (isoLocallyConstantOfIsColimit X hX).inv =
      (CompHausLike.LocallyConstant.counitApp.{u, u+1} X)

Proof state:
case w.h.w
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1})))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S =
    colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1})))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafNatIso fun x =>
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1}))))
                  x).hom ≫
            counitApp X).app
        S

Tactic:
simp? [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp] says
  simp only [comp_obj, CostructuredArrow.proj_obj, op_obj, functorToPresheaves_obj_obj,
    isoFinYoneda, locallyConstantIsoFinYoneda, finYoneda_obj, LocallyConstant.toFun_eq_coe,
    NatTrans.comp_app, pointwiseLeftKanExtension_obj, lanPresheafExt_inv, Iso.trans_inv,
    Iso.symm_inv, whiskerLeft_comp, lanPresheafNatIso_hom_app, Opposite.op_unop, colimit.map_desc,
    id_eq, Functor.comp_map, op_map, colimit.ι_desc, Cocones.precompose_obj_pt,
    Profinite.Extend.cocone_pt, Cocones.precompose_obj_ι, Category.assoc, const_obj_obj,
    whiskerLeft_app, NatIso.ofComponents_hom_app, NatIso.ofComponents_inv_app,
    Profinite.Extend.cocone_ι_app, counitApp, colimit.ι_desc_assoc]

Result:
case w.h.w
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ (fun f => ⇑f) ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (locallyConstantPresheaf (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1}))))).map g ≫
      counitAppApp (Opposite.unop S) X

Proof state:
case w.h.w
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1})))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S =
    colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1})))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafNatIso fun x =>
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1}))))
                  x).hom ≫
            counitApp X).app
        S

Tactic:
simp only [comp_obj, CostructuredArrow.proj_obj, op_obj, functorToPresheaves_obj_obj,
  isoFinYoneda, locallyConstantIsoFinYoneda, finYoneda_obj, LocallyConstant.toFun_eq_coe,
  NatTrans.comp_app, pointwiseLeftKanExtension_obj, lanPresheafExt_inv, Iso.trans_inv,
  Iso.symm_inv, whiskerLeft_comp, lanPresheafNatIso_hom_app, Opposite.op_unop, colimit.map_desc,
  id_eq, Functor.comp_map, op_map, colimit.ι_desc, Cocones.precompose_obj_pt,
  Profinite.Extend.cocone_pt, Cocones.precompose_obj_ι, Category.assoc, const_obj_obj,
  whiskerLeft_app, NatIso.ofComponents_hom_app, NatIso.ofComponents_inv_app,
  Profinite.Extend.cocone_ι_app, counitApp, colimit.ι_desc_assoc]

Result:
case w.h.w
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ (fun f => ⇑f) ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (locallyConstantPresheaf (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1}))))).map g ≫
      counitAppApp (Opposite.unop S) X

Proof state:
case w.h.w.e_a.h.h
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1}))))
x : Function.Fiber ⇑f
⊢ X.map (sigmaIncl f x).op ((isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ⇑f) =
    X.map (CompHausLike.isTerminalPUnit.from (fiber f x)).op (Function.Fiber.image (⇑f) x)

Tactic:
letI : Fintype (fiber.{u, u+1} f x) :=
  Fintype.ofInjective (sigmaIncl.{u, u+1} f x).1 Subtype.val_injective

Result:
case w.h.w.e_a.h.h
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1}))))
x : Function.Fiber ⇑f
this : Fintype ↑(fiber f x).toTop := Fintype.ofInjective ⇑(sigmaIncl f x).hom' ⋯
⊢ X.map (sigmaIncl f x).op ((isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ⇑f) =
    X.map (CompHausLike.isTerminalPUnit.from (fiber f x)).op (Function.Fiber.image (⇑f) x)

Proof state:
case w.h.w
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ (fun f => ⇑f) ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (counitApp X).app (Opposite.op (toProfinite.obj (Opposite.unop Y))) ≫ X.map g

Tactic:
simp only [← Category.assoc]

Result:
case w.h.w
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ ((fun f => ⇑f) ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv) ≫ X.map g =
    (counitApp X).app (Opposite.op (toProfinite.obj (Opposite.unop Y))) ≫ X.map g