Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
P✝ : Ideal A
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N : OpenNormalSubgroup G
this :
  IsScalarTower (A ⧸ P)
    (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
      Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
    (B ⧸ Q)
σ' :
  (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
      Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) ≃ₐ[A ⧸ P]
    ↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸ Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q
hσ' :
  ∀
    (x :
      ↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
        Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q),
    (algebraMap
          (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
            Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
          (B ⧸ Q))
        (σ' x) =
      σ
        ((algebraMap
            (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
              Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
            (B ⧸ Q))
          x)
⊢ Nonempty ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)

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

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
P✝ : Ideal A
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N : OpenNormalSubgroup G
this :
  IsScalarTower (A ⧸ P)
    (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
      Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
    (B ⧸ Q)
τ : ↥(MulAction.stabilizer (G ⧸ ↑N.toOpenSubgroup) (Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q))
hσ' :
  ∀
    (x :
      ↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
        Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q),
    (algebraMap
          (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
            Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
          (B ⧸ Q))
        (((stabilizerHom (Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P (G ⧸ ↑N.toOpenSubgroup))
            τ)
          x) =
      σ
        ((algebraMap
            (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
              Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
            (B ⧸ Q))
          x)
⊢ Nonempty ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)