-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
i j : J
f : i ⟶ j
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const J)
          (ofProfinite
            (Profinite.limitCone.{v, u}
                (F ⋙
                  forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                    (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)) →ₜ*
                      (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)))
                    (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                    (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)))
                    Profinite (FD :=
                    fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)),
                      (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v))))
                    (CD := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v))))).pt))
        i ⟶
      F.obj j)
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          (ofProfinite
            (Profinite.limitCone.{v, u}
                (F ⋙
                  forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                    (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)) →ₜ*
                      (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)))
                    (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                    (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)))
                    Profinite (FD :=
                    fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)),
                      (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v))))
                    (CD := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v))))).pt))
        f ≫
      {
        hom' :=
          {
            toFun :=
              fun
                (x :
                  (↑((Functor.obj
                              (Functor.obj (Functor.const J)
                                (ofProfinite
                                  (Profinite.limitCone.{v, u}
                                      (F ⋙
                                        forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                                          (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                              Type (max u v)) →ₜ*
                                            (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                              Type (max u v)))
                                          (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                                          (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                            Type (max u v)))
                                          Profinite (FD :=
                                          fun
                                            (x1 x2 :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                          C((↑(x1.toTop (P := fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                              Type (max u v)),
                                            (↑(x2.toTop (P := fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                              Type (max u v))))
                                          (CD :=
                                          fun
                                            (X :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                          (↑(X.toTop (P := fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                            Type (max u v))))).pt))
                              j).toProfinite.toTop
                        (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))) ↦
              (↑x :
                  (j : J) →
                    (↑((((F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) :
                      Type (max u v)))
                j,
            map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ } })
    ({
        hom' :=
          {
            toFun :=
              fun
                (x :
                  (↑((Functor.obj
                              (Functor.obj (Functor.const J)
                                (ofProfinite
                                  (Profinite.limitCone.{v, u}
                                      (F ⋙
                                        forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                                          (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                              Type (max u v)) →ₜ*
                                            (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                              Type (max u v)))
                                          (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                                          (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                            Type (max u v)))
                                          Profinite (FD :=
                                          fun
                                            (x1 x2 :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                          C((↑(x1.toTop (P := fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                              Type (max u v)),
                                            (↑(x2.toTop (P := fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                              Type (max u v))))
                                          (CD :=
                                          fun
                                            (X :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                          (↑(X.toTop (P := fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                            Type (max u v))))).pt))
                              i).toProfinite.toTop
                        (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))) ↦
              (↑x :
                  (j : J) →
                    (↑((((F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) :
                      Type (max u v)))
                i,
            map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ } } ≫
      F.map f)
have simp : {
    hom' :=
      {
        toFun :=
          fun
            (x :
              (↑((Profinite.limitCone.{v, u}
                          (F ⋙
                            forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                              (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v)) →ₜ*
                                (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v)))
                              (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                              (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                Type (max u v)))
                              Profinite (FD :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v)),
                                (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v))))
                              (CD :=
                              fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                              (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                Type (max u v))))).pt.toTop
                    (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))) ↦
          (↑x :
              (j : J) →
                (↑(compHausToTop.obj
                      (profiniteToCompHaus.obj ((forget₂ ProfiniteGrp.{max u v} Profinite).obj (F.obj j)))) :
                  Type (max u v)))
            j,
        map_one' := sorry, map_mul' := sorry, continuous_toFun := sorry :
        (↑((Profinite.limitCone.{v, u}
                      (F ⋙
                        forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                          (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                              Type (max u v)) →ₜ*
                            (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                              Type (max u v)))
                          (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                          (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                            Type (max u v)))
                          Profinite (FD :=
                          fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                              Type (max u v)),
                            (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                              Type (max u v))))
                          (CD :=
                          fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                          (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                            Type (max u v))))).pt.toTop
                (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
            Type (max u v)) →ₜ*
          (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
            Type (max u v)) } :
    (ofProfinite
          (Profinite.limitCone.{v, u}
              (F ⋙
                forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                  (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)) →ₜ*
                    (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)))
                  (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                  (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v)))
                  Profinite (FD :=
                  fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)),
                    (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v))))
                  (CD := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))))).pt).Hom
      (F.obj j) } =
  {
      hom' :=
        {
          toFun :=
            fun
              (x :
                (↑((Profinite.limitCone.{v, u}
                            (F ⋙
                              forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v)) →ₜ*
                                  (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v)))
                                (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                                (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v)))
                                Profinite (FD :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v)),
                                  (↑(x2.toTop (P := fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                    Type (max u v))))
                                (CD :=
                                fun
                                  (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                                (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                  Type (max u v))))).pt.toTop
                      (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                  Type (max u v))) ↦
            (↑x :
                (j : J) →
                  (↑(compHausToTop.obj
                        (profiniteToCompHaus.obj ((forget₂ ProfiniteGrp.{max u v} Profinite).obj (F.obj j)))) :
                    Type (max u v)))
              i,
          map_one' := sorry, map_mul' := sorry, continuous_toFun := sorry :
          (↑((Profinite.limitCone.{v, u}
                        (F ⋙
                          forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                            (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                Type (max u v)) →ₜ*
                              (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                Type (max u v)))
                            (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                            (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                              Type (max u v)))
                            Profinite (FD :=
                            fun
                              (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                Type (max u v)),
                              (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                                Type (max u v))))
                            (CD :=
                            fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                            (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                              Type (max u v))))).pt.toTop
                  (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
              Type (max u v)) →ₜ*
            (↑((F.obj i).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
              Type (max u v)) } :
      (ofProfinite
            (Profinite.limitCone.{v, u}
                (F ⋙
                  forget₂ ProfiniteGrp.{max u v} (FC := fun (X Y : ProfiniteGrp.{max u v}) ↦
                    (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)) →ₜ*
                      (↑(Y.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)))
                    (CC := fun (X : ProfiniteGrp.{max u v}) ↦
                    (↑(X.toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v)))
                    Profinite (FD :=
                    fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v)),
                      (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v))))
                    (CD := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v))))).pt).Hom
        (F.obj i) } ≫
    F.map f
Tactic: simp only [Functor.const_obj_obj, Functor.comp_obj,
        Functor.const_obj_map, Category.id_comp, Functor.comp_map]