-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
P : ProfiniteGrp.{u}
f : completion G ⟶ P
⊢ (fun
          (f :
            G ⟶
              GrpCat.of
                (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) ↦
        lift f)
      ((fun (f : completion G ⟶ 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 :
            G ⟶
              GrpCat.of
                (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)))
        f) =
    f
have 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))
      ((fun
            (f :
              G ⟶
                GrpCat.of
                  (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) ↦
          lift f)
        ((fun (f : completion G ⟶ 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 :
              G ⟶
                GrpCat.of
                  (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)))
          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))
      f)
Tactic: apply lift_unique