Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: case mk
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
X✝ Y✝ Z✝ : OpenNormalSubgroup G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
val✝ : G ⧸ ↑X✝.toOpenSubgroup
x : G
hx :
  Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x ∈
    MulAction.stabilizer (G ⧸ ↑X✝.toOpenSubgroup) (under (↥(FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup)) Q)
hx' :
  (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup)) Q) P (G ⧸ ↑X✝.toOpenSubgroup))
          ⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })
⊢ ↑↑((ConcreteCategory.hom
              (↾fun x ↦
                ⟨⟨(QuotientGroup.map (↑X✝.toOpenSubgroup) Z✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩)).toFun
          ⟨⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩, hx'⟩) =
    ↑↑((ConcreteCategory.hom
              ((↾fun x ↦
                  ⟨⟨(QuotientGroup.map (↑X✝.toOpenSubgroup) Y✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩) ≫
                ↾fun x ↦
                  ⟨⟨(QuotientGroup.map (↑Y✝.toOpenSubgroup) Z✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩)).toFun
          ⟨⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩, hx'⟩)

Tactic:
;

Goal state after:
case mk
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
X✝ Y✝ Z✝ : OpenNormalSubgroup G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
val✝ : G ⧸ ↑X✝.toOpenSubgroup
x : G
hx :
  Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x ∈
    MulAction.stabilizer (G ⧸ ↑X✝.toOpenSubgroup) (under (↥(FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup)) Q)
hx' :
  (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup)) Q) P (G ⧸ ↑X✝.toOpenSubgroup))
          ⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })
⊢ ↑↑((ConcreteCategory.hom
              (↾fun x ↦
                ⟨⟨(QuotientGroup.map (↑X✝.toOpenSubgroup) Z✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩)).toFun
          ⟨⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩, hx'⟩) =
    ↑↑((ConcreteCategory.hom
              ((↾fun x ↦
                  ⟨⟨(QuotientGroup.map (↑X✝.toOpenSubgroup) Y✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩) ≫
                ↾fun x ↦
                  ⟨⟨(QuotientGroup.map (↑Y✝.toOpenSubgroup) Z✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩)).toFun
          ⟨⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩, hx'⟩)