awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Invariant.Basic
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
pos : coeff (map (algebraMap B (B ⧸ Q)) f) (n + j) = q.coeff n
pos₁ :
  (HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q).coeff (n + j) =
    q.coeff n
pos₂ pos₃ : q.coeff n = q.coeff n
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (f.coeff (n + j)) = q.coeff n

Tactic:
rw [← Polynomial.coeff_map, hq, Polynomial.coeff_X_pow_mul]

Premises used: Polynomial.coeff_map, Polynomial.coeff_X_pow_mul
-- Module: Mathlib.RingTheory.Invariant.Basic
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
neg₂ neg₃ : Eq.{u_2 + 1} (α := B ⧸ Q) 0 0
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 = q.coeff n

Tactic:
rw [map_zero, eq_comm, Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_not_ge hn)]

Premises used: lt_of_not_ge, map_zero, eq_comm, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Invariant.Basic
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))
⊢ 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)]
-- Module: Mathlib.RingTheory.Invariant.Basic
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
⊢ eval b f = 0

Tactic:
have hf : f.eval b = 0 := MulSemiringAction.eval_charpoly G b
-- Module: Mathlib.RingTheory.Invariant.Basic
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
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)
⊢ eval b r ∈ Q

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

Premises used: Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Invariant.Basic
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) : (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
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
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)
⊢ Eq (α := B ⧸ Q) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) (eval b r) : B ⧸ Q) (0 : B ⧸ Q)

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

Premises used: Polynomial.eval_map, Polynomial.eval₂_at_apply
-- Module: Mathlib.RingTheory.Invariant.Basic
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

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
-- Module: Mathlib.RingTheory.Invariant.Basic
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
⊢ ∀ (g : G), g • a = a

Tactic:
have ha : ∀ g : G, g • a = a := MulSemiringAction.smul_coeff_charpoly b j
-- Module: Mathlib.RingTheory.Invariant.Basic
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
⊢ 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
-- Module: Mathlib.RingTheory.Invariant.Basic
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))
rw : eval b (∑ k ∈ Finset.range k, (monomial (k + 1) : (a : B) → B[X]) (f.coeff (k + 1 + j))) ∈ g • Q
⊢ a - eval b r ∈ 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]

Premises used: neg_sub, zero_add, pow_zero, Polynomial.eval_add, Ideal.neg_mem_iff, add_sub_cancel_right, mul_one, Finset.sum_range_succ', Polynomial.eval_monomial
-- Module: Mathlib.RingTheory.Invariant.Basic
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))
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
⊢ eval b (∑ k ∈ Finset.range k, (monomial (k + 1) : (a : B) → B[X]) (f.coeff (k + 1 + j))) ∈ g • Q

Tactic:
simp only [← Polynomial.monomial_mul_X]

Premises used: Polynomial.monomial_mul_X
-- Module: Mathlib.RingTheory.Invariant.Basic
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))
rw : eval b (∑ i ∈ Finset.range k, (monomial i : (a : B) → B[X]) (f.coeff (i + 1 + j))) * b ∈ g • Q
⊢ 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:
rw [← Finset.sum_mul, Polynomial.eval_mul_X]

Premises used: Polynomial.eval_mul_X, Finset.sum_mul
-- Module: Mathlib.RingTheory.Invariant.Basic
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 (∑ i ∈ Finset.range k, (monomial i : (a : B) → B[X]) (f.coeff (i + 1 + j))) * b ∈ g • Q

Tactic:
Ideal.mul_mem_left (g • Q) _ (hbP g hg)

Premises used: Set.Mem, HSMul.hSMul, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Invariant.Basic
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 (∑ i ∈ Finset.range k, (monomial i : (a : B) → B[X]) (f.coeff (i + 1 + j))) * b ∈ g • Q

Tactic:
exact Ideal.mul_mem_left (g • Q) _ (hbP g hg)

Premises used: HSMul.hSMul, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Invariant.Basic
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), g • Q ≠ Q → a - eval b r ∈ g • Q

Tactic:
have hr' : ∀ g : G, g • Q ≠ Q → a - r.eval b ∈ g • Q := by
    intro g hg
    have hr : r = ∑ i ∈ Finset.range (k + 1), Polynomial.monomial i (f.coeff (i + j)) := rfl
    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]
    simp only [← Polynomial.monomial_mul_X]
    rw [← Finset.sum_mul, Polynomial.eval_mul_X]
    exact Ideal.mul_mem_left (g • Q) _ (hbP g hg)
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • 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)

Tactic:
⟨a, a - r.eval b, ha, ?_, fun h ↦ ?_⟩

Premises used: Polynomial.eval, HSub.hSub, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
refine_1 : a ∉ Q
refine_2 :
  ∀ (h : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (h • (a - eval b r)) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if h • Q = Q then a else 0) : B ⧸ 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)

Tactic:
refine ⟨a, a - r.eval b, ha, ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
refine_1 : ¬Eq (α := B ⧸ Q) ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) a : B ⧸ Q) (0 : B ⧸ Q)
refine_1₁ : ¬Eq (α := B ⧸ Q) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q) (0 : B ⧸ Q)
refine_1₂ : ¬Eq (α := B ⧸ Q) (coeff (map (algebraMap B (B ⧸ Q)) f) j) 0
refine_1₃ : ¬Eq (α := B ⧸ Q) (coeff (map (algebraMap B (B ⧸ Q)) f) (0 + j)) 0
refine_1₄ :
  ¬(HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q).coeff (0 + j) =
      0
refine_1₅ : ¬q.coeff 0 = 0
refine_1₆ refine_1₇ refine_1₈ refine_1₉ : ¬X ∣ q
⊢ a ∉ Q

Tactic:
rwa [← Ideal.Quotient.eq_zero_iff_mem, ← Ideal.Quotient.algebraMap_eq, ← Polynomial.coeff_map,
      ← zero_add j, hq, Polynomial.coeff_X_pow_mul, ← Polynomial.X_dvd_iff]

Premises used: Polynomial.coeff_map, Ideal.Quotient.algebraMap_eq, Polynomial.coeff_X_pow_mul, zero_add, Ideal.Quotient.eq_zero_iff_mem, Polynomial.X_dvd_iff