awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KummerExtension
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
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this_1 : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
k : ℕ
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    (σ ^ (finrank K L * k))
this : ζ ^ (finrank K L * k) • v = HSMul.hSMul.{u, u_1, u_1} (α := K) 1 v
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ 1

Tactic:
one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.FieldTheory.KummerExtension
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
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this_1 : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
k : ℕ
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    (σ ^ (finrank K L * k))
this : ζ ^ (finrank K L * k) • v = HSMul.hSMul.{u, u_1, u_1} (α := K) 1 v
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ 1

Tactic:
exact one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
⊢ HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]) = minpoly K α

Tactic:
minpoly.unique _ _ (monic_X_pow_sub_C _ finrank_pos.ne.symm) ?_ ?_

Premises used: minpoly.unique, Polynomial.monic_X_pow_sub_C, Ne.symm, Module.finrank_pos, LT.lt.ne
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
refine_1 :
  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)
refine_2 :
  ∀ (q : K [X]),
    q.Monic →
      Eq.{u_1 + 1} (α := L) ((aeval α : (a : K [X]) → L) q : L) (0 : L) →
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).degree ≤
          q.degree
⊢ HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]) = minpoly K α

Tactic:
refine minpoly.unique _ _ (monic_X_pow_sub_C _ finrank_pos.ne.symm) ?_ ?_

Premises used: minpoly.unique, Polynomial.monic_X_pow_sub_C, Ne.symm, Module.finrank_pos, LT.lt.ne
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
⊢ 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:
simp only [aeval_def, eval₂_sub, eval₂_X_pow, ha, eval₂_C, sub_self]

Premises used: Polynomial.eval₂_X_pow, sub_self, Polynomial.eval₂_sub, Polynomial.aeval_def, Polynomial.eval₂_C
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
q : K [X]
hq : q.Monic
hq' : Eq.{u_1 + 1} (α := L) ((aeval α : (a : K [X]) → L) q : L) (0 : L)
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).degree ≤ q.degree

Tactic:
le_trans ?_ (degree_le_of_dvd (minpoly.dvd _ _ hq') hq.ne_zero)

Premises used: Polynomial.degree_le_of_dvd, minpoly.dvd, Polynomial.Monic.ne_zero, le_trans
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
q : K [X]
hq : q.Monic
hq' : Eq.{u_1 + 1} (α := L) ((aeval α : (a : K [X]) → L) q : L) (0 : L)
refine_2 :
  (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).degree ≤
    degree (minpoly K α)
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).degree ≤ q.degree

Tactic:
refine le_trans ?_ (degree_le_of_dvd (minpoly.dvd _ _ hq') hq.ne_zero)

Premises used: Polynomial.degree_le_of_dvd, minpoly.dvd, Polynomial.Monic.ne_zero, le_trans
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
q : K [X]
hq : q.Monic
hq' : Eq.{u_1 + 1} (α := L) ((aeval α : (a : K [X]) → L) q : L) (0 : L)
refine_2 : finrank K L ≤ finrank.{u, u_1} K ↥⊤
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).degree ≤
    degree (minpoly K α)

Tactic:
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]

Premises used: IntermediateField.adjoin.finrank, Polynomial.degree_eq_natDegree, Polynomial.degree_X_pow_sub_C, IsIntegral.of_finite, Nat.cast_le, minpoly.ne_zero, Module.finrank_pos
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
q : K [X]
hq : q.Monic
hq' : Eq.{u_1 + 1} (α := L) ((aeval α : (a : K [X]) → L) q : L) (0 : L)
⊢ finrank K L ≤ finrank.{u, u_1} K ↥⊤

Tactic:
(finrank_top K L).ge

Premises used: IntermediateField.copy, Eq.ge, Set.Mem, finrank_top
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
q : K [X]
hq : q.Monic
hq' : Eq.{u_1 + 1} (α := L) ((aeval α : (a : K [X]) → L) q : L) (0 : L)
⊢ finrank K L ≤ finrank.{u, u_1} K ↥⊤

Tactic:
exact (finrank_top K L).ge

Premises used: Eq.ge, finrank_top
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
⊢ 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
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
this : HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]) = minpoly K α
⊢ Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))

Tactic:
this ▸ minpoly.irreducible (IsIntegral.of_finite K α)

Premises used: Eq.rec, IsIntegral.of_finite, Eq.symm, minpoly.irreducible
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
this : HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]) = minpoly K α
⊢ Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))

Tactic:
exact this ▸ minpoly.irreducible (IsIntegral.of_finite K α)
-- Module: Mathlib.FieldTheory.KummerExtension
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])))
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))
    ⊤
⊢ IsSplittingField K L
    (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))

Tactic:
constructor
-- Module: Mathlib.FieldTheory.KummerExtension
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' :
  (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
⊢ 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:
rw [Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_C,
      Polynomial.map_X]

Premises used: Polynomial.map_pow, Polynomial.map_X, Polynomial.map_sub, Polynomial.map_C
-- Module: Mathlib.FieldTheory.KummerExtension
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' :
  ∀ (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
⊢ (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
-- Module: Mathlib.FieldTheory.KummerExtension
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
⊢ IsPrimitiveRoot w (finrank K L)

Tactic:
rw [mem_primitiveRoots finrank_pos] at hζ

Premises used: mem_primitiveRoots, Module.finrank_pos
-- Module: Mathlib.FieldTheory.KummerExtension
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ζ : IsPrimitiveRoot w (finrank K L)
⊢ (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:
X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective) ha

Premises used: X_pow_sub_C_splits_of_isPrimitiveRoot, Algebra.algebraMap, RingHom.injective, IsPrimitiveRoot.map_of_injective
-- Module: Mathlib.FieldTheory.KummerExtension
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ζ : IsPrimitiveRoot w (finrank K L)
⊢ (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:
exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective) ha

Premises used: X_pow_sub_C_splits_of_isPrimitiveRoot, Algebra.algebraMap, RingHom.injective, IsPrimitiveRoot.map_of_injective
-- Module: Mathlib.FieldTheory.KummerExtension
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' :
  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))
⊢ 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:
rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← hα,
      IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite K α)]

Premises used: IsAlgebraic.of_finite, eq_top_iff, IntermediateField.top_toSubalgebra, IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-- Module: Mathlib.FieldTheory.KummerExtension
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
⊢ 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:
apply Algebra.adjoin_mono

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.FieldTheory.KummerExtension
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
adjoin_rootSet'₇ adjoin_rootSet'₈ : Eq.{u_1 + 1} (α := L) 0 0
⊢ {α} ⊆ (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]

Premises used: Set.singleton_subset_iff, Polynomial.eval₂_X_pow, sub_self, Polynomial.eval₂_sub, Polynomial.aeval_def, Polynomial.eval₂_C, Polynomial.mem_rootSet_of_ne, Module.finrank_pos, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.FieldTheory.KummerExtension
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
⊢ NeZero (finrank K L)

Tactic:
have : NeZero (Module.finrank K L) := NeZero.of_pos finrank_pos
-- Module: Mathlib.FieldTheory.KummerExtension
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)

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.KummerExtension
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)
⊢ ∃ (α : 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:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.KummerExtension
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)
⊢ ∀ (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:
1 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.KummerExtension
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)
⊢ ∀ (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
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
⊢ ∃ (α : 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:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
⊢ ∃ (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:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
⊢ ∀
    (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:
3 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.KummerExtension
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⟮α⟯ ⊤
⊢ ∀
    (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α⟩