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.LiesOver P
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N N' : OpenNormalSubgroup G
i : N ⟶ N'
h : FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup ≤ FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup
x : G ⧸ ↑N.toOpenSubgroup
hx : x ∈ MulAction.stabilizer (G ⧸ ↑N.toOpenSubgroup) (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
hx' :
  (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P (G ⧸ ↑N.toOpenSubgroup))
          ⟨x, hx⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })
⊢ (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup)) Q) P (G ⧸ ↑N'.toOpenSubgroup))
          ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑⟨⟨x, hx⟩, hx'⟩, ⋯⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })

Tactic:
obtain ⟨x, rfl⟩ := QuotientGroup.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.LiesOver P
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N N' : OpenNormalSubgroup G
i : N ⟶ N'
h : FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup ≤ FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup
x : G
hx : ↑x ∈ MulAction.stabilizer (G ⧸ ↑N.toOpenSubgroup) (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
hx' :
  (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P (G ⧸ ↑N.toOpenSubgroup))
          ⟨↑x, hx⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })
⊢ (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup)) Q) P (G ⧸ ↑N'.toOpenSubgroup))
          ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑⟨⟨↑x, hx⟩, hx'⟩, ⋯⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })