-- 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.h.h.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}))))
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 (Profinite.of PUnit.{u + 1}) y ≫ sigmaIncl f x).op
      ((isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ⇑f) =
    X.map (𝟙 (Profinite.of PUnit.{u + 1})).op (Function.Fiber.image (⇑f) x)

Tactic:
simp only [op_comp, FunctorToTypes.map_comp_apply, op_id, FunctorToTypes.map_id_apply]

Result:
case w.h.w.e_a.h.h.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}))))
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 (Profinite.of PUnit.{u + 1}) y).op
      (X.map (sigmaIncl f x).op ((isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ⇑f)) =
    Function.Fiber.image (⇑f) 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) =
    counitAppAppImage f x

Tactic:
simp only [counitAppAppImage, CompHausLike.coe_of]

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
⊢ 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.e_a.h.h.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}))))
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 (Profinite.of PUnit.{u + 1}) y).op
      ((isoFinYonedaComponents X (fiber f x)).inv (⇑f ∘ ⇑(ConcreteCategory.hom (sigmaIncl f x)))) =
    Function.Fiber.image (⇑f) x

Tactic:
simpa [← isoFinYonedaComponents_hom_apply] using x.map_eq_image f y

Result:
no goals

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
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)

Tactic:
apply injective_of_mono (isoFinYonedaComponents X (fiber.{u, u+1} f x)).hom

Result:
case w.h.w.e_a.h.h.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✝
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' ⋯
⊢ (isoFinYonedaComponents X (fiber f x)).hom
      (X.map (sigmaIncl f x).op ((isoFinYonedaComponents X (toProfinite.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))

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}))))
⊢ ∀ (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)

Tactic:
intro x

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
⊢ X.map (sigmaIncl f x).op ((isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ⇑f) =
    X.map (sigmaIncl f x).op (counitAppApp (toProfinite.obj (Opposite.unop Y)) X f)