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]))
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
η : ↥(rootsOfUnity n K)
rw :
  (((MulEquiv.symm
                (MulEquiv.trans
                  (AlgEquiv.autCongr
                    (AlgEquiv.symm (adjoinRootXPowSubCEquiv (α := rootOfSplitsXPowSubC (n := n) ⋯ a L) hζ H ⋯)))
                  (autAdjoinRootXPowSubCEquiv hζ H).symm) :
              (a : ↥(rootsOfUnity n K)) → Gal(L/K))
            η :
          Gal(L/K)) :
        (a : L) → L)
      (rootOfSplitsXPowSubC ⋯ a L) =
    η • rootOfSplitsXPowSubC ⋯ a L
⊢ (((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)

Tactic:
rw [MulEquiv.apply_symm_apply, autEquivRootsOfUnity]

Premises used: autEquivRootsOfUnity, MulEquiv.apply_symm_apply
-- 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
η : ↥(rootsOfUnity n K)
simp : (↑(↑η : Kˣ) : K) • rootOfSplitsXPowSubC (n := n) ⋯ a L = η • rootOfSplitsXPowSubC ⋯ a L
⊢ (((MulEquiv.symm
                (MulEquiv.trans
                  (AlgEquiv.autCongr
                    (AlgEquiv.symm (adjoinRootXPowSubCEquiv (α := rootOfSplitsXPowSubC (n := n) ⋯ a L) hζ H ⋯)))
                  (autAdjoinRootXPowSubCEquiv hζ H).symm) :
              (a : ↥(rootsOfUnity n K)) → Gal(L/K))
            η :
          Gal(L/K)) :
        (a : L) → L)
      (rootOfSplitsXPowSubC ⋯ a L) =
    η • rootOfSplitsXPowSubC ⋯ a L

Tactic:
simp only [MulEquiv.symm_trans_apply, AlgEquiv.autCongr_symm, AlgEquiv.symm_symm,
    MulEquiv.symm_symm, AlgEquiv.autCongr_apply, AlgEquiv.trans_apply,
    adjoinRootXPowSubCEquiv_symm_eq_root, autAdjoinRootXPowSubCEquiv_root, map_smul,
    adjoinRootXPowSubCEquiv_root]

Premises used: autAdjoinRootXPowSubCEquiv_root, adjoinRootXPowSubCEquiv_symm_eq_root, AlgEquiv.autCongr_symm, MulEquiv.symm_trans_apply, adjoinRootXPowSubCEquiv_root, AlgEquiv.autCongr_apply, AlgEquiv.trans_apply, MulEquiv.symm_symm, AlgEquiv.symm_symm, map_smul
-- 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
η : ↥(rootsOfUnity n K)
⊢ (↑(↑η : Kˣ) : K) • rootOfSplitsXPowSubC (n := n) ⋯ a L = η • rootOfSplitsXPowSubC ⋯ a L

Tactic:
rfl
-- 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
inst_4 : NeZero n
σ : Gal(L/K)
have :
  ∀ (ζ : K) (hζ' : ζ ∈ primitiveRoots n K),
    HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
        (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
              (a : Gal(L/K)) → ↥(rootsOfUnity n K))
            σ :
          ↥(rootsOfUnity n K))
        α =
      (σ : (a : L) → 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))
      α =
    (σ : (a : L) → L) α

Tactic:
have ⟨ζ, hζ'⟩ := hζ
-- 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
inst_4 : NeZero n
σ : Gal(L/K)
ζ : K
hζ' : ζ ∈ primitiveRoots n K
⊢ 0 < n

Tactic:
have hn := NeZero.pos n
-- 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
inst_4 : NeZero n
σ : Gal(L/K)
ζ : K
hζ' : ζ ∈ primitiveRoots n K
hn : 0 < n
⊢ IsPrimitiveRoot ζ n

Tactic:
rw [mem_primitiveRoots hn] at hζ'

Premises used: mem_primitiveRoots
-- 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
inst_4 : NeZero n
σ : Gal(L/K)
ζ : K
hζ' : ζ ∈ primitiveRoots n K
hn : 0 < n
hζ'₁ : IsPrimitiveRoot ζ n
⊢ 0 < n

Tactic:
rw [mem_primitiveRoots hn] at hζ'

Premises used: mem_primitiveRoots
-- 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
inst_4 : NeZero n
σ : Gal(L/K)
ζ : K
hζ'_1 : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
rw :
  ∀ [inst_5 : NeZero n] (σ : Gal(L/K)) (ζ : K)
    (hα :
      Membership.mem (γ := Multiset L)
        (Multiset.map
          (fun (x : ℕ) ↦
            HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) x * rootOfSplitsXPowSubC ⋯ a L)
          (Multiset.range n))
        α)
    (hζ' : ζ ∈ primitiveRoots n K) (hζ'_2 : IsPrimitiveRoot ζ n) (hn : 0 < n),
    HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
        (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
              (a : Gal(L/K)) → ↥(rootsOfUnity n K))
            σ :
          ↥(rootsOfUnity n K))
        α =
      (σ : (a : L) → L) α
⊢ HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
            (a : Gal(L/K)) → ↥(rootsOfUnity n K))
          σ :
        ↥(rootsOfUnity n K))
      α =
    (σ : (a : L) → L) α

Tactic:
rw [← mem_nthRoots hn, (hζ'.map_of_injective (algebraMap K L).injective).nthRoots_eq
    (rootOfSplitsXPowSubC_pow a L)] at hα

Premises used: Algebra.algebraMap, RingHom.injective, rootOfSplitsXPowSubC_pow, IsPrimitiveRoot.map_of_injective, Polynomial.mem_nthRoots, IsPrimitiveRoot.nthRoots_eq
-- 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
inst_4 : NeZero n
σ : Gal(L/K)
ζ : K
hα :
  Membership.mem (γ := Multiset L)
    (Multiset.map
      (fun (x : ℕ) ↦
        HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) x * rootOfSplitsXPowSubC ⋯ a L)
      (Multiset.range n))
    α
hζ'_1 : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ ∃ a_1 < n, HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) a_1 * rootOfSplitsXPowSubC ⋯ a L = α

Tactic:
simp only [Multiset.mem_map, Multiset.mem_range] at hα

Premises used: Multiset.mem_map, Multiset.mem_range
-- 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
inst_4 : NeZero n
σ : Gal(L/K)
ζ : K
hζ'_1 : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
hα :
  ∃ a_1 < n, HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) a_1 * rootOfSplitsXPowSubC ⋯ a L = α
obtain :
  ∀ i < n,
    HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
        (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
              (a : Gal(L/K)) → ↥(rootsOfUnity n K))
            σ :
          ↥(rootsOfUnity n K))
        (HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) i * rootOfSplitsXPowSubC ⋯ a L) =
      (σ : (a : L) → L)
        (HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) i * rootOfSplitsXPowSubC ⋯ a L)
⊢ HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
            (a : Gal(L/K)) → ↥(rootsOfUnity n K))
          σ :
        ↥(rootsOfUnity n K))
      α =
    (σ : (a : L) → L) α

Tactic:
obtain ⟨i, _, rfl⟩ := hα

Premises used: rfl
-- 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)
ζ : K
hζ'_1 : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left : i < n
simp :
  HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
            (a : Gal(L/K)) → ↥(rootsOfUnity n K))
          σ :
        ↥(rootsOfUnity n K))
      (ζ ^ i • rootOfSplitsXPowSubC ⋯ a L) =
    ζ ^ i •
      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)
⊢ HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
            (a : Gal(L/K)) → ↥(rootsOfUnity n K))
          σ :
        ↥(rootsOfUnity n K))
      (HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) i * rootOfSplitsXPowSubC ⋯ a L) =
    (σ : (a : L) → L)
      (HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) i * rootOfSplitsXPowSubC ⋯ a L)

Tactic:
simp only [← map_pow, ← Algebra.smul_def, map_smul,
    autEquivRootsOfUnity_apply_rootOfSplit hζ H L]

Premises used: map_pow, Algebra.smul_def, autEquivRootsOfUnity_apply_rootOfSplit, map_smul
-- 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)
ζ : K
hζ'_1 : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left : i < n
⊢ HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
            (a : Gal(L/K)) → ↥(rootsOfUnity n K))
          σ :
        ↥(rootsOfUnity n K))
      (ζ ^ i • rootOfSplitsXPowSubC ⋯ a L) =
    ζ ^ i •
      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:
smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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)
ζ : K
hζ'_1 : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left : i < n
⊢ HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
            (a : Gal(L/K)) → ↥(rootsOfUnity n K))
          σ :
        ↥(rootsOfUnity n K))
      (ζ ^ i • rootOfSplitsXPowSubC ⋯ a L) =
    ζ ^ i •
      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:
exact smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
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
inst_4 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
⊢ 0 < n

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
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
inst_4 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
hn : 0 < n
rw :
  HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
            (a : Gal(L/K)) → ↥(rootsOfUnity n K))
          ((MulEquiv.symm (autEquivZmod H L hζ) : (a : Multiplicative (ZMod n)) → Gal(L/K))
            ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) (↑m : ZMod n))) :
        ↥(rootsOfUnity n K))
      α =
    ζ ^ m • α
⊢ (((MulEquiv.symm (autEquivZmod H L hζ) : (a : Multiplicative (ZMod n)) → Gal(L/K))
            ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) (↑m : ZMod n)) :
          Gal(L/K)) :
        (a : L) → L)
      α =
    ζ ^ m • α

Tactic:
rw [← autEquivRootsOfUnity_smul ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L hα]

Premises used: Iff.mpr, mem_primitiveRoots, Exists.intro, autEquivRootsOfUnity_smul
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
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
inst_4 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
hn : 0 < n
⊢ HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity ⋯ H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
            (a : Gal(L/K)) → ↥(rootsOfUnity n K))
          ((MulEquiv.symm (autEquivZmod H L hζ) : (a : Multiplicative (ZMod n)) → Gal(L/K))
            ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) (↑m : ZMod n))) :
        ↥(rootsOfUnity n K))
      α =
    ζ ^ m • α

Tactic:
simp [MulEquiv.subgroupCongr_symm_apply, Subgroup.smul_def, Units.smul_def, autEquivZmod]

Premises used: autEquivZmod, Subgroup.smul_def, Units.smul_def, MulEquiv.subgroupCongr_symm_apply
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
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
inst_4 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℕ
⊢ (((MulEquiv.symm (autEquivZmod H L hζ) : (a : Multiplicative (ZMod n)) → Gal(L/K))
            ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) (↑m : ZMod n)) :
          Gal(L/K)) :
        (a : L) → L)
      α =
    ζ ^ m • α

Tactic:
simpa only [Int.cast_natCast, zpow_natCast] using autEquivZmod_symm_apply_intCast H L hα hζ m

Premises used: zpow_natCast, Int.cast_natCast, autEquivZmod_symm_apply_intCast, Nat.cast
-- 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
⊢ IsCyclic.{u_1} Gal(L/K)

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  isCyclic_of_surjective _
    (autEquivZmod H _ <| (mem_primitiveRoots hn).mp hζ.choose_spec).symm.surjective

Premises used: Iff.mpr, isCyclic_of_surjective, Exists.choose_spec, autEquivZmod, ne_zero_of_irreducible_X_pow_sub_C, Nat.pos_iff_ne_zero, MulEquiv.surjective, mem_primitiveRoots, Iff.mp, MulEquiv.symm
-- 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]))
⊢ IsGalois K L

Tactic:
IsGalois.of_separable_splitting_field (separable_X_pow_sub_C_of_irreducible hζ a H)

Premises used: Polynomial.separable_X_pow_sub_C_of_irreducible, IsGalois.of_separable_splitting_field
-- 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]))
⊢ FiniteDimensional K L

Tactic:
have := Polynomial.IsSplittingField.finiteDimensional L (X ^ n - C a)
-- 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]))
this : FiniteDimensional K L
⊢ IsGalois K L

Tactic:
have := isGalois_of_isSplittingField_X_pow_sub_C hζ H L
-- 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]))
this_1 : FiniteDimensional K L
this : IsGalois K L
⊢ 0 < n

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-- 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]))
this_1 : FiniteDimensional K L
this : IsGalois K L
hn : 0 < n
⊢ NeZero n

Tactic:
have : NeZero n := ⟨ne_zero_of_irreducible_X_pow_sub_C H⟩
-- 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]))
this_1 : FiniteDimensional K L
this_2 : IsGalois K L
hn : 0 < n
this : NeZero n
rw : Nat.card.{u_1} Gal(L/K) = n
rw₁ : Nat.card (ZMod n) = n
rw₂ rw₃ : n = n
⊢ Module.finrank K L = n

Tactic:
rw [← IsGalois.card_aut_eq_finrank, Nat.card_congr ((autEquivZmod H L <|
    (mem_primitiveRoots hn).mp hζ.choose_spec).toEquiv.trans Multiplicative.toAdd), Nat.card_zmod]

Premises used: IsGalois.card_aut_eq_finrank, Exists.choose_spec, autEquivZmod, Equiv.trans, MulEquiv.toEquiv, Nat.card_congr, mem_primitiveRoots, Iff.mp, Multiplicative.toAdd, Nat.card_zmod
-- 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)
have :
  ∀ (ζ : K) (hζ : ζ ∈ primitiveRoots (finrank K L) K),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ ∃ (α : L),
    Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) (α ^ finrank K L) ∧
      Eq (α := IntermediateField K L) K⟮α⟯ ⊤

Tactic:
have ⟨ζ, hζ⟩ := hK