-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (goal)
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.LiesOver P
σ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
N : OpenNormalSubgroup G
⊢ Finite.{u + 1} (Functor.obj (stabilizerHomSurjectiveAuxFunctor P Q σ) N)
have dsimp : Finite.{u + 1}
  { σ' :
    ↥(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)) //
    Eq (α :=
      AlgHom.{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))
      (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))
          ({
              toRingHom :=
                Ideal.quotientMap Q
                  (↑(Subalgebra.val (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) :
                    ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) →+* B)
                  sorry,
              commutes' := sorry } :
            AlgHom.{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))
          ((↑((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)
                  σ') :
              AlgHom.{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))) :
            AlgHom.{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))) :
        AlgHom.{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))
      ((↑σ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q).comp
          {
            toRingHom :=
              Ideal.quotientMap Q
                (↑(Subalgebra.val (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) :
                  ↥(FixedPoints.subalgebra A B ↥(↑N.toOpenSubgroup : Subgroup G)) →+* B)
                sorry,
            commutes' := sorry } :
        AlgHom.{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)) }
Tactic: dsimp [stabilizerHomSurjectiveAuxFunctor]