-- 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 : OpenNormalSubgroup G
val : G ⧸ (↑N.toOpenSubgroup : Subgroup G)
x : G
hx :
  Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
    HSMul.hSMul (α := G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)))
      (Quot.mk (⇑(QuotientGroup.leftRel (↑N.toOpenSubgroup : Subgroup G)) : G → G → Prop) x)
      (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P)
⊢ (↑(TypeCat.Fun.toFun (X :=
          { 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) })
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun
                (x :
                  { 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) }) ↦
              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))
                ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
                    (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N.toOpenSubgroup.1)
                  (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
                ⋯))
          (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))
            (Quot.mk (⇑(QuotientGroup.leftRel (↑N.toOpenSubgroup : Subgroup G)) : G → G → Prop) x) hx)) :
      G ⧸ (↑N.toOpenSubgroup : Subgroup G)) =
    (↑((ConcreteCategory.hom (FC := TypeCat.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) })).toFun
          (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))
            (Quot.mk (⇑(QuotientGroup.leftRel (↑N.toOpenSubgroup : Subgroup G)) : G → G → Prop) x) hx)) :
      G ⧸ (↑N.toOpenSubgroup : Subgroup G))

Tactic:
rfl