-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
X' X : GrpCat
Y : ProfiniteGrp.{u_1}
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1) →ₜ*
          (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1))
        (CC := fun (X : ProfiniteGrp.{u_1}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1))
        GrpCat (FD := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := GrpCat.carrier))
      Y
⊢ Eq (α :=
    X' ⟶
      Functor.obj
        (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
              Type u_1) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
              Type u_1))
          (CC := fun (X : ProfiniteGrp.{u_1}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1))
          GrpCat (FD := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := GrpCat.carrier))
        Y)
    (eta X' ≫
      CategoryTheory.Functor.map
        (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
              Type u_1) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
              Type u_1))
          (CC := fun (X : ProfiniteGrp.{u_1}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1))
          GrpCat (FD := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := GrpCat.carrier))
        (((homEquiv X' Y).symm : (a : X' ⟶ (forget₂ ProfiniteGrp.{u_1} GrpCat).obj Y) → profiniteCompletion.obj X' ⟶ Y)
          (f ≫ g)))
    (eta X' ≫
      CategoryTheory.Functor.map
        (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
              Type u_1) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
              Type u_1))
          (CC := fun (X : ProfiniteGrp.{u_1}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
            Type u_1))
          GrpCat (FD := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := GrpCat.carrier))
        (profiniteCompletion.map f ≫
          ((homEquiv X Y).symm : (a : X ⟶ (forget₂ ProfiniteGrp.{u_1} GrpCat).obj Y) → profiniteCompletion.obj X ⟶ Y)
            g))

Tactic:
simp [homEquiv]

Premises used: ProfiniteGrp.ProfiniteCompletion.homEquiv