awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : Algebra K K[n√a] := inferInstance
this : n ≠ 0
adjoin_rootSet' :
  Membership.mem (γ := Set K[n√a])
    ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).rootSet K[n√a])
    (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
adjoin_rootSet'₁ :
  Eq (α := K[n√a])
    ((aeval (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
        (a_1 : K [X]) → K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
    0
adjoin_rootSet'₂ :
  eval₂ (algebraMap K K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    0
adjoin_rootSet'₃ :
  eval₂ (of (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])))
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    0
adjoin_rootSet'₄ adjoin_rootSet'₅ : Eq.{u + 1} (α := K[n√a]) 0 0
⊢ Subset (α := Set K[n√a])
    {root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))}
    ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).rootSet K[n√a])

Tactic:
rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero
      (Nat.pos_of_ne_zero this) a), aeval_def, AdjoinRoot.algebraMap_eq, AdjoinRoot.eval₂_root]

Premises used: Set.singleton_subset_iff, AdjoinRoot.algebraMap_eq, Polynomial.aeval_def, Nat.pos_of_ne_zero, AdjoinRoot.eval₂_root, Polynomial.mem_rootSet_of_ne, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
⊢ eval₂ (↑(Algebra.ofId K L) : K →+* L) α
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    0

Tactic:
simp [hα]
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
⊢ Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
haveI := Fact.mk H
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : IsSplittingField K K[n√a]
  (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :=
  ⋯
⊢ Function.Bijective.{u + 1, u_1 + 1} (α := K[n√a]) (β := L)
    (⇑(liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K L) α ⋯) :
      (a : K[n√a]) → L)

Tactic:
⟨(liftAlgHom (X ^ n - C a) _ α _).injective, ?_⟩

Premises used: Polynomial.C, HSub.hSub, RingHom.injective, HPow.hPow, AlgHom.toRingHom, And.intro, Function.Bijective, AdjoinRoot.liftAlgHom, Polynomial.X, DFunLike.coe
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : IsSplittingField K K[n√a]
  (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :=
  ⋯
refine :
  Function.Surjective.{u + 1, u_1 + 1} (α := K[n√a]) (β := L)
    (⇑(liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K L) α ⋯) :
      (a : K[n√a]) → L)
⊢ Function.Bijective.{u + 1, u_1 + 1} (α := K[n√a]) (β := L)
    (⇑(liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K L) α ⋯) :
      (a : K[n√a]) → L)

Tactic:
refine ⟨(liftAlgHom (X ^ n - C a) _ α _).injective, ?_⟩
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : IsSplittingField K K[n√a]
  (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :=
  ⋯
hf :
  Splits (R := K[n√a])
    (Polynomial.map (algebraMap K K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
⊢ Function.Surjective.{u + 1, u_1 + 1} (α := K[n√a]) (β := L)
    (⇑(liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K L) α ⋯) :
      (a : K[n√a]) → L)

Tactic:
rw [← AlgHom.range_eq_top, ← IsSplittingField.adjoin_rootSet _ (X ^ n - C a),
      eq_comm, Splits.adjoin_rootSet_eq_range, IsSplittingField.adjoin_rootSet]

Premises used: Polynomial.C, Polynomial.IsSplittingField.adjoin_rootSet, HSub.hSub, Polynomial.Splits.adjoin_rootSet_eq_range, eq_comm, AlgHom.range_eq_top, HPow.hPow, Polynomial.X, DFunLike.coe
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : IsSplittingField K K[n√a]
  (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :=
  ⋯
⊢ Splits (R := K[n√a])
    (Polynomial.map (algebraMap K K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
IsSplittingField.splits _ _

Premises used: Polynomial.IsSplittingField.splits
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : IsSplittingField K K[n√a]
  (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :=
  ⋯
⊢ Splits (R := K[n√a])
    (Polynomial.map (algebraMap K K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
exact IsSplittingField.splits _ _

Premises used: Polynomial.IsSplittingField.splits
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
rw :
  (AlgEquiv.ofBijective
          (liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
            (Algebra.ofId K L) α ⋯)
          ⋯ :
        (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    α
rw₁ :
  (liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) (Algebra.ofId K L)
          α ⋯ :
        (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    α
rw₂ rw₃ : α = α
⊢ (adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    α

Tactic:
rw [adjoinRootXPowSubCEquiv, AlgEquiv.coe_ofBijective, liftAlgHom_root]

Premises used: AlgEquiv.coe_ofBijective, AdjoinRoot.liftAlgHom_root, adjoinRootXPowSubCEquiv
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
a₁ :
  Eq.{u_1 + 1} (α := L)
    ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
        (((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α : K[n√a]) :
      L)
    ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
      L)
⊢ ((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α =
    root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))

Tactic:
apply (adjoinRootXPowSubCEquiv hζ H hα).injective

Premises used: AlgEquiv.injective, adjoinRootXPowSubCEquiv
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
a₁ :
  α =
    (adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
a₂ a₃ : α = α
⊢ Eq.{u_1 + 1} (α := L)
    ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
        (((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α : K[n√a]) :
      L)
    ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
      L)

Tactic:
rw [(adjoinRootXPowSubCEquiv hζ H hα).apply_symm_apply, adjoinRootXPowSubCEquiv_root]

Premises used: AlgEquiv.apply_symm_apply, adjoinRootXPowSubCEquiv_root, adjoinRootXPowSubCEquiv
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
a₁ :
  Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤
⊢ Eq (α := Subalgebra K L) K [α] ⊤

Tactic:
apply Subalgebra.map_injective (B := K[n√a]) (f := (adjoinRootXPowSubCEquiv hζ H hα).symm)
    (adjoinRootXPowSubCEquiv hζ H hα).symm.injective

Premises used: Subalgebra.map_injective
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
a₁ :
  Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]).range
a₂ : Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] = ⊤
a₃ :
  Eq (α := Subalgebra K K[n√a])
    (adjoin K
      (Set.image (α := L) (⇑(↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) {α}))
    ⊤
a₄ :
  Eq (α := Subalgebra K K[n√a])
    K [(((↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) α : K[n√a])] ⊤
a₅ : Eq (α := Subalgebra K K[n√a]) K [(((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α : K[n√a])] ⊤
a₆ :
  Eq (α := Subalgebra K K[n√a])
    K [root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))] ⊤
a₇ a₈ : Eq.{u + 1} (α := Subalgebra K K[n√a]) ⊤ ⊤
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤

Tactic:
rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
    (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgEquiv.coe_algHom, adjoinRootXPowSubCEquiv_symm_eq_root,
      adjoinRoot_eq_top]

Premises used: Iff.mpr, adjoinRootXPowSubCEquiv_symm_eq_root, Set.image_singleton, AlgHom.map_adjoin, AlgHom.range_eq_top, AlgEquiv.coe_algHom, Algebra.map_top, AdjoinRoot.adjoinRoot_eq_top
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
⊢ Eq (α := IntermediateField K L) K⟮α⟯ ⊤

Tactic:
(IntermediateField.eq_adjoin_of_eq_algebra_adjoin _ _ _ ?_).symm

Premises used: Eq.symm, IntermediateField.eq_adjoin_of_eq_algebra_adjoin
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
refine : Eq (α := Subalgebra K L) (toSubalgebra ⊤) K [α]
⊢ Eq (α := IntermediateField K L) K⟮α⟯ ⊤

Tactic:
refine (IntermediateField.eq_adjoin_of_eq_algebra_adjoin _ _ _ ?_).symm

Premises used: Eq.symm, IntermediateField.eq_adjoin_of_eq_algebra_adjoin
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
⊢ Eq (α := Subalgebra K L) (toSubalgebra ⊤) K [α]

Tactic:
(Algebra.adjoin_root_eq_top_of_isSplittingField hζ H hα).symm

Premises used: Algebra.adjoin_root_eq_top_of_isSplittingField, Eq.symm, Subalgebra.copy
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
⊢ Eq (α := Subalgebra K L) (toSubalgebra ⊤) K [α]

Tactic:
exact (Algebra.adjoin_root_eq_top_of_isSplittingField hζ H hα).symm

Premises used: Algebra.adjoin_root_eq_top_of_isSplittingField, Eq.symm
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a_1 : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a_1 : K [X]))
L_1 : Type u_1
inst_1 : Field L_1
inst_2 : Algebra K L_1
inst_3 :
  IsSplittingField K L_1 (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a_1 : K [X]))
α : L_1
hα : α ^ n = (algebraMap K L_1 : (a : K) → L_1) a_1
hn : 0 < n
a : K
L : Type u_2
inst_4 : Field L
inst_5 : Algebra K L
inst_6 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
⊢ degree
      (Polynomial.map (algebraMap K L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ≠
    0

Tactic:
simpa [degree_X_pow_sub_C hn] using Nat.pos_iff_ne_zero.mp hn

Premises used: Nat.pos_iff_ne_zero, Polynomial.degree_X_pow_sub_C, Iff.mp
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_4 : NeZero n
⊢ degree
      (Polynomial.map (algebraMap K L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ≠
    0

Tactic:
simp [degree_X_pow_sub_C (NeZero.pos n), NeZero.ne n]

Premises used: Polynomial.degree_X_pow_sub_C, NeZero.pos, NeZero.ne
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_4 : NeZero n
⊢ eval
      (rootOfSplits (f :=
        Polynomial.map (algebraMap K L)
          (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
        ⋯ ⋯)
      (Polynomial.map (algebraMap K L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    0

Tactic:
have := eval_rootOfSplits (IsSplittingField.splits L (X ^ n - C a))
    (by simp [degree_X_pow_sub_C (NeZero.pos n), NeZero.ne n])
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_4 : NeZero n
this :
  eval
      (rootOfSplits (f :=
        Polynomial.map (algebraMap K L)
          (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
        ⋯ ⋯)
      (Polynomial.map (algebraMap K L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    0
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L : (a : K) → L) a

Tactic:
simpa only [eval_map, eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] using this

Premises used: Polynomial.eval_map, Polynomial.eval₂_X_pow, sub_eq_zero, Polynomial.eval₂_sub, Polynomial.eval₂_C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_4 : NeZero n
σ : Gal(L/K)
obtain :
  ∀ (η : ↥(rootsOfUnity n K)),
    (((MulEquiv.symm (autEquivRootsOfUnity hζ H L) : (a : ↥(rootsOfUnity n K)) → Gal(L/K)) η : Gal(L/K)) : (a : L) → L)
        (rootOfSplitsXPowSubC ⋯ a L) =
      HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
        (((autEquivRootsOfUnity hζ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
              (a : Gal(L/K)) → ↥(rootsOfUnity n K))
            ((MulEquiv.symm (autEquivRootsOfUnity hζ H L) : (a : ↥(rootsOfUnity n K)) → Gal(L/K)) η) :
          ↥(rootsOfUnity n K))
        (rootOfSplitsXPowSubC ⋯ a L)
⊢ (σ : (a : L) → L) (rootOfSplitsXPowSubC ⋯ a L) =
    HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity hζ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
            (a : Gal(L/K)) → ↥(rootsOfUnity n K))
          σ :
        ↥(rootsOfUnity n K))
      (rootOfSplitsXPowSubC ⋯ a L)

Tactic:
obtain ⟨η, rfl⟩ := (autEquivRootsOfUnity hζ H L).symm.surjective σ

Premises used: MulEquiv.surjective, autEquivRootsOfUnity, MulEquiv.symm, rfl