awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
suffices : ∃ (g : G), Membership.mem (γ := Finset G) Finset.univ g ∧ g • b ∈ P
⊢ Membership.mem (γ := Set B) (⋃ i ∈ (↑⊤ : Set G), (↑(i • P) : Set B)) b

Tactic:
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)
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
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
⊢ ∃ (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)

Premises used: Finset.univ, Finset.prod, Algebra.IsInvariant.isInvariant, HSMul.hSMul, Finset.smul_prod_perm
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
rw : ∃ (i : G), Membership.mem (γ := Finset G) Finset.univ i ∧ i • b ∈ Q
⊢ ∃ (g : G), Membership.mem (γ := Finset G) Finset.univ g ∧ g • b ∈ P

Tactic:
rw [← hP.prod_mem_iff, ← ha, ← P.mem_comap, ← P.under_def A,
      hPQ, Q.mem_comap, ha, hQ.prod_mem_iff]

Premises used: Ideal.IsPrime.prod_mem_iff, Ideal.under_def, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
⊢ ∃ (i : G), Membership.mem (γ := Finset G) Finset.univ i ∧ i • b ∈ Q

Tactic:
⟨1, Finset.mem_univ 1, (one_smul G b).symm ▸ hb⟩

Premises used: Finset.mem_univ, Eq.rec, one_smul, And.intro, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
⊢ ∃ (i : G), Membership.mem (γ := Finset G) Finset.univ i ∧ i • b ∈ Q

Tactic:
exact ⟨1, Finset.mem_univ 1, (one_smul G b).symm ▸ hb⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
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
⊢ ∀ (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⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
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
intro : ∀ (g : G) (hg : Q ≤ g • P), ∃ (g : G), Q = g • P
⊢ ∃ (g : G), Q = g • P

Tactic:
obtain ⟨g, -, hg⟩ := this P Q hPQ
-- Module: Mathlib.RingTheory.Invariant.Basic
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
intro : ∀ (g' : G) (hg' : g • P ≤ g' • Q), ∃ (g : G), Q = g • P
⊢ ∃ (g : G), Q = g • P

Tactic:
obtain ⟨g', -, hg'⟩ := this Q (g • P) ((P.under_smul A g).trans hPQ).symm

Premises used: Ideal.under_smul, HSMul.hSMul, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hg' : g • P ≤ g' • Q
⊢ ∃ (g : G), Q = g • P

Tactic:
⟨g, le_antisymm hg (smul_eq_of_le_smul (hg.trans hg') ▸ hg')⟩

Premises used: Eq.rec, le_antisymm, Exists.intro, smul_eq_of_le_smul, LE.le.trans
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hg' : g • P ≤ g' • Q
⊢ ∃ (g : G), Q = g • P

Tactic:
exact ⟨g, le_antisymm hg (smul_eq_of_le_smul (hg.trans hg') ▸ hg')⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
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

Tactic:
Set.ext fun R ↦ ⟨fun ⟨g, hg⟩ ↦ hg ▸ ⟨hQ.smul g, hP.smul g⟩, fun h ↦ ?_⟩

Premises used: Set.ext, Ideal.LiesOver.smul, Ideal.primesOver, Membership.mem, Eq.rec, Ideal.IsPrime.smul, And.intro, Iff.intro, _private.0.Algebra.IsInvariant.orbit_eq_primesOver.match_1
-- Module: Mathlib.RingTheory.Invariant.Basic
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
refine : ∀ (R : Ideal B) (h : Membership.mem (γ := Set (Ideal B)) (P.primesOver B) R), R ∈ MulAction.orbit G Q
⊢ MulAction.orbit G Q = P.primesOver B

Tactic:
refine Set.ext fun R ↦ ⟨fun ⟨g, hg⟩ ↦ hg ▸ ⟨hQ.smul g, hP.smul g⟩, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
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.IsPrime

Tactic:
have : R.IsPrime := h.1
-- Module: Mathlib.RingTheory.Invariant.Basic
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
obtain : ∀ (g : G) (hg : R = g • Q), R ∈ MulAction.orbit 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)

Premises used: Algebra.IsInvariant.exists_smul_of_under_eq, Ideal.LiesOver.over, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Invariant.Basic
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
g : G
hg : R = g • Q
⊢ R ∈ MulAction.orbit G Q

Tactic:
⟨g, hg.symm⟩

Premises used: Set.Mem, setOf, MulAction.orbit, Exists.intro, Set.range, Eq.symm
-- Module: Mathlib.RingTheory.Invariant.Basic
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
g : G
hg : R = g • Q
⊢ R ∈ MulAction.orbit G Q

Tactic:
exact ⟨g, hg.symm⟩
-- 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
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)
⊢ ∃ (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

Premises used: nonempty_fintype
-- 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
rw : ¬∃ (i : G), Membership.mem (γ := Finset G) {g : G | g • Q ≠ Q} i ∧ i • Q ≤ Q
⊢ ¬P ≤ Q

Tactic:
rw [Ideal.IsPrime.inf_le' inferInstance]

Premises used: Ideal.IsPrime.inf_le', inferInstance
-- 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
g : G
hg1 : Membership.mem (γ := Finset G) {g : G | g • Q ≠ Q} g
hg2 : g • Q ≤ Q
⊢ False

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

Premises used: And.right, Iff.mp, smul_eq_of_smul_le, Finset.mem_filter
-- 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
g : G
hg1 : Membership.mem (γ := Finset G) {g : G | g • Q ≠ Q} g
hg2 : g • Q ≤ Q
⊢ False

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

Premises used: And.right, Iff.mp, smul_eq_of_smul_le, Finset.mem_filter
-- 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
⊢ ¬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)
-- 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
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)
⊢ ∃ (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

Premises used: Iff.mp, SetLike.not_le_iff_exists
-- 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
hbP : b ∈ P
hbQ : b ∉ Q
⊢ ∀ (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
-- 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
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)
⊢ ∃ (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

Premises used: Algebra.algebraMap, Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd, Polynomial.map_monic_ne_zero, HasQuotient.Quotient, MulSemiringAction.monic_charpoly, Polynomial.map, OfNat.ofNat
-- 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 =
    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
⊢ 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

Premises used: sub_zero, map_zero
-- 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 =
    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
⊢ ¬X ∣ q

Tactic:
rw [map_zero, sub_zero] at hq hq0

Premises used: sub_zero, map_zero
-- 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))
a : ∀ (n : ℕ), coeff (map (algebraMap B (B ⧸ Q)) r) n = q.coeff n
⊢ map (algebraMap B (B ⧸ Q)) r = q

Tactic:
ext n
-- 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 : ℕ
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
⊢ coeff (map (algebraMap B (B ⧸ Q)) r) n = q.coeff n

Tactic:
rw [Polynomial.coeff_map, Polynomial.finsetSum_coeff]

Premises used: Polynomial.coeff_map, Polynomial.finsetSum_coeff
-- 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 : ℕ
a : (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if n ≤ k then f.coeff (n + j) else 0) = q.coeff 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

Tactic:
simp only [Polynomial.coeff_monomial, Finset.sum_ite_eq', Finset.mem_range_succ_iff]

Premises used: Finset.sum_ite_eq', Finset.mem_range_succ_iff, Polynomial.coeff_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))
n : ℕ
pos : ∀ (hn : n ≤ k), (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (f.coeff (n + j)) = q.coeff n
neg : ∀ (hn : ¬n ≤ k), (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 = q.coeff n
⊢ (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if n ≤ k then f.coeff (n + j) else 0) = q.coeff n

Tactic:
split_ifs with hn