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

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

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