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)
τ : ↥(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)

Tactic:
refine ⟨τ, ?_⟩

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)
⊢ (let __RingHom := Ideal.quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P (G ⧸ ↑N.toOpenSubgroup))
          τ) =
    (↑σ).comp
      (let __RingHom := Ideal.quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })