-- 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_1 : ∀ (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)))
      ⋯)
this :
  ∀ (N : OpenNormalSubgroup G),
    (↑a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) = (↑(s N) : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
⊢ ∃ (g : G), Q = g • P

Tactic:
⟨a, ?_⟩

Premises used: Exists.intro