-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
rw :
  Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (a : B ⧸ Q) → k)
        (((Polynomial.aeval ((mk Q : (a : B) → B ⧸ Q) x) : AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
              (a : Polynomial A) → B ⧸ Q)
            P :
          B ⧸ Q) :
      k)
    (0 : k)
rw₁ :
  Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (a : B ⧸ Q) → k)
        (((Polynomial.aeval (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) x) :
                AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
              (a : Polynomial A) → B ⧸ Q)
            P :
          B ⧸ Q) :
      k)
    (0 : k)
rw₂ :
  Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (a : B ⧸ Q) → k)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) ((Polynomial.aeval x : (a : Polynomial A) → B) P) : B ⧸ Q) :
      k)
    (0 : k)
rw₃ :
  Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (a : B ⧸ Q) → k)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0) :
      k)
    (0 : k)
rw₄ :
  Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (a : B ⧸ Q) → k) 0 : k) (0 : k)
rw₅ rw₆ : Eq.{u_3 + 1} (α := k) 0 0
⊢ Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (B := B ⧸ Q)
            (AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) :
              AlgHom.{u_1, u_2, u_3} A (B ⧸ Q) k)
            (Polynomial.aeval ((mk Q : (a : B) → B ⧸ Q) x) : AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
          (a : Polynomial A) → k)
        P :
      k)
    (0 : k)

Tactic:
rw [AlgHom.comp_apply, ← algebraMap_eq, Polynomial.aeval_algebraMap_apply, this,
      map_zero, map_zero]

Premises used: Ideal.Quotient.algebraMap_eq, AlgHom.comp_apply, map_zero, Polynomial.aeval_algebraMap_apply