-- 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
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
inst_13 : IsInvariant A B G
P Q : Ideal B
inst_14 : P.IsPrime
inst_15 : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
B' : (G : Type u) → [inst_16 : Monoid G] → [inst_17 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
N N' : OpenNormalSubgroup G
f : N ⟶ N'
h : B' ↥(↑N'.toOpenSubgroup : Subgroup G) ≤ B' ↥(↑N.toOpenSubgroup : Subgroup G)
x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)
hx :
  Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
    HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) x
      (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P)
obtain :
  ∀ (x : G)
    (hx :
      Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
        HSMul.hSMul (α := G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)))
          (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P)),
    Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) Q =
      HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β := Ideal ↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G)))
        ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
              (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
            (↑(Subtype.mk (p := fun (g : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) ↦
                  Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
                    HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) g
                      (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P))
                  (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) hx) :
              G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
          HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
        (Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) P)
⊢ Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) Q =
    HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β := Ideal ↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G)))
      ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
            (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
          (↑(Subtype.mk (p := fun (g : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) ↦
                Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
                  HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) g
                    (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P))
                x hx) :
            G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
        HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
      (Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) P)

Tactic:
obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x

Premises used: QuotientGroup.mk_surjective, rfl