awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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))
n : ℕ
hn : ¬n ≤ k
neg : 0 = q.coeff n
neg₁ : q.coeff n = 0
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 = q.coeff n
have neg₂ : Eq.{u_2 + 1} (α := B ⧸ Q) 0 0
Tactic: rw [map_zero, eq_comm, Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_not_ge hn)]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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 : 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))
⊢ ∃ (a : B) (b : B),
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧
        ∀ (g : G),
          Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
            ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
have hr : map (algebraMap B (B ⧸ Q)) r = q
Tactic: have hr : r.map (algebraMap B (B ⧸ Q)) = q := by
    ext n
    rw [Polynomial.coeff_map, Polynomial.finsetSum_coeff]
    simp only [Polynomial.coeff_monomial, Finset.sum_ite_eq', Finset.mem_range_succ_iff]
    split_ifs with hn
    · rw [← Polynomial.coeff_map, hq, Polynomial.coeff_X_pow_mul]
    · rw [map_zero, eq_comm, Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_not_ge hn)]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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 : 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
⊢ ∃ (a : B) (b : B),
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧
        ∀ (g : G),
          Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
            ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
have hf : eval b f = 0
Tactic: have hf : f.eval b = 0 := MulSemiringAction.eval_charpoly G b
-- 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 : 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 : eval b f = 0
⊢ eval b r ∈ Q
have rw : ∀ (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),
  let 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),
    let j := rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f);
    let k := q.natDegree;
    let 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 : eval b f = 0),
      Eq (α := B ⧸ Q) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) (eval b r) : B ⧸ Q) (0 : B ⧸ Q)
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, ← Ideal.Quotient.algebraMap_eq] at hbQ ⊢
Cleared hypotheses: hbQ, hbP, f, q, hq, hq0, j, k, r, hr, hf
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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 : eval b f = 0
⊢ Eq (α := B ⧸ Q) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) (eval b r) : B ⧸ Q) (0 : B ⧸ Q)
have hf₁ : Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (eval b f) : B ⧸ Q)
  ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 : B ⧸ Q)
Tactic: replace hf := congrArg (algebraMap B (B ⧸ Q)) hf
Cleared hypotheses: hf
-- 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) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (eval b f) : B ⧸ Q)
    ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 : B ⧸ Q)
⊢ Eq (α := B ⧸ Q) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) (eval b r) : B ⧸ Q) (0 : B ⧸ Q)
have rw : ∀
  (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)),
  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: rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval_map] at hf ⊢
Cleared hypotheses: hf
-- 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)
⊢ 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 :
    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)
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
-- 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)
⊢ 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 :
    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)
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
-- 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)
⊢ 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 :
    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)
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
-- 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)
⊢ 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) (β := 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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 : 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 : eval b f = 0
⊢ ∃ (a : B) (b : B),
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧
        ∀ (g : G),
          Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
            ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
have hr₁ : eval b r ∈ Q
Tactic: have hr : r.eval b ∈ Q := by
    rw [← Ideal.Quotient.eq_zero_iff_mem, ← Ideal.Quotient.algebraMap_eq] at hbQ ⊢
    replace hf := congrArg (algebraMap B (B ⧸ Q)) hf
    rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval_map] at hf ⊢
    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
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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 : 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_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
⊢ ∃ (a : B) (b : B),
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧
        ∀ (g : G),
          Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
            ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
have ha : ∀ (g : G), g • a = a
Tactic: have ha : ∀ g : G, g • a = a := MulSemiringAction.smul_coeff_charpoly b j
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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 : 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_1 : 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
have hr₁ : r = ∑ i ∈ Finset.range (k + 1), (monomial i : (a : B) → B[X]) (f.coeff (i + j))
Tactic: have hr : r = ∑ i ∈ Finset.range (k + 1), Polynomial.monomial i (f.coeff (i + j)) := rfl
-- 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 : 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_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr_2 : 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 : (a : B) → B[X]) (f.coeff (i + j))
⊢ a - eval b r ∈ g • Q
have rw : eval b (∑ k ∈ Finset.range k, (monomial (k + 1) : (a : B) → B[X]) (f.coeff (k + 1 + j))) ∈ g • Q
Tactic: rw [← Ideal.neg_mem_iff, neg_sub, hr, Finset.sum_range_succ', Polynomial.eval_add,
        Polynomial.eval_monomial, zero_add, pow_zero, mul_one, add_sub_cancel_right]
-- 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 : 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_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr_2 : 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 : (a : B) → B[X]) (f.coeff (i + j))
⊢ eval b (∑ k ∈ Finset.range k, (monomial (k + 1) : (a : B) → B[X]) (f.coeff (k + 1 + j))) ∈ g • Q
have simp : eval b
    (∑ x ∈ Finset.range k,
      HMul.hMul (α := B[X]) (β := B[X]) ((monomial x : (a : B) → B[X]) (f.coeff (x + 1 + j)) : B[X]) X) ∈
  g • Q
Tactic: simp only [← Polynomial.monomial_mul_X]