-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
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 (α := profiniteCompletion.obj X' ⟶ Y)
    (((homEquiv X' Y).symm : (a : X' ⟶ (forget₂ ProfiniteGrp.{u_1} GrpCat).obj Y) → profiniteCompletion.obj X' ⟶ Y)
        (f ≫ g) :
      profiniteCompletion.obj X' ⟶ Y)
    (profiniteCompletion.map f ≫
        ((homEquiv X Y).symm : (a : X ⟶ (forget₂ ProfiniteGrp.{u_1} GrpCat).obj Y) → profiniteCompletion.obj X ⟶ Y) g :
      profiniteCompletion.obj X' ⟶ Y)
have h : 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: apply lift_unique