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

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

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