-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
b : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((Ideal.Quotient.stabilizerHom Q P G :
                  MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                    (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
              g :
            AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
          (a : B ⧸ Q) → B ⧸ Q)
        b =
      b
intro :
  ∀ (val : Fintype G),
    Eq (α := L) ((f : (a : L) → L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L) : L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)
intro₁ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
intro₂ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₃ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₄ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q))
    (M : A[X]) (key : Eq (α := B[X]) (map (algebraMap A B) M) (MulSemiringAction.charpoly G b)),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₅ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q))
    (M : A[X])
    (key :
      Eq (α := (B ⧸ Q)[X]) (map (algebraMap B (B ⧸ Q)) (map (algebraMap A B) M))
        (map (algebraMap B (B ⧸ Q)) (MulSemiringAction.charpoly G b))),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₆ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q))
    (M : A[X])
    (key :
      Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
        (∏ i : G,
          map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₇ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q))
    (M : A[X])
    (key :
      Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
        (∏ i : G,
          map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X]))))
    (key₀ :
      ∀ (g : G),
        map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
          if g • Q = Q then
            HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
              ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
          else X),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₈ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q))
    (M : A[X])
    (key₀ :
      ∀ (g : G),
        map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
          if g • Q = Q then
            HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
              ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
          else X)
    (key :
      map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M) =
        HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
              ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X]) ^
            Finset.card.{u_3} (α := G) {x : G | x • Q = Q} *
          HPow.hPow (α := (B ⧸ Q)[X]) X (Finset.card.{u_3} (α := G) {x : G | ¬x • Q = Q})),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₉ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q))
    (M : A[X])
    (key₀ :
      ∀ (g : G),
        map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
          if g • Q = Q then
            HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
              ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
          else X)
    (key :
      Eq (α := L[X])
        (map.{u_2, u_5} (R := B ⧸ Q) (algebraMap (B ⧸ Q) L)
          (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M)))
        (map (algebraMap (B ⧸ Q) L)
          (HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
                ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X]) ^
              Finset.card.{u_3} (α := G) {x : G | x • Q = Q} *
            HPow.hPow (α := (B ⧸ Q)[X]) X (Finset.card.{u_3} (α := G) {x : G | ¬x • Q = Q})))),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₁₀ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q))
    (M : A[X])
    (key₀ :
      ∀ (g : G),
        map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
          if g • Q = Q then
            HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
              ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
          else X)
    (key :
      map (algebraMap K L) (map (R := A ⧸ P) (algebraMap (A ⧸ P) K) (map (algebraMap A (A ⧸ P)) M)) =
        HSub.hSub (α := L[X]) (β := L[X]) X
              ((C : (a : L) → L[X])
                  ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
                    ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀) : B ⧸ Q)) :
                L[X]) ^
            Finset.card.{u_3} (α := G) {x : G | x • Q = Q} *
          HPow.hPow (α := L[X]) X (Finset.card.{u_3} (α := G) {x : G | ¬x • Q = Q})),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₁₁ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q))
    (M : A[X])
    (key₀ :
      ∀ (g : G),
        map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
          if g • Q = Q then
            HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
              ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
          else X)
    (key :
      Eq (α := L)
        ((f : (a : L) → L)
            ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀) : B ⧸ Q) : L) :
          L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀) : B ⧸ Q) : L)),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₁₂ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q))
    (M : A[X])
    (key₀ :
      ∀ (g : G),
        map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
          if g • Q = Q then
            HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
              ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
          else X)
    (key :
      HMul.hMul (α := L) (β := L)
          ((f : (a : L) → L)
              ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q) : L) :
            L)
          ((f : (a : L) → L)
              ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L) :
            L) =
        HMul.hMul (α := L) (β := L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q) : L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₁₃ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (b : B) (M : A[X]) (a : A)
    (ha1 : ∀ (g : G), HSMul.hSMul (β := B) g ((algebraMap A B : (a : A) → B) a : B) = (algebraMap A B : (a : A) → B) a)
    (ha2 : ((algebraMap A B : (a : A) → B) a : B) ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q)
              (if g • Q = Q then HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) a : B) b₀ else 0) :
            B ⧸ Q))
    (key₀ :
      ∀ (g : G),
        map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
          if g • Q = Q then
            HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
              ((C : (a : B ⧸ Q) → (B ⧸ Q)[X])
                  ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q)
                    (HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) a : B) b₀)) :
                (B ⧸ Q)[X])
          else X)
    (key :
      HMul.hMul (α := L) (β := L)
          ((f : (a : L) → L)
              ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
                  ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) ((algebraMap A B : (a : A) → B) a) : B ⧸ Q) :
                L) :
            L)
          ((f : (a : L) → L)
              ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L) :
            L) =
        HMul.hMul (α := L) (β := L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) ((algebraMap A B : (a : A) → B) a) : B ⧸ Q) :
            L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)),
    Eq (α := L)
      ((f : (a : L) → L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
              (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
            L) :
        L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
        L)
intro₁₄ :
  ∀ (val : Fintype G) (b₀ : B)
    (hx :
      ∀ (g : ↥(MulAction.stabilizer G Q)),
        Eq (α := B ⧸ Q)
          (((((Ideal.Quotient.stabilizerHom Q P G :
                        MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                          (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                      (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                    g :
                  AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
                (a : B ⧸ Q) → B ⧸ Q)
              ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
            B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q))
    (b : B) (M : A[X]) (a : A)
    (ha1 : ∀ (g : G), HSMul.hSMul (β := B) g ((algebraMap A B : (a : A) → B) a : B) = (algebraMap A B : (a : A) → B) a)
    (ha2 : ((algebraMap A B : (a : A) → B) a : B) ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q)
              (if g • Q = Q then HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) a : B) b₀ else 0) :
            B ⧸ Q))
    (key₀ :
      ∀ (g : G),
        map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
          if g • Q = Q then
            HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
              ((C : (a : B ⧸ Q) → (B ⧸ Q)[X])
                  ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q)
                    (HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) a : B) b₀)) :
                (B ⧸ Q)[X])
          else X)
    (key :
      HMul.hMul (α := L) (β := L)
          ((algebraMap K L : (a : K) → L)
              ((algebraMap (A ⧸ P) K : (a : A ⧸ P) → K) ((algebraMap A (A ⧸ P) : (a : A) → A ⧸ P) a : A ⧸ P) : K) :
            L)
          ((f : (a : L) → L)
              ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L) :
            L) =
        HMul.hMul (α := L) (β := L)
          ((algebraMap K L : (a : K) → L)
              ((algebraMap (A ⧸ P) K : (a : A ⧸ P) → K) ((algebraMap A (A ⧸ P) : (a : A) → A ⧸ P) a : A ⧸ P) : K) :
            L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)),
    Ne.{u_5 + 1} (α := L)
      ((algebraMap K L : (a : K) → L)
          ((algebraMap (A ⧸ P) K : (a : A ⧸ P) → K) ((algebraMap A (A ⧸ P) : (a : A) → A ⧸ P) a : A ⧸ P) : K) :
        L)
      (0 : L)
⊢ Eq (α := L) ((f : (a : L) → L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L) : L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)

Tactic:
classical
  cases nonempty_fintype G
  obtain ⟨b₀, rfl⟩ := Ideal.Quotient.mk_surjective b
  rw [← Ideal.Quotient.algebraMap_eq]
  obtain ⟨a, b, ha1, ha2, hb⟩ := fixed_of_fixed1_aux2 G Q b₀ (fun g hg ↦ hx ⟨g, hg⟩)
  obtain ⟨M, key⟩ := (mem_lifts _).mp (Algebra.IsInvariant.charpoly_mem_lifts A B G b)
  replace key := congrArg (map (algebraMap B (B ⧸ Q))) key
  rw [map_map, ← algebraMap_eq, algebraMap_eq A (A ⧸ P) (B ⧸ Q),
      ← map_map, MulSemiringAction.charpoly, Polynomial.map_prod] at key
  have key₀ : ∀ g : G, (X - C (g • b)).map (algebraMap B (B ⧸ Q)) =
      if g • Q = Q then X - C (algebraMap B (B ⧸ Q) (a * b₀)) else X := by
    intro g
    rw [Polynomial.map_sub, map_X, map_C, hb]
    split_ifs
    · rfl
    · rw [map_zero, map_zero, sub_zero]
  simp only [key₀, Finset.prod_ite, Finset.prod_const] at key
  replace key := congrArg (map (algebraMap (B ⧸ Q) L)) key
  rw [map_map, ← algebraMap_eq, algebraMap_eq (A ⧸ P) K L,
      ← map_map, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_pow, Polynomial.map_sub,
      map_X, map_C] at key
  replace key := fixed_of_fixed1_aux3 key f (Finset.card_ne_zero_of_mem
    (Finset.mem_filter.mpr ⟨Finset.mem_univ 1, one_smul G Q⟩))
  simp only [map_mul] at key
  obtain ⟨a, rfl⟩ := Algebra.IsInvariant.isInvariant (A := A) a ha1
  rwa [← algebraMap_apply A B (B ⧸ Q), algebraMap_apply A (A ⧸ P) (B ⧸ Q),
      ← algebraMap_apply, algebraMap_apply (A ⧸ P) K L, f.commutes, mul_right_inj'] at key
  rwa [← algebraMap_apply, algebraMap_apply (A ⧸ P) (B ⧸ Q) L,
      ← algebraMap_apply A (A ⧸ P) (B ⧸ Q), algebraMap_apply A B (B ⧸ Q),
      Ne, algebraMap_eq_zero_iff, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Polynomial.map_mul, Ideal.Quotient.algebraMap_eq, AlgEquiv.commutes, Polynomial.map_pow, Polynomial.map_X, Ne, Finset.prod_const, MulSemiringAction.charpoly, Ideal.Quotient.eq_zero_iff_mem, Polynomial.map_prod, Ideal.Quotient.mk_surjective, HasQuotient.Quotient, map_mul, nonempty_fintype, Finset.prod_ite, IsScalarTower.algebraMap_eq, Polynomial.map_sub, mul_right_inj', Polynomial.map_C, Polynomial.map_map, IsScalarTower.algebraMap_apply, rfl, FaithfulSMul.algebraMap_eq_zero_iff