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
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
⊢ Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
have inl : Subsingleton B → Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
Tactic: cases subsingleton_or_nontrivial B
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
inl : Subsingleton B → Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
⊢ Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
have inr : Nontrivial B → Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
Tactic: cases subsingleton_or_nontrivial B
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
⊢ Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
have this : Algebra.IsIntegral A B
Tactic: have := Algebra.IsInvariant.isIntegral A B G
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
⊢ Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
have inr : ∀ (x : B ⧸ Q),
  Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (minpoly (A ⧸ P) x))
Tactic: constructor
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B ⧸ Q
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (minpoly (A ⧸ P) x))
have inr : ∀ (x : B),
  Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))
have inr : ∀ (val : Fintype G),
  Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))
Tactic: cases nonempty_fintype G
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))
have inr : ∀ (p : Polynomial A) (hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x))
  (h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)) (h₂ : p.Monic),
  Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))
Tactic: obtain ⟨p, hp, h₁, h₂⟩ := Polynomial.lifts_and_degree_eq_and_monic
    (Algebra.IsInvariant.charpoly_mem_lifts A B G x) (MulSemiringAction.monic_charpoly _ _)
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
have rw : Polynomial.eval₂ (algebraMap A B) x p = 0
Tactic: rw [Polynomial.aeval_def, ← Polynomial.eval_map, hp, MulSemiringAction.eval_charpoly]
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
rw : Polynomial.eval₂ (algebraMap A B) x p = 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
have rw₁ : Polynomial.eval x (Polynomial.map (algebraMap A B) p) = 0
Tactic: rw [Polynomial.aeval_def, ← Polynomial.eval_map, hp, MulSemiringAction.eval_charpoly]
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
rw : Polynomial.eval₂ (algebraMap A B) x p = 0
rw₁ : Polynomial.eval x (Polynomial.map (algebraMap A B) p) = 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
have rw₂ : Polynomial.eval x (MulSemiringAction.charpoly G x) = 0
Tactic: rw [Polynomial.aeval_def, ← Polynomial.eval_map, hp, MulSemiringAction.eval_charpoly]
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
rw : Polynomial.eval₂ (algebraMap A B) x p = 0
rw₁ : Polynomial.eval x (Polynomial.map (algebraMap A B) p) = 0
rw₂ : Polynomial.eval x (MulSemiringAction.charpoly G x) = 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
have rw₃ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [Polynomial.aeval_def, ← Polynomial.eval_map, hp, MulSemiringAction.eval_charpoly]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))
have H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
Tactic: have H : Polynomial.aeval x p = 0 := by
    rw [Polynomial.aeval_def, ← Polynomial.eval_map, hp, MulSemiringAction.eval_charpoly]
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B ⧸ Q)
    (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) :
            AlgHom.{u_1, u_1, u_2} (A ⧸ P) (Polynomial (A ⧸ P)) (B ⧸ Q)) :
          (a : Polynomial (A ⧸ P)) → B ⧸ Q)
        (Polynomial.map (algebraMap A (A ⧸ P)) p) :
      B ⧸ Q)
    (0 : B ⧸ Q)
have rw : Eq.{u_2 + 1} (α := B ⧸ Q)
  (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) : AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
        (a : Polynomial A) → B ⧸ Q)
      p :
    B ⧸ Q)
  (0 : B ⧸ Q)
Tactic: rw [Polynomial.aeval_map_algebraMap, Polynomial.aeval_algebraMap_apply, H, map_zero]
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
rw :
  Eq.{u_2 + 1} (α := B ⧸ Q)
    (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) :
            AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
          (a : Polynomial A) → B ⧸ Q)
        p :
      B ⧸ Q)
    (0 : B ⧸ Q)
⊢ Eq.{u_2 + 1} (α := B ⧸ Q)
    (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) :
            AlgHom.{u_1, u_1, u_2} (A ⧸ P) (Polynomial (A ⧸ P)) (B ⧸ Q)) :
          (a : Polynomial (A ⧸ P)) → B ⧸ Q)
        (Polynomial.map (algebraMap A (A ⧸ P)) p) :
      B ⧸ Q)
    (0 : B ⧸ Q)
have rw₁ : Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) ((Polynomial.aeval x : (a : Polynomial A) → B) p) : B ⧸ Q)
  (0 : B ⧸ Q)
Tactic: rw [Polynomial.aeval_map_algebraMap, Polynomial.aeval_algebraMap_apply, H, map_zero]
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
rw :
  Eq.{u_2 + 1} (α := B ⧸ Q)
    (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) :
            AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
          (a : Polynomial A) → B ⧸ Q)
        p :
      B ⧸ Q)
    (0 : B ⧸ Q)
rw₁ :
  Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) ((Polynomial.aeval x : (a : Polynomial A) → B) p) : B ⧸ Q)
    (0 : B ⧸ Q)
⊢ Eq.{u_2 + 1} (α := B ⧸ Q)
    (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) :
            AlgHom.{u_1, u_1, u_2} (A ⧸ P) (Polynomial (A ⧸ P)) (B ⧸ Q)) :
          (a : Polynomial (A ⧸ P)) → B ⧸ Q)
        (Polynomial.map (algebraMap A (A ⧸ P)) p) :
      B ⧸ Q)
    (0 : B ⧸ Q)
have rw₂ : Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0) 0
Tactic: rw [Polynomial.aeval_map_algebraMap, Polynomial.aeval_algebraMap_apply, H, map_zero]
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
rw :
  Eq.{u_2 + 1} (α := B ⧸ Q)
    (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) :
            AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
          (a : Polynomial A) → B ⧸ Q)
        p :
      B ⧸ Q)
    (0 : B ⧸ Q)
rw₁ :
  Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) ((Polynomial.aeval x : (a : Polynomial A) → B) p) : B ⧸ Q)
    (0 : B ⧸ Q)
rw₂ : Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0) 0
⊢ Eq.{u_2 + 1} (α := B ⧸ Q)
    (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) :
            AlgHom.{u_1, u_1, u_2} (A ⧸ P) (Polynomial (A ⧸ P)) (B ⧸ Q)) :
          (a : Polynomial (A ⧸ P)) → B ⧸ Q)
        (Polynomial.map (algebraMap A (A ⧸ P)) p) :
      B ⧸ Q)
    (0 : B ⧸ Q)
have rw₃ : Eq.{u_2 + 1} (α := B ⧸ Q) 0 0
Tactic: rw [Polynomial.aeval_map_algebraMap, Polynomial.aeval_algebraMap_apply, H, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))
have this₁ : Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
  (Polynomial.map (algebraMap A (A ⧸ P)) p)
Tactic: have := minpoly.dvd _ (algebraMap _ (B ⧸ Q) x) (p := p.map (algebraMap _ (A ⧸ P)))
    (by rw [Polynomial.aeval_map_algebraMap, Polynomial.aeval_algebraMap_apply, H, map_zero])
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this_1 : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
this :
  Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
    (Polynomial.map (algebraMap A (A ⧸ P)) p)
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))
have inr : Polynomial.Splits.{u_2} (R := B ⧸ Q)
  (Polynomial.map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (Polynomial.map (algebraMap A (A ⧸ P)) p))
Tactic: refine Polynomial.Splits.of_dvd ?_ ?_ ((Polynomial.map_dvd_map' _).mpr this)
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this_1 : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
this :
  Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
    (Polynomial.map (algebraMap A (A ⧸ P)) p)
inr :
  Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (Polynomial.map (algebraMap A (A ⧸ P)) p))
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))
have inr₁ : Ne.{u_2 + 1} (α := Polynomial (B ⧸ Q))
  (Polynomial.map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (Polynomial.map (algebraMap A (A ⧸ P)) p)) 0
Tactic: refine Polynomial.Splits.of_dvd ?_ ?_ ((Polynomial.map_dvd_map' _).mpr this)
-- 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_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this_1 : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
this :
  Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
    (Polynomial.map (algebraMap A (A ⧸ P)) p)
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (Polynomial.map (algebraMap A (A ⧸ P)) p))
have inr : Polynomial.Splits.{u_2} (R := B ⧸ Q)
  (∏ i : G,
    Polynomial.map (algebraMap B (B ⧸ Q))
      (HSub.hSub (α := Polynomial B) (β := Polynomial B) Polynomial.X
        ((Polynomial.C : (a : B) → Polynomial B) (i • x) : Polynomial B)))
Tactic: rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A B,
      ← Polynomial.map_map, hp, MulSemiringAction.charpoly_eq, Polynomial.map_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
inst_10 : SMulCommClass G A B
inst_11 : Algebra.IsSeparable.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
⊢ Module.Finite.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
have this : IsGalois.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
Tactic: have : IsGalois (A ⧸ P) (B ⧸ Q) := { __ := Ideal.Quotient.normal (A := A) G P Q }
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
inst_10 : SMulCommClass G A B
inst_11 : Algebra.IsSeparable.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
this : IsGalois.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
⊢ Module.Finite.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
have this₁ : Finite.{u_2 + 1} Gal((B ⧸ Q)/A ⧸ P)
Tactic: have := Finite.of_surjective _ (Ideal.Quotient.stabilizerHom_surjective G P Q)
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
⊢ Algebra.IsInvariant K L G
have refine : ∀ (x : L) (h : ∀ (g : G), g • x = x), ∃ (a : K), (algebraMap K L : (a : K) → L) a = x
Tactic: refine ⟨fun x h ↦ ?_⟩