-- 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.IsPrime
inst_14 : Q.LiesOver P
inst_15 : Algebra.IsInvariant A B G
σ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
N : OpenNormalSubgroup G
this :
  IsScalarTower.{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)))
      (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    (B ⧸ Q)
obtain :
  ∀
    (σ' :
      AlgEquiv.{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)))
          (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
        (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)))
          (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)))
    (hσ' :
      ∀
        (x :
          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)))
            (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)),
        Eq (α := B ⧸ Q)
          ((algebraMap
                  (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)))
                    (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
                  (B ⧸ Q) :
                (a :
                    ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                      Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →
                  B ⧸ Q)
              ((σ' :
                  (a :
                      ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                        Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →
                    ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                      Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
                x) :
            B ⧸ Q)
          ((σ : (a : B ⧸ Q) → B ⧸ Q)
              ((algebraMap
                    (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)))
                      (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
                    (B ⧸ Q) :
                  (a :
                      ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                        Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →
                    B ⧸ Q)
                x) :
            B ⧸ Q)),
    Nonempty.{u + 1} (Functor.obj (stabilizerHomSurjectiveAuxFunctor P Q σ) N)
⊢ Nonempty.{u + 1} (Functor.obj (stabilizerHomSurjectiveAuxFunctor P Q σ) N)

Tactic:
obtain ⟨σ', hσ'⟩ := Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under (G ⧸ N.1.1) P
    (Q.under (FixedPoints.subalgebra A B N.1.1)) σ

Premises used: Membership.mem, Subtype, Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under, HasQuotient.Quotient, FixedPoints.subalgebra, OpenNormalSubgroup.toOpenSubgroup, OpenSubgroup.toSubgroup, Ideal.under