awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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 : IsGalois K L
⊢ IsInvariant.{u_1, u_4, u_3} A B Gal(L/K)
have h₁ : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
Tactic: replace h := ((IsGalois.tfae (F := K) (E := L)).out 0 1).mp h
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ IsInvariant.{u_1, u_4, u_3} A B Gal(L/K)
have refine : ∀ (b : B) (hb : ∀ (g : Gal(L/K)), g • b = b), ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
Tactic: refine ⟨fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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
hb : ∀ (g : Gal(L/K)), g • b = b
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
have hb₁ : Membership.mem.{u_3, u_3} (α := L) (γ := IntermediateField K L) (IntermediateField.fixedField ⊤)
  ((algebraMap B L : (a : B) → L) b : L)
Tactic: replace hb : algebraMap B L b ∈ IntermediateField.fixedField (⊤ : Subgroup Gal(L/K)) := by
    rintro ⟨g, -⟩
    exact (algebraMap_galRestrict_apply A g b).symm.trans (congrArg (algebraMap B L) (hb g))
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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
hb :
  Membership.mem.{u_3, u_3} (α := L) (γ := IntermediateField K L) (IntermediateField.fixedField ⊤)
    ((algebraMap B L : (a : B) → L) b : L)
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
have hb₁ : Membership.mem.{u_3, u_3} (α := L) (γ := Set L) (Set.range.{u_3, u_2 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
  ((algebraMap B L : (a : B) → L) b : L)
Tactic: rw [h, IntermediateField.mem_bot] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
hb :
  Membership.mem.{u_3, u_3} (α := L) (γ := Set L) (Set.range.{u_3, u_2 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
    ((algebraMap B L : (a : B) → L) b : L)
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
have obtain : ∀ (k : K) (hk : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) k : L) ((algebraMap B L : (a : B) → L) b : L)),
  ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
Tactic: obtain ⟨k, hk⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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)
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
have hb : IsIntegral A b
Tactic: have hb : IsIntegral A b := IsIntegralClosure.isIntegral A L b
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
have hb₁ : IsIntegral A k
Tactic: rw [← isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective B L), ← hk,
    isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective K L)] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
have 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
Tactic: obtain ⟨a, rfl⟩ := IsIntegrallyClosed.algebraMap_eq_of_integral hb
Cleared hypotheses: k, hk, hb
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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)
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
have hk₁ : (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
Cleared hypotheses: hk, hb
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ 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)
have 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)) sorry :
              ↥(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)) sorry :
              ↥(FixedPoints.subring.{u_2, u_3} B ↥H)))
          a c) :
      B)
Tactic: ext c
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ ∃ (a : A),
    (algebraMap A ↥(FixedPoints.subalgebra.{u_1, u_2, u_3} A B ↥H) : (a : A) → ↥(FixedPoints.subalgebra A B ↥H)) a = x
have 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
Tactic: obtain ⟨y, hy⟩ := Algebra.IsInvariant.isInvariant (A := A) (G := G) x.1
      (fun g ↦ congr_arg Subtype.val (hx g))
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ eval b (charpoly G b) = 0
have 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
Tactic: rw [charpoly_eq, eval_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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.{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
have 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
Tactic: apply Finset.prod_eq_zero (Finset.mem_univ (1 : G))
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ 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
have rw : eval b (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X])) = 0
Tactic: rw [one_smul, eval_sub, eval_C, eval_X, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ 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
have rw₁ : eval b X - eval b ((C : (a : B) → B[X]) b) = 0
Tactic: rw [one_smul, eval_sub, eval_C, eval_X, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ 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
have rw₂ : eval b X - b = 0
Tactic: rw [one_smul, eval_sub, eval_C, eval_X, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ 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
have rw₃ : b - b = 0
Tactic: rw [one_smul, eval_sub, eval_C, eval_X, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ 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
have rw₄ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [one_smul, eval_sub, eval_C, eval_X, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ HSMul.hSMul (β := B[X]) g (charpoly G b) = charpoly G b
have 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])
Tactic: rw [charpoly_eq_prod_smul, Finset.smul_prod_perm]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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])
⊢ HSMul.hSMul (β := B[X]) g (charpoly G b) = charpoly G b
have 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]))
Tactic: rw [charpoly_eq_prod_smul, Finset.smul_prod_perm]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ g • coeff (charpoly G b) n = coeff (charpoly G b) n
have rw : (HSMul.hSMul (β := B[X]) g (charpoly G b)).coeff n = coeff (charpoly G b) n
Tactic: rw [← coeff_smul, smul_charpoly]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ g • coeff (charpoly G b) n = coeff (charpoly G b) n
have rw₁ : coeff (charpoly G b) n = coeff (charpoly G b) n
Tactic: rw [← coeff_smul, smul_charpoly]
-- 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
⊢ Algebra.IsIntegral A B
have intro : ∀ (val : Fintype G), Algebra.IsIntegral A B
Tactic: cases nonempty_fintype G
-- 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
val : Fintype G
⊢ Algebra.IsIntegral A B
have intro : ∀ (b : B), IsIntegral A b
Tactic: refine ⟨fun 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
val : Fintype G
b : B
⊢ IsIntegral A b
have intro : ∀ (p : A[X]) (hp1 : Eq (α := B[X]) (map (algebraMap A B) p) (charpoly G b)) (hp2 : p.Monic), 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)
-- 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
val : Fintype G
b : B
p : A[X]
hp1 : Eq (α := B[X]) (map (algebraMap A B) p) (charpoly G b)
hp2 : p.Monic
⊢ eval₂ (algebraMap A B) b p = 0
have rw : eval b (map (algebraMap A B) p) = 0
Tactic: rw [← eval_map, hp1, eval_charpoly]
-- 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
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
⊢ eval₂ (algebraMap A B) b p = 0
have rw₁ : eval b (charpoly G b) = 0
Tactic: rw [← eval_map, hp1, eval_charpoly]
-- 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
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
⊢ eval₂ (algebraMap A B) b p = 0
have rw₂ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [← eval_map, hp1, eval_charpoly]
-- 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)
⊢ ∃ (g : G), Q = g • P
have intro : ∀ (val : Fintype G), ∃ (g : G), Q = g • P
Tactic: cases nonempty_fintype G
-- 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)
⊢ ∃ (g : G), Membership.mem (γ := Finset G) ⊤ g ∧ Q ≤ g • P
have rw : (↑Q : Set B) ⊆ ⋃ i ∈ (↑⊤ : Set G), (↑(i • P) : Set B)
Tactic: rw [← Ideal.subset_union_prime 1 1 (fun _ _ _ _ ↦ hP.smul _)]
-- 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)
h : ∃ (g : G), Membership.mem (γ := Finset G) Finset.univ g ∧ g • b ∈ P
⊢ Membership.mem (γ := Set B) (⋃ i ∈ (↑⊤ : Set G), (↑(i • P) : Set B)) b
have obtain : ∀ (g : G) (hg : g • b ∈ P), Membership.mem (γ := Set B) (⋃ i ∈ (↑⊤ : Set G), (↑(i • P) : Set B)) b
Tactic: obtain ⟨g, -, hg⟩ := h
Cleared hypotheses: h
-- 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)
⊢ Membership.mem (γ := Set B) (⋃ i ∈ (↑⊤ : Set G), (↑(i • P) : Set B)) b
have suffices : ∃ (g : G), Membership.mem (γ := Finset G) Finset.univ g ∧ g • b ∈ P
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)