-- 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.e_a
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 =
    (counitApp X).app (Opposite.op (toProfinite.obj (Opposite.unop Y)))

Tactic:
ext f

Result:
case w.h.w.e_a.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}))))
⊢ ((fun f => ⇑f) ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv) f =
    (counitApp X).app (Opposite.op (toProfinite.obj (Opposite.unop Y))) f

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ᵒᵖ
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι
          (CostructuredArrow.proj toProfinite.op S ⋙
            toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1})))))
          j ≫
        ((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})))))
          j ≫
        ((lanPresheafNatIso fun x =>
                  isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1}))))
                    x).hom ≫
              counitApp X).app
          S

Tactic:
intro ⟨Y, _, g⟩

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✝
⊢ 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

Proof state:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
⊢ (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    (lanPresheafNatIso fun x =>
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1})))) x).hom ≫
      counitApp X

Tactic:
ext S : 2

Result:
case w.h
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
⊢ ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app S =
    ((lanPresheafNatIso fun x =>
              isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1}))))
                x).hom ≫
          counitApp X).app
      S

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 =
    (locallyConstantPresheaf (X.obj (Opposite.op (toProfinite.obj (of PUnit.{u + 1}))))).map g ≫
      counitAppApp (Opposite.unop S) X

Tactic:
erw [(counitApp.{u, u+1} X).naturality]

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

Proof state:
case w.h.w.e_a.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}))))
⊢ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ⇑f =
    counitAppApp (toProfinite.obj (Opposite.unop Y)) X f

Tactic:
apply presheaf_ext.{u, u+1} (X := X) (Y := X) (f := f)

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}))))
⊢ ∀ (a : Function.Fiber ⇑f),
    X.map (sigmaIncl f a).op ((isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ⇑f) =
      X.map (sigmaIncl f a).op (counitAppApp (toProfinite.obj (Opposite.unop Y)) X f)