-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
i j : J
f : i ⟶ j
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' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ :
          (↑((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' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ :
            (↑((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
⊢ 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)

Tactic:
simp only [Functor.const_obj_obj, Functor.comp_obj,
        Functor.const_obj_map, Category.id_comp, Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp