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

Tactic:
have h : FixedPoints.subalgebra A B N'.1.1 ≤ FixedPoints.subalgebra A B N.1.1 :=
      fun x hx n ↦ hx ⟨_, i.le n.2⟩

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