-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
val : Fintype G
P : Ideal B := Finset.inf {g : G | g • Q ≠ Q} fun (g : G) ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : ¬Eq (α := B ⧸ Q) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b : B ⧸ Q) (0 : B ⧸ Q)
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq :
  map (algebraMap B (B ⧸ Q)) f =
    HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i : (a : B) → B[X]) (f.coeff (i + j))
hr : map (algebraMap B (B ⧸ Q)) r = q
hf :
  Eq (α := B ⧸ Q) (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) f) : B ⧸ Q)
    ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 : B ⧸ Q)
rwa :
  ∀
    (hf :
      Eq (α := B ⧸ Q) (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) f) : B ⧸ Q)
        (0 : B ⧸ Q)),
    Eq (α := B ⧸ Q) (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) r) : B ⧸ Q)
      (0 : B ⧸ Q)
rwa₁ :
  ∀
    (hf :
      Eq (α := B ⧸ Q)
        (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b)
            (HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q) :
          B ⧸ Q)
        (0 : B ⧸ Q)),
    Eq (α := B ⧸ Q) (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) r) : B ⧸ Q)
      (0 : B ⧸ Q)
rwa₂ :
  ∀
    (hf :
      Eq (α := B ⧸ Q)
        (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b)
            (HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) *
              map (algebraMap B (B ⧸ Q)) r) :
          B ⧸ Q)
        (0 : B ⧸ Q)),
    Eq (α := B ⧸ Q) (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) r) : B ⧸ Q)
      (0 : B ⧸ Q)
rwa₃ :
  ∀
    (hf :
      HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q)
          (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b)
              (HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f))) :
            B ⧸ Q)
          (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) r) : B ⧸ Q) =
        0),
    Eq (α := B ⧸ Q) (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) r) : B ⧸ Q)
      (0 : B ⧸ Q)
⊢ Eq (α := B ⧸ Q) (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) r) : B ⧸ Q) (0 : B ⧸ Q)
have rwa₄ : ∀
  (hf :
    HMul.hMul (β := B ⧸ Q)
        (HPow.hPow (α := B ⧸ Q) (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) X : B ⧸ Q)
          (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)))
        (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) r) : B ⧸ Q) =
      0),
  Eq (α := B ⧸ Q) (eval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b) (map (algebraMap B (B ⧸ Q)) r) : B ⧸ Q) (0 : B ⧸ Q)
Tactic: rwa [map_zero, hq, ← hr, Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_X,
      mul_eq_zero, or_iff_right (pow_ne_zero _ hbQ)] at hf
Cleared hypotheses: hf