-- Module: Mathlib.RingTheory.Invariant.Profinite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
inst_13 : IsInvariant A B G
P Q : Ideal B
inst_14 : P.IsPrime
inst_15 : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
B' : (G : Type u) → [inst_16 : Monoid G] → [inst_17 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
F : OpenNormalSubgroup G ⥤ Type u :=
  {
    obj := fun (N : OpenNormalSubgroup G) ↦
      { g : G ⧸ (↑N.toOpenSubgroup : Subgroup G) //
        Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
          HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) g
            (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P) },
    map := fun {N N' : OpenNormalSubgroup G} (f : N ⟶ N') ↦
      ↾fun
          (x :
            { g : G ⧸ (↑N.toOpenSubgroup : Subgroup G) //
              Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
                HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) g
                  (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P) }) ↦
        Subtype.mk (p := fun (g : G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) ↦
          Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) Q =
            HSMul.hSMul (β := Ideal ↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) g
              (Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) P))
          ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
              (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
            (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
          ⋯,
    map_id := ⋯, map_comp := ⋯ }
this : ∀ (N : OpenNormalSubgroup G), Nonempty.{u + 1} (F.obj N)
s : (j : OpenNormalSubgroup G) → F.obj j
hs : s ∈ F.sections
a : (↑((ProfiniteGrp.of G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
  Type u) :=
  (ProfiniteGrp.Hom.hom (Iso.inv (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor) :
      (a : (↑(ProfiniteGrp.limit (ProfiniteGrp.of G).diagram).toProfinite.toTop : Type u)) →
        (↑(ProfiniteGrp.of G).toProfinite.toTop : Type u))
    (Subtype.mk (p :=
      fun
        (x :
          (j :
              OpenNormalSubgroup
                (↑((ProfiniteGrp.of G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) →
            (↑((Functor.obj (ProfiniteGrp.of G).diagram j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u)) ↦
      Membership.mem (γ :=
        Subgroup
          ((j :
              OpenNormalSubgroup
                (↑((ProfiniteGrp.of G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) →
            (↑((Functor.obj (ProfiniteGrp.of G).diagram j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u)))
        (ProfiniteGrp.limitConePtAux (ProfiniteGrp.of G).diagram) x)
      (fun
          (N :
            OpenNormalSubgroup
              (↑((ProfiniteGrp.of G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) ↦
        (↑(s N) : G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
      ⋯)
N : OpenNormalSubgroup G
rw :
  (↑((ProfiniteGrp.Hom.hom (𝟙 (ProfiniteGrp.limit (J := OpenNormalSubgroup G) (ProfiniteGrp.of G).diagram)) :
              (a : (↑(ProfiniteGrp.limit (ProfiniteGrp.of G).diagram).toProfinite.toTop : Type u)) →
                (↑(ProfiniteGrp.limit (ProfiniteGrp.of G).diagram).toProfinite.toTop : Type u))
            (Subtype.mk (p :=
              fun
                (x :
                  (j : OpenNormalSubgroup G) →
                    (↑((Functor.obj (ProfiniteGrp.of G).diagram j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                      Type u)) ↦
              Membership.mem (γ :=
                Subgroup
                  ((j : OpenNormalSubgroup G) →
                    (↑((Functor.obj (ProfiniteGrp.of G).diagram j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                      Type u)))
                (ProfiniteGrp.limitConePtAux (ProfiniteGrp.of G).diagram) x)
              (fun (N : OpenNormalSubgroup G) ↦ (↑(s N) : G ⧸ (↑N.toOpenSubgroup : Subgroup G))) ⋯)) :
        (j : OpenNormalSubgroup G) → (↑((ProfiniteGrp.of G).diagram.obj j).toProfinite.toTop : Type u))
      N =
    (↑(s N) : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
⊢ (↑(((ProfiniteGrp.Hom.hom (Iso.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor) :
                (↑((ProfiniteGrp.of G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u) →ₜ*
                  (↑((ProfiniteGrp.limit (J := OpenNormalSubgroup G) (ProfiniteGrp.of G).diagram).toProfinite.toTop
                        (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) :
              (a : G) → ↥(ProfiniteGrp.limitConePtAux (ProfiniteGrp.of G).diagram))
            ((ProfiniteGrp.Hom.hom (Iso.inv (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor) :
                (a : ↥(ProfiniteGrp.limitConePtAux (ProfiniteGrp.of G).diagram)) → G)
              (Subtype.mk (p :=
                fun
                  (x :
                    (j : OpenNormalSubgroup G) →
                      (↑((Functor.obj (ProfiniteGrp.of G).diagram j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                        Type u)) ↦
                Membership.mem (γ :=
                  Subgroup
                    ((j : OpenNormalSubgroup G) →
                      (↑((Functor.obj (ProfiniteGrp.of G).diagram j).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                        Type u)))
                  (ProfiniteGrp.limitConePtAux (ProfiniteGrp.of G).diagram) x)
                (fun (N : OpenNormalSubgroup G) ↦ (↑(s N) : G ⧸ (↑N.toOpenSubgroup : Subgroup G))) ⋯))) :
        (j : OpenNormalSubgroup G) → (↑((ProfiniteGrp.of G).diagram.obj j).toProfinite.toTop : Type u))
      N =
    (↑(s N) : G ⧸ (↑N.toOpenSubgroup : Subgroup G))

Tactic:
rw [← ProfiniteGrp.comp_apply, Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id, ProfiniteGrp.comp_apply