-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (goal)
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))
N : OpenNormalSubgroup G
x : ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))
hN : (↑N : Set G) ⊆ (↑(MulAction.stabilizer G (↑x : B)) : Set G)
⊢ x ∈
      HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) (↑(s N) : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
        (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P) ↔
    Membership.mem (γ := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)))
      (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) (a • P)) x
have h : Membership.mem (γ := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)))
    (Ideal.comap (F := ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)) →+* B)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) B)
        (↑(RingEquiv.symm
              ((MulSemiringAction.toRingAut (G ⧸ (↑N.toOpenSubgroup : Subgroup G))
                    ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)) :
                  (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → RingAut ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)))
                (↑(s N) : G ⧸ (↑N.toOpenSubgroup : Subgroup G)))) :
          ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)) →+* ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))))
      P)
    x ↔
  Membership.mem (γ := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)))
    (Ideal.comap (F := ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)) →+* B)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(RingEquiv.symm
              (((MulSemiringAction.toRingAut G B : MonoidHom.{u, u_2} G (RingAut B)) : (a : G) → RingAut B) a)) :
          B →+* B)
        (algebraMap (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) B))
      P)
    x
Tactic: simp only [Ideal.comap_comap, Ideal.pointwise_smul_eq_comap, ← Ideal.comap_coe
        (F := RingEquiv _ _)]