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

Tactic:
apply injective_of_mono (isoFinYonedaComponents F X).hom

Premises used: Condensed.isoFinYonedaComponents, CategoryTheory.injective_of_mono, CategoryTheory.Iso.hom