-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts F
X Y : LightProfinite
inst_1 :
  Finite.{u + 1}
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
inst_2 :
  Finite.{u + 1}
    (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
f :
  (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u) →
    F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
a :
  Eq (α :=
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u) →
      F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
    (f ∘
      (⇑(ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
            g) :
        (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F X).hom :
        (a : F.obj (Opposite.op X)) → (↑X.toTop : Type u) → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) : (a : F.obj (Opposite.op Y)) → F.obj (Opposite.op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F Y).inv :
                (a : (↑Y.toTop : Type u) → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) →
                  F.obj (Opposite.op Y))
              f :
            F.obj (Opposite.op Y)) :
        F.obj (Opposite.op X)))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((↑(X.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u) →
        F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F X).hom :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op X))) →
            (fun (X : Type u) ↦ X) ((↑X.toTop : Type u) → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F X).inv :
              (a :
                  (fun (X : Type u) ↦ X)
                    ((↑X.toTop : Type u) → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) →
                (fun (X : Type u) ↦ X) (F.obj (Opposite.op X)))
            (f ∘
              (⇑(ConcreteCategory.hom (FC :=
                    fun
                      (x1 x2 :
                        CompHausLike fun (X : TopCat.{u}) ↦
                          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                        Type u),
                      (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                        Type u)))
                    (CC :=
                    fun
                      (X :
                        CompHausLike fun (X : TopCat.{u}) ↦
                          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
                    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                      Type u))
                    g) :
                (a :
                    (fun
                          (X :
                            CompHausLike fun (X : TopCat) ↦
                              TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                        (↑X.toTop : Type u))
                      X) →
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    Y)) :
          (fun (X : Type u) ↦ X) (F.obj (Opposite.op X))) :
      (fun (X : Type u) ↦ X)
        ((↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u) →
          F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F X).hom :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op X))) →
            (fun (X : Type u) ↦ X) ((↑X.toTop : Type u) → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
              (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op Y))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op X)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F Y).inv :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((↑Y.toTop : Type u) → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) →
                    (fun (X : Type u) ↦ X) (F.obj (Opposite.op Y)))
                f :
              (fun (X : Type u) ↦ X) (F.obj (Opposite.op Y))) :
          (fun (X : Type u) ↦ X) (F.obj (Opposite.op X))) :
      (fun (X : Type u) ↦ X)
        ((↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u) →
          F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))

Tactic:
simp only [Iso.inv_hom_id_apply]

Premises used: CategoryTheory.Iso.inv_hom_id_apply