-- 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
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' := ⋯ }))
g :
  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)
H :
  ∀ (g : ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))),
    Eq (α := 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) :
            (a :
                ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                  under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) →
              B ⧸ Q)
          ((mk (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) :
              (a : ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) →
                ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                  under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q)
            g) :
        B ⧸ 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' := ⋯ }) :
            (a :
                ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                  under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) →
              B ⧸ Q)
          ((mk (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) :
              (a : ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) →
                ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                  under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q)
            g) :
        B ⧸ Q)
⊢ Eq (α := 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) :
          (a :
              ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) →
            B ⧸ Q)
        g :
      B ⧸ 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' := ⋯ }) :
          (a :
              ↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G)) ⧸
                under (↥(FixedPoints.subalgebra A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) →
            B ⧸ Q)
        g :
      B ⧸ Q)

Tactic:
obtain ⟨g, rfl⟩ := Ideal.Quotient.mk_surjective g

Premises used: Ideal.Quotient.mk_surjective, rfl