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

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

Tactic:
ext y

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

Proof state:
case w.h.w.e_a.h.h
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (toLightProfinite.obj (of PUnit.{u + 1}))))
⊢ ∀ (a : Function.Fiber ⇑f),
    X.map (sigmaIncl f a).op ((isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ⇑f) =
      X.map (sigmaIncl f a).op (counitAppApp (toLightProfinite.obj (Opposite.unop Y)) X f)

Tactic:
intro x

Result:
case w.h.w.e_a.h.h
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (toLightProfinite.obj (of PUnit.{u + 1}))))
x : Function.Fiber ⇑f
⊢ X.map (sigmaIncl f x).op ((isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ⇑f) =
    X.map (sigmaIncl f x).op (counitAppApp (toLightProfinite.obj (Opposite.unop Y)) X f)

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

Tactic:
apply colimit.hom_ext

Result:
case w.h.w
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
⊢ ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι
          (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙
              locallyConstantPresheaf (X.obj (Opposite.op (toLightProfinite.obj (of PUnit.{u + 1})))))
          j ≫
        ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
          S =
      colimit.ι
          (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙
              locallyConstantPresheaf (X.obj (Opposite.op (toLightProfinite.obj (of PUnit.{u + 1})))))
          j ≫
        ((lanPresheafNatIso fun x =>
                  isColimitLocallyConstantPresheafDiagram
                    (X.obj (Opposite.op (toLightProfinite.obj (of PUnit.{u + 1})))) x).hom ≫
              counitApp X).app
          S

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

Tactic:
rw [← isoFinYonedaComponents_inv_comp X _ (sigmaIncl.{u, u} f x)]

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

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

Tactic:
congr

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