-- 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
X Y Z : OpenNormalSubgroup G
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (val : G ⧸ (↑X.toOpenSubgroup : Subgroup G)) (x : G)
    (hx :
      Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
        HSMul.hSMul (α := G ⧸ (↑X.toOpenSubgroup : Subgroup G)) (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G)))
          (Quot.mk (⇑(QuotientGroup.leftRel (↑X.toOpenSubgroup : Subgroup G)) : G → G → Prop) x)
          (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P)),
    Eq (α := G ⧸ (↑Z.toOpenSubgroup : Subgroup G))
      (↑(TypeCat.Fun.toFun (X :=
            { g : G ⧸ (↑X.toOpenSubgroup : Subgroup G) //
              Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
                HSMul.hSMul (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) g
                  (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P) })
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun
                  (x :
                    { g : G ⧸ (↑X.toOpenSubgroup : Subgroup G) //
                      Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
                        HSMul.hSMul (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) g
                          (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P) }) ↦
                Subtype.mk (p := fun (g : G ⧸ (↑Z.toOpenSubgroup : Subgroup G)) ↦
                  Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) Q =
                    HSMul.hSMul (β := Ideal ↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) g
                      (Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) P))
                  ((QuotientGroup.map (↑X.toOpenSubgroup : Subgroup G) Z.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
                      (a : G ⧸ (↑X.toOpenSubgroup : Subgroup G)) → G ⧸ Z.toOpenSubgroup.1)
                    (↑x : G ⧸ (↑X.toOpenSubgroup : Subgroup G)))
                  ⋯))
            (Subtype.mk (p := fun (g : G ⧸ (↑X.toOpenSubgroup : Subgroup G)) ↦
              Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
                HSMul.hSMul (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) g
                  (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P))
              (Quot.mk (⇑(QuotientGroup.leftRel (↑X.toOpenSubgroup : Subgroup G)) : G → G → Prop) x) hx)) :
        G ⧸ (↑Z.toOpenSubgroup : Subgroup G))
      (↑(TypeCat.Fun.toFun (X :=
            { g : G ⧸ (↑X.toOpenSubgroup : Subgroup G) //
              Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
                HSMul.hSMul (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) g
                  (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P) })
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y :=
                { g : G ⧸ (↑Y.toOpenSubgroup : Subgroup G) //
                  Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) Q =
                    HSMul.hSMul (β := Ideal ↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) g
                      (Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) P) })
                (↾fun
                    (x :
                      { g : G ⧸ (↑X.toOpenSubgroup : Subgroup G) //
                        Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
                          HSMul.hSMul (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) g
                            (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P) }) ↦
                  Subtype.mk (p := fun (g : G ⧸ (↑Y.toOpenSubgroup : Subgroup G)) ↦
                    Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) Q =
                      HSMul.hSMul (β := Ideal ↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) g
                        (Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) P))
                    ((QuotientGroup.map (↑X.toOpenSubgroup : Subgroup G) Y.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
                        (a : G ⧸ (↑X.toOpenSubgroup : Subgroup G)) → G ⧸ Y.toOpenSubgroup.1)
                      (↑x : G ⧸ (↑X.toOpenSubgroup : Subgroup G)))
                    ⋯)
                (↾fun
                    (x :
                      { g : G ⧸ (↑Y.toOpenSubgroup : Subgroup G) //
                        Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) Q =
                          HSMul.hSMul (β := Ideal ↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) g
                            (Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) P) }) ↦
                  Subtype.mk (p := fun (g : G ⧸ (↑Z.toOpenSubgroup : Subgroup G)) ↦
                    Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) Q =
                      HSMul.hSMul (β := Ideal ↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) g
                        (Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) P))
                    ((QuotientGroup.map (↑Y.toOpenSubgroup : Subgroup G) Z.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
                        (a : G ⧸ (↑Y.toOpenSubgroup : Subgroup G)) → G ⧸ Z.toOpenSubgroup.1)
                      (↑x : G ⧸ (↑Y.toOpenSubgroup : Subgroup G)))
                    ⋯)))
            (Subtype.mk (p := fun (g : G ⧸ (↑X.toOpenSubgroup : Subgroup G)) ↦
              Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
                HSMul.hSMul (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) g
                  (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P))
              (Quot.mk (⇑(QuotientGroup.leftRel (↑X.toOpenSubgroup : Subgroup G)) : G → G → Prop) x) hx)) :
        G ⧸ (↑Z.toOpenSubgroup : Subgroup G))
⊢ Eq.{u + 1} (α :=
    { g : G ⧸ (↑X.toOpenSubgroup : Subgroup G) //
        Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
          HSMul.hSMul (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) g
            (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P) } ⟶
      { g : G ⧸ (↑Z.toOpenSubgroup : Subgroup G) //
        Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) Q =
          HSMul.hSMul (β := Ideal ↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) g
            (Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) P) })
    (↾fun
        (x :
          { g : G ⧸ (↑X.toOpenSubgroup : Subgroup G) //
            Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
              HSMul.hSMul (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) g
                (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P) }) ↦
      Subtype.mk (p := fun (g : G ⧸ (↑Z.toOpenSubgroup : Subgroup G)) ↦
        Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) Q =
          HSMul.hSMul (β := Ideal ↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) g
            (Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) P))
        ((QuotientGroup.map (↑X.toOpenSubgroup : Subgroup G) Z.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
            (a : G ⧸ (↑X.toOpenSubgroup : Subgroup G)) → G ⧸ Z.toOpenSubgroup.1)
          (↑x : G ⧸ (↑X.toOpenSubgroup : Subgroup G)))
        ⋯)
    (CategoryStruct.comp (Y :=
      { g : G ⧸ (↑Y.toOpenSubgroup : Subgroup G) //
        Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) Q =
          HSMul.hSMul (β := Ideal ↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) g
            (Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) P) })
      (↾fun
          (x :
            { g : G ⧸ (↑X.toOpenSubgroup : Subgroup G) //
              Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) Q =
                HSMul.hSMul (β := Ideal ↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) g
                  (Ideal.under (↥(B' ↥(↑X.toOpenSubgroup : Subgroup G))) P) }) ↦
        Subtype.mk (p := fun (g : G ⧸ (↑Y.toOpenSubgroup : Subgroup G)) ↦
          Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) Q =
            HSMul.hSMul (β := Ideal ↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) g
              (Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) P))
          ((QuotientGroup.map (↑X.toOpenSubgroup : Subgroup G) Y.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
              (a : G ⧸ (↑X.toOpenSubgroup : Subgroup G)) → G ⧸ Y.toOpenSubgroup.1)
            (↑x : G ⧸ (↑X.toOpenSubgroup : Subgroup G)))
          ⋯)
      (↾fun
          (x :
            { g : G ⧸ (↑Y.toOpenSubgroup : Subgroup G) //
              Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) Q =
                HSMul.hSMul (β := Ideal ↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) g
                  (Ideal.under (↥(B' ↥(↑Y.toOpenSubgroup : Subgroup G))) P) }) ↦
        Subtype.mk (p := fun (g : G ⧸ (↑Z.toOpenSubgroup : Subgroup G)) ↦
          Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) Q =
            HSMul.hSMul (β := Ideal ↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) g
              (Ideal.under (↥(B' ↥(↑Z.toOpenSubgroup : Subgroup G))) P))
          ((QuotientGroup.map (↑Y.toOpenSubgroup : Subgroup G) Z.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
              (a : G ⧸ (↑Y.toOpenSubgroup : Subgroup G)) → G ⧸ Z.toOpenSubgroup.1)
            (↑x : G ⧸ (↑Y.toOpenSubgroup : Subgroup G)))
          ⋯))

Tactic:
ext ⟨⟨x⟩, hx⟩