-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Goal:
G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h :
  Eq (α :=
    G ⟶
      Functor.obj
        (forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (CC := fun (X : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
        P)
    (eta G ≫
      CategoryTheory.Functor.map
        (forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (CC := fun (X : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
        f)
    (eta G ≫
      CategoryTheory.Functor.map
        (forget₂ ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (CC := fun (X : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
        g)
x :
  (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
hf :
  Eq (α :=
    (x :
        (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)) →
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (⇑(Hom.hom f) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u))
    (⇑(Hom.hom g) : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u))
⊢ Eq (α := (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((Hom.hom f : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) x :
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((Hom.hom g : (a : (↑(completion G).toProfinite.toTop : Type u)) → (↑P.toProfinite.toTop : Type u)) x :
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))

Tactic:
apply congrFun

Premises used: congrFun