-- 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
x :
  (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
    Type u)
⊢ (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)))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                (LightProfinite.of PUnit.{u + 1}) x).op) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op X))) →
          (fun (X : Type u) ↦ X) (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))

Tactic:
simp only [← Functor.map_comp_apply, ← op_comp, CompHausLike.const_comp,
    ← isoFinYonedaComponents_hom_apply, Iso.inv_hom_id_apply, Function.comp_apply]

Premises used: LightCondensed.isoFinYonedaComponents_hom_apply, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply, CompHausLike.const_comp, Function.comp_apply, CategoryTheory.Iso.inv_hom_id_apply