-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op X)))
    ((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)))
    ((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)))
have a : 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: apply injective_of_mono (isoFinYonedaComponents F X).hom