-- Module: Mathlib.RingTheory.Invariant.Profinite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
P_1 : Ideal A
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst_13 : Q.IsPrime
inst_14 : Q.LiesOver P
inst_15 : Algebra.IsInvariant A B G
σ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
N : OpenNormalSubgroup G
this :
  IsScalarTower.{u_1, u_2, u_2} (A ⧸ P)
    (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    (B ⧸ Q)
τ :
  ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
hσ' :
  ∀
    (x :
      HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
        Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
        (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)),
    Eq (α := B ⧸ Q)
      ((algebraMap
              (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
              (B ⧸ Q) :
            (a :
                ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                  Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →
              B ⧸ Q)
          ((((stabilizerHom
                      (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) P
                      (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
                    (a :
                        ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G))
                            (Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))) →
                      (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                          Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) ≃ₐ[A ⧸ P]
                        ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                          Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
                  τ :
                AlgEquiv.{u_1, u_2, u_2} (A ⧸ P)
                  (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
                    (B := Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                    (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
                  (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
                    (B := Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                    (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))) :
              (a :
                  ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                    Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →
                ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                  Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
            x) :
        B ⧸ Q)
      ((σ : (a : B ⧸ Q) → B ⧸ Q)
          ((algebraMap
                (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
                  (B := Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                  (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
                (B ⧸ Q) :
              (a :
                  ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                    Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →
                B ⧸ Q)
            x) :
        B ⧸ Q)
x : ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
⊢ Eq (α := B ⧸ Q)
    ((AlgHom.comp (B :=
            HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
              Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
              (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
            (let __RingHom :
              HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                  Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                  (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →+*
                B ⧸ Q :=
              Ideal.quotientMap Q
                (Subsemiring.subtype
                  (Subalgebra.toSubsemiring
                    (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
                ⋯;
            { toRingHom := __RingHom, commutes' := ⋯ })
            (↑((stabilizerHom
                      (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) P
                      (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
                    (a :
                        ↥(MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G))
                            (Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))) →
                      (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                          Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) ≃ₐ[A ⧸ P]
                        ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                          Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
                  τ) :
              ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                  Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q →ₐ[A ⧸ P]
                ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                  Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) :
          (a :
              ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →
            B ⧸ Q)
        ((mk (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) :
            (a : ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) →
              ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
          x) :
      B ⧸ Q)
    (((↑σ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q).comp
            (let __RingHom :
              HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
                  Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
                  (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →+*
                B ⧸ Q :=
              Ideal.quotientMap Q
                (Subsemiring.subtype
                  (Subalgebra.toSubsemiring
                    (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))))
                ⋯;
            { toRingHom := __RingHom, commutes' := ⋯ }) :
          (a :
              ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) →
            B ⧸ Q)
        ((mk (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q) :
            (a : ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) →
              ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) ⧸
                Ideal.under (↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)
          x) :
      B ⧸ Q)

Tactic:
hσ' x

Premises used: Quotient.liftOn', Ideal.Quotient.mk, AddCon.liftOn, Submodule.Quotient.mk, Membership.mem, Subtype, FixedPoints.subalgebra, OpenNormalSubgroup.toOpenSubgroup, DFunLike.coe, OpenSubgroup.toSubgroup, Ideal.under