-- 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)
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)
intro :
  ∀
    (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)
            (((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)

Tactic:
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

Premises used: AlgEquiv.commutes, HasQuotient.Quotient, mul_right_inj', IsScalarTower.algebraMap_apply