-- Mathlib/RingTheory/Invariant.lean
theorem fixed_of_fixed1_aux1 [DecidableEq (Ideal B)] :
    ∃ a b : B, (∀ g : G, g • a = a) ∧ a ∉ Q ∧
    ∀ g : G, algebraMap B (B ⧸ Q) (g • b) = algebraMap B (B ⧸ Q) (if g • Q = Q then a else 0)

Proof state:
case a
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
b : B
hbQ : 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 = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
⊢ (algebraMap B (B ⧸ Q)) (∑ b ∈ Finset.range (k + 1), ((monomial b) (f.coeff (b + j))).coeff n) = q.coeff n

Tactic:
simp only [Polynomial.coeff_monomial, Finset.sum_ite_eq', Finset.mem_range_succ_iff]

Result:
case a
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
b : B
hbQ : 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 = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
⊢ (algebraMap B (B ⧸ Q)) (if n ≤ k then f.coeff (n + j) else 0) = q.coeff n

Proof state:
case intro
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)

Tactic:
obtain ⟨b, hbP, hbQ⟩ := SetLike.not_le_iff_exists.mp h1

Result:
case intro.intro.intro
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
b : B
hbP : b ∈ P
hbQ : b ∉ Q
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)

Proof state:
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
b : B
hbQ : 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 = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
⊢ a - eval b r ∈ g • Q

Tactic:
have hr : r = ∑ i ∈ Finset.range (k + 1), Polynomial.monomial i (f.coeff (i + j)) := rfl

Result:
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
b : B
hbQ : 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 = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝¹ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ a - eval b r ∈ g • Q

Proof state:
case intro
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)

Tactic:
have h1 : ¬ P ≤ Q := by
  rw [Ideal.IsPrime.inf_le' inferInstance]
  rintro ⟨g, hg1, hg2⟩
  exact (Finset.mem_filter.mp hg1).2 (smul_eq_of_smul_le hg2)

Result:
case intro
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)

Proof state:
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
b : B
hbQ : ¬(algebraMap B (B ⧸ Q)) b = 0
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 = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr : map (algebraMap B (B ⧸ Q)) r = q
hf : (algebraMap B (B ⧸ Q)) (eval b f) = (algebraMap B (B ⧸ Q)) 0
⊢ (algebraMap B (B ⧸ Q)) (eval b r) = 0

Tactic:
rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval_map] at hf ⊢

Result:
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
b : B
hbQ : ¬(algebraMap B (B ⧸ Q)) b = 0
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 = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr : map (algebraMap B (B ⧸ Q)) r = q
hf : eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) f) = (algebraMap B (B ⧸ Q)) 0
⊢ eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) = 0