awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
have this : HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]) = minpoly K α
Tactic: have : X ^ (finrank K L) - C a = minpoly K α := by
    refine minpoly.unique _ _ (monic_X_pow_sub_C _ finrank_pos.ne.symm) ?_ ?_
    · simp only [aeval_def, eval₂_sub, eval₂_X_pow, ha, eval₂_C, sub_self]
    · intro q hq hq'
      refine le_trans ?_ (degree_le_of_dvd (minpoly.dvd _ _ hq') hq.ne_zero)
      rw [degree_X_pow_sub_C finrank_pos,
        degree_eq_natDegree (minpoly.ne_zero (IsIntegral.of_finite K α)),
        ← IntermediateField.adjoin.finrank (IsIntegral.of_finite K α), hα, Nat.cast_le]
      exact (finrank_top K L).ge
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ IsSplittingField K L
    (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
have splits' : Splits
  (Polynomial.map (algebraMap K L)
    (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])))
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
splits' :
  Splits
    (Polynomial.map (algebraMap K L)
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])))
⊢ IsSplittingField K L
    (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
have adjoin_rootSet' : Eq (α := Subalgebra K L)
  (Algebra.adjoin K
    ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L))
  ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ Splits
    (Polynomial.map (algebraMap K L)
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])))
have splits' : (HSub.hSub (β := L[X]) (HPow.hPow (α := L[X]) X (finrank K L))
    ((C : (a : L) → L[X]) (((algebraMap K L : K →+* L) : (a : K) → L) a) : L[X])).Splits
Tactic: rw [Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_C,
      Polynomial.map_X]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ (HSub.hSub (β := L[X]) (HPow.hPow (α := L[X]) X (finrank K L))
      ((C : (a : L) → L[X]) (((algebraMap K L : K →+* L) : (a : K) → L) a) : L[X])).Splits
have splits' : ∀ (w : K) (hζ : w ∈ primitiveRoots (finrank K L) K),
  (HSub.hSub (β := L[X]) (HPow.hPow (α := L[X]) X (finrank K L))
      ((C : (a : L) → L[X]) (((algebraMap K L : K →+* L) : (a : K) → L) a) : L[X])).Splits
Tactic: have ⟨_, hζ⟩ := hK
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
w : K
hζ : w ∈ primitiveRoots (finrank K L) K
⊢ (HSub.hSub (β := L[X]) (HPow.hPow (α := L[X]) X (finrank K L))
      ((C : (a : L) → L[X]) (((algebraMap K L : K →+* L) : (a : K) → L) a) : L[X])).Splits
have hζ₁ : IsPrimitiveRoot w (finrank K L)
Tactic: rw [mem_primitiveRoots finrank_pos] at hζ
Cleared hypotheses: hζ
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ Eq (α := Subalgebra K L)
    (Algebra.adjoin K
      ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L))
    ⊤
have adjoin_rootSet' : LE.le (α := Subalgebra K L) K [α]
  (Algebra.adjoin K
    ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L))
Tactic: rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← hα,
      IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite K α)]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ LE.le (α := Subalgebra K L) K [α]
    (Algebra.adjoin K
      ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L))
have adjoin_rootSet' : {α} ⊆ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
Tactic: apply Algebra.adjoin_mono
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ {α} ⊆ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
have adjoin_rootSet' : α ∈ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
Tactic: rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
adjoin_rootSet' :
  α ∈ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
⊢ {α} ⊆ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
have adjoin_rootSet'₁ : Eq.{u_1 + 1} (α := L)
  ((aeval α : (a : K [X]) → L)
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) :
    L)
  (0 : L)
Tactic: rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
adjoin_rootSet' :
  α ∈ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
adjoin_rootSet'₁ :
  Eq.{u_1 + 1} (α := L)
    ((aeval α : (a : K [X]) → L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) :
      L)
    (0 : L)
⊢ {α} ⊆ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
have adjoin_rootSet'₂ : eval₂ (algebraMap K L) α
    (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) =
  0
Tactic: rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
adjoin_rootSet' :
  α ∈ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
adjoin_rootSet'₁ :
  Eq.{u_1 + 1} (α := L)
    ((aeval α : (a : K [X]) → L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) :
      L)
    (0 : L)
adjoin_rootSet'₂ :
  eval₂ (algebraMap K L) α
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) =
    0
⊢ {α} ⊆ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
have adjoin_rootSet'₃ : eval₂ (algebraMap K L) α (HPow.hPow (α := K [X]) X (finrank K L)) -
    eval₂ (algebraMap K L : K →+* L) α ((C : (a : K) → K [X]) a) =
  0
Tactic: rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
adjoin_rootSet' :
  α ∈ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
adjoin_rootSet'₁ :
  Eq.{u_1 + 1} (α := L)
    ((aeval α : (a : K [X]) → L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) :
      L)
    (0 : L)
adjoin_rootSet'₂ :
  eval₂ (algebraMap K L) α
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) =
    0
adjoin_rootSet'₃ :
  eval₂ (algebraMap K L) α (HPow.hPow (α := K [X]) X (finrank K L)) -
      eval₂ (algebraMap K L : K →+* L) α ((C : (a : K) → K [X]) a) =
    0
⊢ {α} ⊆ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
have adjoin_rootSet'₄ : α ^ finrank K L - eval₂ (algebraMap K L : K →+* L) α ((C : (a : K) → K [X]) a) = 0
Tactic: rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
adjoin_rootSet' :
  α ∈ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
adjoin_rootSet'₁ :
  Eq.{u_1 + 1} (α := L)
    ((aeval α : (a : K [X]) → L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) :
      L)
    (0 : L)
adjoin_rootSet'₂ :
  eval₂ (algebraMap K L) α
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) =
    0
adjoin_rootSet'₃ :
  eval₂ (algebraMap K L) α (HPow.hPow (α := K [X]) X (finrank K L)) -
      eval₂ (algebraMap K L : K →+* L) α ((C : (a : K) → K [X]) a) =
    0
adjoin_rootSet'₄ : α ^ finrank K L - eval₂ (algebraMap K L : K →+* L) α ((C : (a : K) → K [X]) a) = 0
⊢ {α} ⊆ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
have adjoin_rootSet'₅ : HSub.hSub (β := L) (α ^ finrank K L) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = 0
Tactic: rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
adjoin_rootSet' :
  α ∈ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
adjoin_rootSet'₁ :
  Eq.{u_1 + 1} (α := L)
    ((aeval α : (a : K [X]) → L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) :
      L)
    (0 : L)
adjoin_rootSet'₂ :
  eval₂ (algebraMap K L) α
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) =
    0
adjoin_rootSet'₃ :
  eval₂ (algebraMap K L) α (HPow.hPow (α := K [X]) X (finrank K L)) -
      eval₂ (algebraMap K L : K →+* L) α ((C : (a : K) → K [X]) a) =
    0
adjoin_rootSet'₄ : α ^ finrank K L - eval₂ (algebraMap K L : K →+* L) α ((C : (a : K) → K [X]) a) = 0
adjoin_rootSet'₅ : HSub.hSub (β := L) (α ^ finrank K L) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = 0
⊢ {α} ⊆ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
have adjoin_rootSet'₆ : HSub.hSub (α := L) (β := L) ((algebraMap K L : (a : K) → L) a : L) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) =
  0
Tactic: rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
adjoin_rootSet' :
  α ∈ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
adjoin_rootSet'₁ :
  Eq.{u_1 + 1} (α := L)
    ((aeval α : (a : K [X]) → L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) :
      L)
    (0 : L)
adjoin_rootSet'₂ :
  eval₂ (algebraMap K L) α
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) =
    0
adjoin_rootSet'₃ :
  eval₂ (algebraMap K L) α (HPow.hPow (α := K [X]) X (finrank K L)) -
      eval₂ (algebraMap K L : K →+* L) α ((C : (a : K) → K [X]) a) =
    0
adjoin_rootSet'₄ : α ^ finrank K L - eval₂ (algebraMap K L : K →+* L) α ((C : (a : K) → K [X]) a) = 0
adjoin_rootSet'₅ : HSub.hSub (β := L) (α ^ finrank K L) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = 0
adjoin_rootSet'₆ :
  HSub.hSub (α := L) (β := L) ((algebraMap K L : (a : K) → L) a : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) a : L) =
    0
⊢ {α} ⊆ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).rootSet L
have adjoin_rootSet'₇ : Eq.{u_1 + 1} (α := L) 0 0
Tactic: rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
⊢ [IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K),
      ∃ (a : K),
        Irreducible
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
          IsSplittingField K L
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])),
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤].TFAE
have this : NeZero (finrank K L)
Tactic: have : NeZero (Module.finrank K L) := NeZero.of_pos finrank_pos
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
⊢ [IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K),
      ∃ (a : K),
        Irreducible
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
          IsSplittingField K L
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])),
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤].TFAE
have tfae_1_to_3 : ∀ (a : IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)),
  ∃ (α : L),
    Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
        (α ^ finrank K L) ∧
      Eq (α := IntermediateField K L) K⟮α⟯ ⊤
Tactic: tfae_have 1 → 3
  | ⟨inst₁, inst₂⟩ => exists_root_adjoin_eq_top_of_isCyclic K L hK
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 :
  ∀ (a : IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ [IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K),
      ∃ (a : K),
        Irreducible
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
          IsSplittingField K L
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])),
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤].TFAE
have tfae_3_to_2 : ∀
  (a :
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤),
  ∃ (a : K),
    Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
      IsSplittingField K L
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
Tactic: tfae_have 3 → 2
  | ⟨α, ⟨a, ha⟩, hα⟩ => ⟨a, irreducible_X_pow_sub_C_of_root_adjoin_eq_top ha.symm hα,
      isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top hK ha.symm hα⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 :
  ∀ (a : IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
tfae_3_to_2 :
  ∀
    (a :
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤),
    ∃ (a : K),
      Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
        IsSplittingField K L
          (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
⊢ [IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K),
      ∃ (a : K),
        Irreducible
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
          IsSplittingField K L
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])),
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤].TFAE
have tfae_2_to_1 : ∀
  (a :
    ∃ (a : K),
      Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
        IsSplittingField K L
          (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))),
  IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)
Tactic: tfae_have 2 → 1
  | ⟨a, H, inst⟩ => ⟨isGalois_of_isSplittingField_X_pow_sub_C hK H L,
      isCyclic_of_isSplittingField_X_pow_sub_C hK H L⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n =
    (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
      a
have rw : HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
    (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
    ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
        a :
      AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
  0
Tactic: rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]