awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L : (a : K) → L) a
have 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])))
      sorry sorry)
    (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])
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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)
⊢ (σ : (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)
have obtain : ∀ (η : ↥(rootsOfUnity n K)),
  (((MulEquiv.symm (autEquivRootsOfUnity hζ H L) : (a : ↥(rootsOfUnity n K)) → Gal(L/K)) η : Gal(L/K)) : (a : L) → L)
      (rootOfSplitsXPowSubC sorry 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 sorry a L)
Tactic: obtain ⟨η, rfl⟩ := (autEquivRootsOfUnity hζ H L).symm.surjective σ
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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)
⊢ (((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)
have rw : (((MulEquiv.symm
              (MulEquiv.trans
                (AlgEquiv.autCongr
                  (AlgEquiv.symm (adjoinRootXPowSubCEquiv (α := rootOfSplitsXPowSubC (n := n) sorry a L) hζ H sorry)))
                (autAdjoinRootXPowSubCEquiv hζ H).symm) :
            (a : ↥(rootsOfUnity n K)) → Gal(L/K))
          η :
        Gal(L/K)) :
      (a : L) → L)
    (rootOfSplitsXPowSubC sorry a L) =
  η • rootOfSplitsXPowSubC sorry a L
Tactic: rw [MulEquiv.apply_symm_apply, autEquivRootsOfUnity]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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)
⊢ (((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
have simp : (↑(↑η : Kˣ) : K) • rootOfSplitsXPowSubC (n := n) sorry a L = η • rootOfSplitsXPowSubC sorry 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]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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)
⊢ 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) α
have have : ∀ (ζ : K) (hζ' : ζ ∈ primitiveRoots n K),
  HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity sorry 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ζ
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ 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) α
have hn : 0 < n
Tactic: have hn := NeZero.pos n
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ 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) α
have hζ'₁ : IsPrimitiveRoot ζ n
Tactic: rw [mem_primitiveRoots hn] at hζ'
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ 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) α
have 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 sorry 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 sorry 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α
Cleared hypotheses: hα, inst_4, σ, ζ, hζ'_1, hζ', hn
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ 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) α
have hα₁ : ∃ a_1 < n, HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) a_1 * rootOfSplitsXPowSubC sorry a L = α
Tactic: simp only [Multiset.mem_map, Multiset.mem_range] at hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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 = α
⊢ 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) α
have obtain : ∀ i < n,
  HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
      (((autEquivRootsOfUnity sorry 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 sorry a L) =
    (σ : (a : L) → L)
      (HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) ζ : L) i * rootOfSplitsXPowSubC sorry a L)
Tactic: obtain ⟨i, _, rfl⟩ := hα
Cleared hypotheses: α, hα
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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))
      (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)
have simp : HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
    (((autEquivRootsOfUnity sorry H L : MulEquiv.{u_1, u} Gal(L/K) ↥(rootsOfUnity n K)) :
          (a : Gal(L/K)) → ↥(rootsOfUnity n K))
        σ :
      ↥(rootsOfUnity n K))
    (ζ ^ i • rootOfSplitsXPowSubC sorry 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 sorry a L)
Tactic: simp only [← map_pow, ← Algebra.smul_def, map_smul,
    autEquivRootsOfUnity_apply_rootOfSplit hζ H L]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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 • α
have hn : 0 < n
Tactic: have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ (((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 • α
have rw : HSMul.hSMul.{u, u_1, u_1} (α := ↥(rootsOfUnity n K))
    (((autEquivRootsOfUnity sorry 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: rw [← autEquivRootsOfUnity_smul ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L hα]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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]))
⊢ Module.finrank K L = n
have this : FiniteDimensional K L
Tactic: have := Polynomial.IsSplittingField.finiteDimensional L (X ^ n - C a)
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ Module.finrank K L = n
have this₁ : IsGalois K L
Tactic: have := isGalois_of_isSplittingField_X_pow_sub_C hζ H L
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ Module.finrank K L = n
have hn : 0 < n
Tactic: have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ Module.finrank K L = n
have this₁ : NeZero n
Tactic: have : NeZero n := ⟨ne_zero_of_irreducible_X_pow_sub_C H⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ Module.finrank K L = n
have rw : Nat.card.{u_1} Gal(L/K) = 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]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ Module.finrank K L = n
have rw₁ : Nat.card (ZMod n) = 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]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ Module.finrank K L = n
have rw₂ : n = 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]
-- 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
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(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⟮α⟯ ⊤
have 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⟮α⟯ ⊤
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
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : 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⟮α⟯ ⊤
have hζ₁ : IsPrimitiveRoot ζ (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
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
⊢ ∃ (α : 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⟮α⟯ ⊤
have obtain : ∀ (σ : Gal(L/K)) (hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x),
  ∃ (α : 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: obtain ⟨σ, hσ⟩ := ‹IsCyclic Gal(L/K)›
-- 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
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
⊢ ∃ (α : 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⟮α⟯ ⊤
have hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
Tactic: have hσ' := orderOf_eq_card_of_forall_mem_zpowers hσ
-- 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
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σ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
⊢ IsRoot (minpoly K σ.toLinearMap) ζ
have hσ'₁ : orderOf σ = finrank K L
Tactic: rw [IsGalois.card_aut_eq_finrank] at hσ'
Cleared hypotheses: hσ'