awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
k : K
hk : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) k : L) ((algebraMap B L : (a : B) → L) b : L)
hb : IsIntegral A b
⊢ IsIntegral A k

Tactic:
rw [← isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective B L), ← hk,
    isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective K L)] at hb

Premises used: isIntegral_algebraMap_iff, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
k : K
hk : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) k : L) ((algebraMap B L : (a : B) → L) b : L)
hb : IsIntegral A k
obtain :
  ∀ (a : A)
    (hk :
      Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
        ((algebraMap B L : (a : B) → L) b : L))
    (hb : IsIntegral.{u_1, u_2} A (A := K) ((algebraMap A K : (a : A) → K) a : K)),
    ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b

Tactic:
obtain ⟨a, rfl⟩ := IsIntegrallyClosed.algebraMap_eq_of_integral hb

Premises used: IsIntegrallyClosed.algebraMap_eq_of_integral, rfl
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
a : A
hk :
  Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
    ((algebraMap B L : (a : B) → L) b : L)
hb : IsIntegral.{u_1, u_2} A (A := K) ((algebraMap A K : (a : A) → K) a : K)
⊢ (algebraMap A B : (a : A) → B) a = b

Tactic:
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L,
    (FaithfulSMul.algebraMap_injective B L).eq_iff] at hk

Premises used: Function.Injective.eq_iff, FaithfulSMul.algebraMap_injective, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
a : A
hk :
  Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
    ((algebraMap B L : (a : B) → L) b : L)
hb : IsIntegral.{u_1, u_2} A (A := K) ((algebraMap A K : (a : A) → K) a : K)
hk₁ : (algebraMap A B : (a : A) → B) a = b
⊢ IsIntegral.{u_1, u_2} A (A := K) ((algebraMap A K : (a : A) → K) a : K)

Tactic:
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L,
    (FaithfulSMul.algebraMap_injective B L).eq_iff] at hk

Premises used: Function.Injective.eq_iff, FaithfulSMul.algebraMap_injective, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
a : A
hk : (algebraMap A B : (a : A) → B) a = b
hb : IsIntegral.{u_1, u_2} A (A := K) ((algebraMap A K : (a : A) → K) a : K)
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b

Tactic:
⟨a, hk⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
a : A
hk : (algebraMap A B : (a : A) → B) a = b
hb : IsIntegral.{u_1, u_2} A (A := K) ((algebraMap A K : (a : A) → K) a : K)
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b

Tactic:
exact ⟨a, hk⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
inst_16 : IsGalois K L
⊢ IsInvariant A B (B ≃ₐ[A] B)

Tactic:
⟨fun b h ↦ (isInvariant_of_isGalois A K L B).1 b (fun g ↦ h (galRestrict A K L B g))⟩

Premises used: Algebra.IsInvariant.mk, Algebra.IsInvariant.isInvariant, galRestrict, DFunLike.coe
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
H : Subgroup G
inst_6 : H.Normal
g : G
x : ↥(FixedPoints.subring.{u_2, u_3} B ↥H)
h : ↥H
⊢ h • g • (↑x : B) = g • (↑x : B)

Tactic:
simpa [mul_smul] using congr(g • $(x.2 ⟨_, ‹H.Normal›.conj_mem' _ h.2 g⟩))

Premises used: Subtype.mk, SemigroupAction.mul_smul, Subtype.property, Subgroup.Normal.conj_mem'
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
H : Subgroup G
inst_6 : H.Normal
a b : G
hb : { unop' := b : PreOpposite G } ∈ H.op
h :
  ∀ (c : ↥(FixedPoints.subring.{u_2, u_3} B ↥H)),
    Eq.{u_2 + 1} (α := B)
      (↑((fun (g : G) (x : ↥(FixedPoints.subring.{u_2, u_3} B ↥H)) ↦
              (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subring B) (FixedPoints.subring.{u_2, u_3} B ↥H) x)
                  (g • (↑x : B)) ⋯ :
                ↥(FixedPoints.subring.{u_2, u_3} B ↥H)))
            ((fun (m : ↥H.op) ↦ m • a) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ H.op) { unop' := b } hb)) c) :
        B)
      (↑((fun (g : G) (x : ↥(FixedPoints.subring.{u_2, u_3} B ↥H)) ↦
              (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subring B) (FixedPoints.subring.{u_2, u_3} B ↥H) x)
                  (g • (↑x : B)) ⋯ :
                ↥(FixedPoints.subring.{u_2, u_3} B ↥H)))
            a c) :
        B)
⊢ Eq.{u_2 + 1} (α := ↥(FixedPoints.subring.{u_2, u_3} B ↥H) → ↥(FixedPoints.subring.{u_2, u_3} B ↥H))
    ((fun (g : G) (x : ↥(FixedPoints.subring.{u_2, u_3} B ↥H)) ↦
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subring B) (FixedPoints.subring.{u_2, u_3} B ↥H) x)
            (g • (↑x : B)) ⋯ :
          ↥(FixedPoints.subring.{u_2, u_3} B ↥H)))
      ((fun (m : ↥H.op) ↦ m • a) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ H.op) { unop' := b } hb)))
    ((fun (g : G) (x : ↥(FixedPoints.subring.{u_2, u_3} B ↥H)) ↦
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subring B) (FixedPoints.subring.{u_2, u_3} B ↥H) x)
            (g • (↑x : B)) ⋯ :
          ↥(FixedPoints.subring.{u_2, u_3} B ↥H)))
      a)

Tactic:
ext c
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
H : Subgroup G
inst_6 : H.Normal
a b : G
hb : { unop' := b : PreOpposite G } ∈ H.op
c : ↥(FixedPoints.subring.{u_2, u_3} B ↥H)
⊢ Eq.{u_2 + 1} (α := B)
    (↑((fun (g : G) (x : ↥(FixedPoints.subring.{u_2, u_3} B ↥H)) ↦
            (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subring B) (FixedPoints.subring.{u_2, u_3} B ↥H) x)
                (g • (↑x : B)) ⋯ :
              ↥(FixedPoints.subring.{u_2, u_3} B ↥H)))
          ((fun (m : ↥H.op) ↦ m • a) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ H.op) { unop' := b } hb)) c) :
      B)
    (↑((fun (g : G) (x : ↥(FixedPoints.subring.{u_2, u_3} B ↥H)) ↦
            (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subring B) (FixedPoints.subring.{u_2, u_3} B ↥H) x)
                (g • (↑x : B)) ⋯ :
              ↥(FixedPoints.subring.{u_2, u_3} B ↥H)))
          a c) :
      B)

Tactic:
simpa [mul_smul] using congr(a • $(c.2 ⟨b, hb⟩))

Premises used: Subtype.mk, SemigroupAction.mul_smul, Subtype.property
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
H : Subgroup G
inst_6 : H.Normal
inst_7 : Algebra.IsInvariant A B G
x : ↥(FixedPoints.subalgebra.{u_1, u_2, u_3} A B ↥H)
hx : ∀ (g : G ⧸ H), g • x = x
obtain :
  ∀ (y : A) (hy : (algebraMap A B : (a : A) → B) y = (↑x : B)),
    ∃ (a : A),
      (algebraMap A ↥(FixedPoints.subalgebra.{u_1, u_2, u_3} A B ↥H) : (a : A) → ↥(FixedPoints.subalgebra A B ↥H)) a = x
⊢ ∃ (a : A),
    (algebraMap A ↥(FixedPoints.subalgebra.{u_1, u_2, u_3} A B ↥H) : (a : A) → ↥(FixedPoints.subalgebra A B ↥H)) a = x

Tactic:
obtain ⟨y, hy⟩ := Algebra.IsInvariant.isInvariant (A := A) (G := G) x.1
      (fun g ↦ congr_arg Subtype.val (hx g))

Premises used: QuotientGroup.mk, congr_arg, Algebra.IsInvariant.isInvariant, Subtype.val
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
H : Subgroup G
inst_6 : H.Normal
inst_7 : Algebra.IsInvariant A B G
x : ↥(FixedPoints.subalgebra.{u_1, u_2, u_3} A B ↥H)
hx : ∀ (g : G ⧸ H), g • x = x
y : A
hy : (algebraMap A B : (a : A) → B) y = (↑x : B)
⊢ ∃ (a : A),
    (algebraMap A ↥(FixedPoints.subalgebra.{u_1, u_2, u_3} A B ↥H) : (a : A) → ↥(FixedPoints.subalgebra A B ↥H)) a = x

Tactic:
⟨y, Subtype.ext hy⟩

Premises used: Exists.intro, Subtype.ext
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
H : Subgroup G
inst_6 : H.Normal
inst_7 : Algebra.IsInvariant A B G
x : ↥(FixedPoints.subalgebra.{u_1, u_2, u_3} A B ↥H)
hx : ∀ (g : G ⧸ H), g • x = x
y : A
hy : (algebraMap A B : (a : A) → B) y = (↑x : B)
⊢ ∃ (a : A),
    (algebraMap A ↥(FixedPoints.subalgebra.{u_1, u_2, u_3} A B ↥H) : (a : A) → ↥(FixedPoints.subalgebra A B ↥H)) a = x

Tactic:
exact ⟨y, Subtype.ext hy⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
G : Type u_3
inst : CommRing B
inst_1 : Group G
inst_2 : MulSemiringAction G B
inst_3 : Fintype G
b : B
⊢ Eq (α := B[X]) (charpoly G b) (∏ g : G, HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X]))

Tactic:
rfl

Premises used: MulSemiringAction.charpoly, rfl
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
G : Type u_3
inst : CommRing B
inst_1 : Group G
inst_2 : MulSemiringAction G B
inst_3 : Fintype G
b : B
⊢ Eq (α := B[X]) (charpoly G b) (∏ g : G, g • HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]))

Tactic:
simp only [smul_sub, smul_C, smul_X, charpoly_eq]

Premises used: Polynomial.smul_X, smul_sub, MulSemiringAction.charpoly_eq, Polynomial.smul_C
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
G : Type u_3
inst : CommRing B
inst_1 : Group G
inst_2 : MulSemiringAction G B
inst_3 : Fintype G
b : B
⊢ Monic (charpoly G b)

Tactic:
monic_prod_of_monic _ _ (fun _ _ ↦ monic_X_sub_C _)

Premises used: Polynomial.monic_X_sub_C, MulSemiringAction.charpoly, Polynomial.monic_prod_of_monic, HSMul.hSMul
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
G : Type u_3
inst : CommRing B
inst_1 : Group G
inst_2 : MulSemiringAction G B
inst_3 : Fintype G
b : B
rw :
  Eq.{u_2 + 1} (α := B) (∏ j : G, eval b (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (j • b) : B[X]))) 0
⊢ eval b (charpoly G b) = 0

Tactic:
rw [charpoly_eq, eval_prod]

Premises used: Polynomial.eval_prod, MulSemiringAction.charpoly_eq
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
G : Type u_3
inst : CommRing B
inst_1 : Group G
inst_2 : MulSemiringAction G B
inst_3 : Fintype G
b : B
apply :
  eval b
      (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (HSMul.hSMul.{u_3, u_2, u_2} (α := G) 1 b) : B[X])) =
    0
⊢ Eq.{u_2 + 1} (α := B) (∏ j : G, eval b (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (j • b) : B[X]))) 0

Tactic:
apply Finset.prod_eq_zero (Finset.mem_univ (1 : G))

Premises used: Finset.mem_univ, Finset.prod_eq_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
G : Type u_3
inst : CommRing B
inst_1 : Group G
inst_2 : MulSemiringAction G B
inst_3 : Fintype G
b : B
rw : eval b (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X])) = 0
rw₁ : eval b X - eval b ((C : (a : B) → B[X]) b) = 0
rw₂ : eval b X - b = 0
rw₃ : b - b = 0
rw₄ rw₅ : Eq.{u_2 + 1} (α := B) 0 0
⊢ eval b
      (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (HSMul.hSMul.{u_3, u_2, u_2} (α := G) 1 b) : B[X])) =
    0

Tactic:
rw [one_smul, eval_sub, eval_C, eval_X, sub_self]

Premises used: Polynomial.eval_C, sub_self, Polynomial.eval_X, one_smul, Polynomial.eval_sub
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
G : Type u_3
inst : CommRing B
inst_1 : Group G
inst_2 : MulSemiringAction G B
inst_3 : Fintype G
b : B
g : G
rw :
  HSMul.hSMul (β := B[X]) g (∏ g : G, g • HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X])) =
    ∏ g : G, g • HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X])
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := B[X]) (∏ h : G, h • HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]))
    (∏ g : G, g • HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]))
⊢ HSMul.hSMul (β := B[X]) g (charpoly G b) = charpoly G b

Tactic:
rw [charpoly_eq_prod_smul, Finset.smul_prod_perm]

Premises used: MulSemiringAction.charpoly_eq_prod_smul, Finset.smul_prod_perm
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
G : Type u_3
inst : CommRing B
inst_1 : Group G
inst_2 : MulSemiringAction G B
inst_3 : Fintype G
b : B
n : ℕ
g : G
rw : (HSMul.hSMul (β := B[X]) g (charpoly G b)).coeff n = coeff (charpoly G b) n
rw₁ rw₂ : coeff (charpoly G b) n = coeff (charpoly G b) n
⊢ g • coeff (charpoly G b) n = coeff (charpoly G b) n

Tactic:
rw [← coeff_smul, smul_charpoly]

Premises used: MulSemiringAction.smul_charpoly, Polynomial.coeff_smul
-- 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 : Fintype G
b : B
⊢ Membership.mem (γ := Subsemiring B[X]) (lifts (algebraMap A B)) (charpoly G b)

Tactic:
(charpoly G b).lifts_iff_coeff_lifts.mpr fun n ↦ isInvariant _ (smul_coeff_charpoly b n)

Premises used: Iff.mpr, MulSemiringAction.smul_coeff_charpoly, MulSemiringAction.charpoly, Polynomial.coeff, Algebra.IsInvariant.isInvariant, Polynomial.lifts_iff_coeff_lifts
-- 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
intro : ∀ (val : Fintype G), Algebra.IsIntegral A B
⊢ Algebra.IsIntegral A B

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- 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
val : Fintype G
⊢ Algebra.IsIntegral A B

Tactic:
⟨fun b ↦ ?_⟩

Premises used: Algebra.IsIntegral.mk
-- 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
val : Fintype G
intro : ∀ (b : B), IsIntegral A b
⊢ Algebra.IsIntegral A B

Tactic:
refine ⟨fun b ↦ ?_⟩
-- 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
val : Fintype G
b : B
intro : ∀ (p : A[X]) (hp1 : Eq (α := B[X]) (map (algebraMap A B) p) (charpoly G b)) (hp2 : p.Monic), IsIntegral A b
⊢ IsIntegral A b

Tactic:
obtain ⟨p, hp1, -, hp2⟩ := Polynomial.lifts_and_natDegree_eq_and_monic
    (charpoly_mem_lifts A B G b) (monic_charpoly G b)

Premises used: MulSemiringAction.monic_charpoly, Polynomial.lifts_and_natDegree_eq_and_monic, Algebra.IsInvariant.charpoly_mem_lifts
-- 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
val : Fintype G
b : B
p : A[X]
hp1 : Eq (α := B[X]) (map (algebraMap A B) p) (charpoly G b)
hp2 : p.Monic
rw : eval b (map (algebraMap A B) p) = 0
rw₁ : eval b (charpoly G b) = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := B) 0 0
⊢ eval₂ (algebraMap A B) b p = 0

Tactic:
rw [← eval_map, hp1, eval_charpoly]

Premises used: Polynomial.eval_map, MulSemiringAction.eval_charpoly
-- 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
val : Fintype G
b : B
p : A[X]
hp1 : Eq (α := B[X]) (map (algebraMap A B) p) (charpoly G b)
hp2 : p.Monic
⊢ IsIntegral A b

Tactic:
exact ⟨p, hp2, by rw [← eval_map, hp1, eval_charpoly]⟩
-- 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)
intro : ∀ (val : Fintype G), ∃ (g : G), Q = g • P
⊢ ∃ (g : G), Q = g • P

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- 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)
rw : (↑Q : Set B) ⊆ ⋃ i ∈ (↑⊤ : Set G), (↑(i • P) : Set B)
⊢ ∃ (g : G), Membership.mem (γ := Finset G) ⊤ g ∧ Q ≤ g • P

Tactic:
rw [← Ideal.subset_union_prime 1 1 (fun _ _ _ _ ↦ hP.smul _)]

Premises used: Ideal.IsPrime.smul, Ideal.subset_union_prime, OfNat.ofNat
-- 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)
h : ∃ (g : G), Membership.mem (γ := Finset G) Finset.univ g ∧ g • b ∈ P
obtain : ∀ (g : G) (hg : g • b ∈ P), Membership.mem (γ := Set B) (⋃ i ∈ (↑⊤ : Set G), (↑(i • P) : Set B)) b
⊢ Membership.mem (γ := Set B) (⋃ i ∈ (↑⊤ : Set G), (↑(i • P) : Set B)) b

Tactic:
obtain ⟨g, -, hg⟩ := 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_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
hg : g • b ∈ P
⊢ Membership.mem (γ := Set B) (⋃ i ∈ (↑⊤ : Set G), (↑(i • P) : Set B)) b

Tactic:
apply Set.mem_biUnion (Finset.mem_univ g⁻¹) (Ideal.mem_inv_pointwise_smul_iff.mpr hg)

Premises used: Finset.mem_univ, Set.mem_biUnion, Inv.inv