-- 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 neg
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⁻¹ • 0 ∈ h⁻¹ • Q

Tactic:
rw [smul_zero, sub_zero]

Result:
case neg
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⁻¹ • Q

Proof state:
case 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
g : G
hg1 : g ∈ Finset.filter (fun g => g • Q ≠ Q) Finset.univ
hg2 : g • Q ≤ Q
⊢ False

Tactic:
exact (Finset.mem_filter.mp hg1).2 (smul_eq_of_smul_le hg2)

Result:
no goals

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
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)

Tactic:
replace hbP : ∀ g : G, g • Q ≠ Q → b ∈ g • Q :=
  fun g hg ↦ (Finset.inf_le (Finset.mem_filter.mpr ⟨Finset.mem_univ g, hg⟩) : P ≤ g • Q) hbP

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
⊢ ∃ 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.intro.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
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)
⊢ ∃ 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 k := q.natDegree

Result:
case intro.intro.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
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
⊢ ∃ 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.intro.intro.intro.intro.refine_2
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
⊢ (a - eval b r - h⁻¹ • if h • Q = Q then a else 0) ∈ h⁻¹ • Q

Tactic:
simp only [← eq_inv_smul_iff (g := h), eq_comm (a := Q)]

Result:
case intro.intro.intro.intro.intro.refine_2
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
⊢ (a - eval b r - h⁻¹ • if h⁻¹ • Q = Q then a else 0) ∈ h⁻¹ • Q