awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
G : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : IsInvariant A B G
inst_6 : Finite G
inst_7 : SMulCommClass G A B
P_1 Q_1 : Ideal B
hP_1 : P_1.IsPrime
hQ_1 : Q_1.IsPrime
hPQ_1 : Eq (α := Ideal A) (Ideal.under A P_1) (Ideal.under A Q_1)
val : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
b : B
hb : b ∈ (↑Q : Set B)
⊢ ∃ (g : G), Membership.mem (γ := Finset G) Finset.univ g ∧ g • b ∈ P
have obtain : ∀ (a : A) (ha : Eq.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) a : B) (∏ g : G, g • b : B)),
  ∃ (g : G), Membership.mem (γ := Finset G) Finset.univ g ∧ g • b ∈ P
Tactic: obtain ⟨a, ha⟩ := isInvariant (A := A) (∏ g : G, g • b) (Finset.smul_prod_perm b)
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
G : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : IsInvariant A B G
inst_6 : Finite G
inst_7 : SMulCommClass G A B
P_1 Q_1 : Ideal B
hP_1 : P_1.IsPrime
hQ_1 : Q_1.IsPrime
hPQ_1 : Eq (α := Ideal A) (Ideal.under A P_1) (Ideal.under A Q_1)
val : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
b : B
hb : b ∈ (↑Q : Set B)
a : A
ha : Eq.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) a : B) (∏ g : G, g • b : B)
⊢ ∃ (g : G), Membership.mem (γ := Finset G) Finset.univ g ∧ g • b ∈ P
have rw : ∃ (i : G), Membership.mem (γ := Finset G) Finset.univ i ∧ i • b ∈ Q
Tactic: rw [← hP.prod_mem_iff, ← ha, ← P.mem_comap, ← P.under_def A,
      hPQ, Q.mem_comap, ha, hQ.prod_mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
G : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : IsInvariant A B G
inst_6 : Finite G
inst_7 : SMulCommClass G A B
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
val : Fintype G
⊢ ∃ (g : G), Q = g • P
have this : ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime],
  Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q) → ∃ (g : G), Membership.mem (γ := Finset G) ⊤ g ∧ Q ≤ g • P
Tactic: have : ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime], P.under A = Q.under A →
      ∃ g ∈ (⊤ : Finset G), Q ≤ g • P := by
    intro P Q hP hQ hPQ
    rw [← Ideal.subset_union_prime 1 1 (fun _ _ _ _ ↦ hP.smul _)]
    intro b hb
    suffices h : ∃ g ∈ Finset.univ, g • b ∈ P by
      obtain ⟨g, -, hg⟩ := h
      apply Set.mem_biUnion (Finset.mem_univ g⁻¹) (Ideal.mem_inv_pointwise_smul_iff.mpr hg)
    obtain ⟨a, ha⟩ := isInvariant (A := A) (∏ g : G, g • b) (Finset.smul_prod_perm b)
    rw [← hP.prod_mem_iff, ← ha, ← P.mem_comap, ← P.under_def A,
      hPQ, Q.mem_comap, ha, hQ.prod_mem_iff]
    exact ⟨1, Finset.mem_univ 1, (one_smul G b).symm ▸ hb⟩
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
G : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : IsInvariant A B G
inst_6 : Finite G
inst_7 : SMulCommClass G A B
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
val : Fintype G
this :
  ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime],
    Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q) → ∃ (g : G), Membership.mem (γ := Finset G) ⊤ g ∧ Q ≤ g • P
⊢ ∃ (g : G), Q = g • P
have intro : ∀ (g : G) (hg : Q ≤ g • P), ∃ (g : G), Q = g • P
Tactic: obtain ⟨g, -, hg⟩ := this P Q hPQ
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
G : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : IsInvariant A B G
inst_6 : Finite G
inst_7 : SMulCommClass G A B
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
val : Fintype G
this :
  ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime],
    Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q) → ∃ (g : G), Membership.mem (γ := Finset G) ⊤ g ∧ Q ≤ g • P
g : G
hg : Q ≤ g • P
⊢ ∃ (g : G), Q = g • P
have intro : ∀ (g' : G) (hg' : g • P ≤ g' • Q), ∃ (g : G), Q = g • P
Tactic: obtain ⟨g', -, hg'⟩ := this Q (g • P) ((P.under_smul A g).trans hPQ).symm
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
G : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : IsInvariant A B G
inst_6 : Finite G
inst_7 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
hP : Q.LiesOver P
hQ : Q.IsPrime
⊢ MulAction.orbit G Q = P.primesOver B
have refine : ∀ (R : Ideal B) (h : Membership.mem (γ := Set (Ideal B)) (P.primesOver B) R), R ∈ MulAction.orbit G Q
Tactic: refine Set.ext fun R ↦ ⟨fun ⟨g, hg⟩ ↦ hg ▸ ⟨hQ.smul g, hP.smul g⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
G : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : IsInvariant A B G
inst_6 : Finite G
inst_7 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
hP : Q.LiesOver P
hQ : Q.IsPrime
R : Ideal B
h : Membership.mem (γ := Set (Ideal B)) (P.primesOver B) R
⊢ R ∈ MulAction.orbit G Q
have this : R.IsPrime
Tactic: have : R.IsPrime := h.1
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
G : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : IsInvariant A B G
inst_6 : Finite G
inst_7 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
hP : Q.LiesOver P
hQ : Q.IsPrime
R : Ideal B
h : Membership.mem (γ := Set (Ideal B)) (P.primesOver B) R
this : R.IsPrime
⊢ R ∈ MulAction.orbit G Q
have obtain : ∀ (g : G) (hg : R = g • Q), R ∈ MulAction.orbit G Q
Tactic: obtain ⟨g, hg⟩ := exists_smul_of_under_eq A B G Q R (hP.over.symm.trans h.2.over)
-- 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
⊢ ∃ (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 obtain : ∀ (val : Fintype G),
  ∃ (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: obtain ⟨_⟩ := nonempty_fintype G
-- 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
⊢ ¬P ≤ Q
have rw : ¬∃ (i : G), Membership.mem (γ := Finset G) {g : G | g • Q ≠ Q} i ∧ i • Q ≤ Q
Tactic: rw [Ideal.IsPrime.inf_le' inferInstance]
-- 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
⊢ ∃ (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 h1 : ¬P ≤ Q
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)
-- 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
⊢ ∃ (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 obtain : ∀ (b : B) (hbP : b ∈ P) (hbQ : 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: obtain ⟨b, hbP, hbQ⟩ := SetLike.not_le_iff_exists.mp h1
-- 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
hbP : b ∈ P
hbQ : 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)
have hbP₁ : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
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
Cleared hypotheses: hbP
-- 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
⊢ ∃ (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 obtain : ∀ (q : (B ⧸ Q)[X])
  (hq :
    map (algebraMap B (B ⧸ Q)) f =
      HSub.hSub (α := (B ⧸ Q)[X]) X ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) 0) ^
          rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f) *
        q)
  (hq0 : ¬HSub.hSub (α := (B ⧸ Q)[X]) X ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) 0) ∣ 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: obtain ⟨q, hq, hq0⟩ :=
    (f.map (algebraMap B (B ⧸ Q))).exists_eq_pow_rootMultiplicity_mul_and_not_dvd
      (Polynomial.map_monic_ne_zero (MulSemiringAction.monic_charpoly G b)) 0
-- 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 =
    HSub.hSub (α := (B ⧸ Q)[X]) X ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) 0) ^
        rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f) *
      q
hq0 : ¬HSub.hSub (α := (B ⧸ Q)[X]) X ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) 0) ∣ 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 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
Tactic: rw [map_zero, sub_zero] at hq hq0
Cleared hypotheses: hq, hq0
-- 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 =
    HSub.hSub (α := (B ⧸ Q)[X]) X ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) 0) ^
        rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f) *
      q
hq0 : ¬HSub.hSub (α := (B ⧸ Q)[X]) X ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) 0) ∣ q
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
⊢ ∃ (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 hq0₁ : ¬X ∣ q
Tactic: rw [map_zero, sub_zero] at hq hq0
Cleared hypotheses: hq, hq0
-- 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))
⊢ map (algebraMap B (B ⧸ Q)) r = q
have a : ∀ (n : ℕ), coeff (map (algebraMap B (B ⧸ Q)) r) n = q.coeff n
Tactic: ext n
-- 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 : ℕ
⊢ coeff (map (algebraMap B (B ⧸ Q)) r) n = q.coeff n
have a : (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q)
    (∑ b ∈ Finset.range (k + 1), coeff ((monomial b : (a : B) → B[X]) (f.coeff (b + j))) n) =
  q.coeff n
Tactic: rw [Polynomial.coeff_map, Polynomial.finsetSum_coeff]
-- 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 : ℕ
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q)
      (∑ b ∈ Finset.range (k + 1), coeff ((monomial b : (a : B) → B[X]) (f.coeff (b + j))) n) =
    q.coeff n
have a : (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if n ≤ k then f.coeff (n + j) else 0) = q.coeff n
Tactic: simp only [Polynomial.coeff_monomial, Finset.sum_ite_eq', Finset.mem_range_succ_iff]
-- 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 : ℕ
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if n ≤ k then f.coeff (n + j) else 0) = q.coeff n
have pos : ∀ (hn : n ≤ k), (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (f.coeff (n + j)) = q.coeff n
Tactic: split_ifs with hn
-- 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 : ℕ
pos : ∀ (hn : n ≤ k), (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (f.coeff (n + j)) = q.coeff n
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if n ≤ k then f.coeff (n + j) else 0) = q.coeff n
have neg : ∀ (hn : ¬n ≤ k), (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 = q.coeff n
Tactic: split_ifs with hn
-- 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
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (f.coeff (n + j)) = q.coeff n
have pos : coeff (map (algebraMap B (B ⧸ Q)) f) (n + j) = q.coeff n
Tactic: rw [← Polynomial.coeff_map, hq, Polynomial.coeff_X_pow_mul]
-- 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
pos : coeff (map (algebraMap B (B ⧸ Q)) f) (n + j) = q.coeff n
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (f.coeff (n + j)) = q.coeff n
have 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
Tactic: rw [← Polynomial.coeff_map, hq, Polynomial.coeff_X_pow_mul]
-- 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
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
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (f.coeff (n + j)) = q.coeff n
have pos₂ : q.coeff n = q.coeff n
Tactic: rw [← Polynomial.coeff_map, hq, Polynomial.coeff_X_pow_mul]
-- 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
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 = q.coeff n
have neg : 0 = q.coeff n
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 (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
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 = q.coeff n
have neg₁ : q.coeff n = 0
Tactic: rw [map_zero, eq_comm, Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_not_ge hn)]