∀ (P : ProfiniteGrp.{u_1}) (x x_1 : OpenNormalSubgroup ↑P.toProfinite.toTop) (x_2 : x ⟶ x_1),
  (ProfiniteGrp.Hom.hom
        ((P.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteGrp.{u_1} ProfiniteGrp.{u_1})).map x_2))
      ↑1 =
    (ProfiniteGrp.Hom.hom
        ((P.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteGrp.{u_1} ProfiniteGrp.{u_1})).map x_2))
      ↑1