-- 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:
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)
⊢ ∃ 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 ⟨_⟩ := nonempty_fintype G

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
⊢ ∃ 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:
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
⊢ ∃ 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:
let P := ((Finset.univ : Finset G).filter (fun g ↦ g • Q ≠ Q)).inf (fun g ↦ g • Q)

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
⊢ ∃ 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
⊢ eval b r ∈ Q

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, ← Ideal.Quotient.algebraMap_eq] at hbQ ⊢

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 b f = 0
⊢ (algebraMap B (B ⧸ Q)) (eval b r) = 0

Proof state:
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
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ 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:
let f := MulSemiringAction.charpoly G b

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
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
⊢ ∃ 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:
case pos
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
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
hh : h⁻¹ • Q = Q
⊢ a - eval b r - h⁻¹ • a ∈ h⁻¹ • Q

Tactic:
rwa [ha, sub_sub_cancel_left, hh, Q.neg_mem_iff]

Result:
no goals

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
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ eval b (∑ k ∈ Finset.range k, (monomial (k + 1)) (f.coeff (k + 1 + j))) ∈ g • Q

Tactic:
simp only [ ← Polynomial.monomial_mul_X]

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))
⊢ eval b (∑ x ∈ Finset.range k, (monomial x) (f.coeff (x + 1 + j)) * X) ∈ g • Q