-- 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
P_1 : Ideal A
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
P : Ideal A
Q : Ideal B
inst_13 : Q.LiesOver P
σ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
N N' : OpenNormalSubgroup G
i : N ⟶ N'
h :
  LE.le (α := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))
    (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)
hx :
  Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
    (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    x
hx' :
  Eq (α :=
    AlgHom.{u_1, u_2, u_2} (A ⧸ P)
      (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
        Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
        (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
      (B ⧸ Q))
    (AlgHom.comp (B :=
      HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
        Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
        (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
      (let __RingHom :
        HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
            Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
            (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →+*
          B ⧸ Q :=
        quotientMap Q
          (Subsemiring.subtype
            (Subalgebra.toSubsemiring (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
          ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })
      (↑((stabilizerHom (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) P
                (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
              (a :
                  ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G))
                      (under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))) →
                (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                    under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) ≃ₐ[A ⧸ P]
                  ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                    under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
            (Subtype.mk (p := fun (x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) ↦
              Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
                (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
                  Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                  (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
                x)
              x hx)) :
        ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
            under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q →ₐ[A ⧸ P]
          ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
            under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    ((↑σ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q).comp
      (let __RingHom :
        HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
            Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
            (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →+*
          B ⧸ Q :=
        quotientMap Q
          (Subsemiring.subtype
            (Subalgebra.toSubsemiring (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
          ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ }))
obtain :
  ∀ (x : G)
    (hx :
      Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
        (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
          Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
          (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
        (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
    (hx' :
      Eq (α :=
        AlgHom.{u_1, u_2, u_2} (A ⧸ P)
          (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
            Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
            (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
          (B ⧸ Q))
        (AlgHom.comp (B :=
          HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
            Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
            (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
          (let __RingHom :
            HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →+*
              B ⧸ Q :=
            quotientMap Q
              (Subsemiring.subtype
                (Subalgebra.toSubsemiring (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
              ⋯;
          { toRingHom := __RingHom, commutes' := ⋯ })
          (↑((stabilizerHom (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) P
                    (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
                  (a :
                      ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G))
                          (under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))) →
                    (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                        under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) ≃ₐ[A ⧸ P]
                      ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                        under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
                (Subtype.mk (p := fun (x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) ↦
                  Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
                    (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
                      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
                    x)
                  (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) hx)) :
            ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q →ₐ[A ⧸ P]
              ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
        ((↑σ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q).comp
          (let __RingHom :
            HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →+*
              B ⧸ Q :=
            quotientMap Q
              (Subsemiring.subtype
                (Subalgebra.toSubsemiring (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
              ⋯;
          { toRingHom := __RingHom, commutes' := ⋯ }))),
    Eq (α :=
      AlgHom.{u_1, u_2, u_2} (A ⧸ P)
        (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)) (B :=
          Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
          (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))
        (B ⧸ Q))
      (AlgHom.comp (B :=
        HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)) (B :=
          Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
          (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))
        (let __RingHom :
          HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)) (B :=
              Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
              (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) →+*
            B ⧸ Q :=
          quotientMap Q
            (Subsemiring.subtype
              (Subalgebra.toSubsemiring (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))))
            ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ })
        (↑((stabilizerHom (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) P
                  (G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) :
                (a :
                    ↥(MulAction.stabilizer (G ⧸ (↑N'.toOpenSubgroup : Subgroup G))
                        (under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))) →
                  (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                      under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) ≃ₐ[A ⧸ P]
                    ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                      under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q)
              (Subtype.mk (p := fun (x : G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) ↦
                Membership.mem (γ := Subgroup (G ⧸ (↑N'.toOpenSubgroup : Subgroup G)))
                  (MulAction.stabilizer (G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (α :=
                    Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
                    (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))
                  x)
                ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
                    (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
                  (↑(↑(Subtype.mk (p :=
                            fun
                              (σ' :
                                ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
                                    Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                    (under
                                      (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                      Q))) ↦
                            Eq (α :=
                              AlgHom.{u_1, u_2, u_2} (A ⧸ P)
                                (HasQuotient.Quotient
                                  ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                                  Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                  (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                    Q))
                                (B ⧸ Q))
                              (AlgHom.comp (B :=
                                HasQuotient.Quotient
                                  ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                                  Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                  (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                    Q))
                                (let __RingHom :
                                  HasQuotient.Quotient
                                      ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
                                      (B :=
                                      Ideal
                                        ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                      (under
                                        (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                        Q) →+*
                                    B ⧸ Q :=
                                  quotientMap Q
                                    (Subsemiring.subtype
                                      (Subalgebra.toSubsemiring
                                        (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
                                    ⋯;
                                { toRingHom := __RingHom, commutes' := ⋯ :
                                  AlgHom.{u_1, u_2, u_2} (A ⧸ P)
                                    (HasQuotient.Quotient
                                      ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
                                      (B :=
                                      Ideal
                                        ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                      (under
                                        (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                        Q))
                                    (B ⧸ Q) })
                                (↑((stabilizerHom
                                          (under
                                            (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B
                                                ↥(↑N.toOpenSubgroup : Subgroup G)))
                                            Q)
                                          P (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
                                        (a :
                                            ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G))
                                                (under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                                  Q))) →
                                          (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                                              under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                                Q) ≃ₐ[A ⧸ P]
                                            ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                                              under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
                                      σ') :
                                  ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                                      under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                        Q →ₐ[A ⧸ P]
                                    ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                                      under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
                              ((↑σ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q).comp
                                (let __RingHom :
                                  HasQuotient.Quotient
                                      ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
                                      (B :=
                                      Ideal
                                        ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                      (under
                                        (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                        Q) →+*
                                    B ⧸ Q :=
                                  quotientMap Q
                                    (Subsemiring.subtype
                                      (Subalgebra.toSubsemiring
                                        (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
                                    ⋯;
                                { toRingHom := __RingHom, commutes' := ⋯ :
                                  AlgHom.{u_1, u_2, u_2} (A ⧸ P)
                                    (HasQuotient.Quotient
                                      ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
                                      (B :=
                                      Ideal
                                        ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                      (under
                                        (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                        Q))
                                    (B ⧸ Q) })))
                            (Subtype.mk (p := fun (x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) ↦
                              Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
                                (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
                                  Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                  (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                    Q))
                                x)
                              (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) hx)
                            hx') :
                        ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G))
                            (under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))) :
                    G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
                ⋯)) :
          ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
              under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q →ₐ[A ⧸ P]
            ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
              under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))
      ((↑σ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q).comp
        (let __RingHom :
          HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)) (B :=
              Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
              (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) →+*
            B ⧸ Q :=
          quotientMap Q
            (Subsemiring.subtype
              (Subalgebra.toSubsemiring (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))))
            ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }))
⊢ Eq (α :=
    AlgHom.{u_1, u_2, u_2} (A ⧸ P)
      (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)) (B :=
        Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
        (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))
      (B ⧸ Q))
    (AlgHom.comp (B :=
      HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)) (B :=
        Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
        (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))
      (let __RingHom :
        HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)) (B :=
            Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
            (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) →+*
          B ⧸ Q :=
        quotientMap Q
          (Subsemiring.subtype
            (Subalgebra.toSubsemiring (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))))
          ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })
      (↑((stabilizerHom (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) P
                (G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) :
              (a :
                  ↥(MulAction.stabilizer (G ⧸ (↑N'.toOpenSubgroup : Subgroup G))
                      (under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))) →
                (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                    under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) ≃ₐ[A ⧸ P]
                  ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                    under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q)
            (Subtype.mk (p := fun (x : G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) ↦
              Membership.mem (γ := Subgroup (G ⧸ (↑N'.toOpenSubgroup : Subgroup G)))
                (MulAction.stabilizer (G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (α :=
                  Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
                  (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))
                x)
              ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
                  (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
                (↑(↑(Subtype.mk (p :=
                          fun
                            (σ' :
                              ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
                                  Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                  (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                    Q))) ↦
                          Eq (α :=
                            AlgHom.{u_1, u_2, u_2} (A ⧸ P)
                              (HasQuotient.Quotient
                                ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                                Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                  Q))
                              (B ⧸ Q))
                            (AlgHom.comp (B :=
                              HasQuotient.Quotient
                                ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                                Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                  Q))
                              (let __RingHom :
                                HasQuotient.Quotient
                                    ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                                    Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                    (under
                                      (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                      Q) →+*
                                  B ⧸ Q :=
                                quotientMap Q
                                  (Subsemiring.subtype
                                    (Subalgebra.toSubsemiring
                                      (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
                                  ⋯;
                              { toRingHom := __RingHom, commutes' := ⋯ :
                                AlgHom.{u_1, u_2, u_2} (A ⧸ P)
                                  (HasQuotient.Quotient
                                    ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                                    Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                    (under
                                      (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                      Q))
                                  (B ⧸ Q) })
                              (↑((stabilizerHom
                                        (under
                                          (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B
                                              ↥(↑N.toOpenSubgroup : Subgroup G)))
                                          Q)
                                        P (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
                                      (a :
                                          ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G))
                                              (under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                                Q))) →
                                        (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                                            under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                              Q) ≃ₐ[A ⧸ P]
                                          ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                                            under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
                                    σ') :
                                ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                                    under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q →ₐ[A ⧸ P]
                                  ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                                    under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
                            ((↑σ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q).comp
                              (let __RingHom :
                                HasQuotient.Quotient
                                    ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                                    Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                    (under
                                      (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                      Q) →+*
                                  B ⧸ Q :=
                                quotientMap Q
                                  (Subsemiring.subtype
                                    (Subalgebra.toSubsemiring
                                      (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
                                  ⋯;
                              { toRingHom := __RingHom, commutes' := ⋯ :
                                AlgHom.{u_1, u_2, u_2} (A ⧸ P)
                                  (HasQuotient.Quotient
                                    ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                                    Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                    (under
                                      (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                      Q))
                                  (B ⧸ Q) })))
                          (Subtype.mk (p := fun (x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) ↦
                            Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
                              (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
                                Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                                  Q))
                              x)
                            x hx)
                          hx') :
                      ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G))
                          (under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))) :
                  G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
              ⋯)) :
        ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
            under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q →ₐ[A ⧸ P]
          ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
            under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q))
    ((↑σ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q).comp
      (let __RingHom :
        HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)) (B :=
            Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
            (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) →+*
          B ⧸ Q :=
        quotientMap Q
          (Subsemiring.subtype
            (Subalgebra.toSubsemiring (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))))
          ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ }))

Tactic:
obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x

Premises used: QuotientGroup.mk_surjective, rfl