awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]))
η : ↥(rootsOfUnity n K)
this : (↑(↑η : Kˣ) : K) ^ n = 1
rw :
  HSub.hSub (α := K[n√a]) (β := K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          (HPow.hPow (α := K [X]) X n) :
        K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
rw₁ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a])
        ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          X)
        n)
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
⊢ Eq (α := K[n√a])
    ((aeval
          ((↑(↑η : Kˣ) : K) •
            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
have rw₂ : HSub.hSub (β := K[n√a])
    (HPow.hPow (α := K[n√a])
      ((aeval
            ((↑(↑η : Kˣ) : K) •
              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])
        X)
      n)
    ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
  0
Tactic: rw [map_sub, map_pow, aeval_C, aeval_X, Algebra.smul_def, mul_pow, root_X_pow_sub_C_pow,
      AdjoinRoot.algebraMap_eq, ← map_pow, this, map_one, one_mul, sub_self]
-- 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]))
η : ↥(rootsOfUnity n K)
this : (↑(↑η : Kˣ) : K) ^ n = 1
rw :
  HSub.hSub (α := K[n√a]) (β := K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          (HPow.hPow (α := K [X]) X n) :
        K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
rw₁ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a])
        ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          X)
        n)
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
rw₂ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a])
        ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          X)
        n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
⊢ Eq (α := K[n√a])
    ((aeval
          ((↑(↑η : Kˣ) : K) •
            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
have rw₃ : HSub.hSub (β := K[n√a])
    (((↑(↑η : Kˣ) : K) • root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ^
      n)
    ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
  0
Tactic: rw [map_sub, map_pow, aeval_C, aeval_X, Algebra.smul_def, mul_pow, root_X_pow_sub_C_pow,
      AdjoinRoot.algebraMap_eq, ← map_pow, this, map_one, one_mul, sub_self]
-- 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]))
η : ↥(rootsOfUnity n K)
this : (↑(↑η : Kˣ) : K) ^ n = 1
rw :
  HSub.hSub (α := K[n√a]) (β := K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          (HPow.hPow (α := K [X]) X n) :
        K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
rw₁ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a])
        ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          X)
        n)
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
rw₂ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a])
        ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          X)
        n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
rw₃ :
  HSub.hSub (β := K[n√a])
      (((↑(↑η : Kˣ) : K) •
          root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ^
        n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
⊢ Eq (α := K[n√a])
    ((aeval
          ((↑(↑η : Kˣ) : K) •
            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
have rw₄ : HSub.hSub (β := K[n√a])
    (HMul.hMul (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) (↑(↑η : Kˣ) : K) : K[n√a])
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ^
      n)
    ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
  0
Tactic: rw [map_sub, map_pow, aeval_C, aeval_X, Algebra.smul_def, mul_pow, root_X_pow_sub_C_pow,
      AdjoinRoot.algebraMap_eq, ← map_pow, this, map_one, one_mul, sub_self]
-- 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]))
η : ↥(rootsOfUnity n K)
this : (↑(↑η : Kˣ) : K) ^ n = 1
rw :
  HSub.hSub (α := K[n√a]) (β := K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          (HPow.hPow (α := K [X]) X n) :
        K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
rw₁ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a])
        ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          X)
        n)
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
rw₂ :
  HSub.hSub (β := K[n√a])
      (HPow.hPow (α := K[n√a])
        ((aeval
              ((↑(↑η : Kˣ) : K) •
                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])
          X)
        n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
rw₃ :
  HSub.hSub (β := K[n√a])
      (((↑(↑η : Kˣ) : K) •
          root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ^
        n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
rw₄ :
  HSub.hSub (β := K[n√a])
      (HMul.hMul (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) (↑(↑η : Kˣ) : K) : K[n√a])
          (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ^
        n)
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    0
⊢ Eq (α := K[n√a])
    ((aeval
          ((↑(↑η : Kˣ) : K) •
            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
have rw₅ : HSub.hSub (β := K[n√a])
    (HPow.hPow (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) (↑(↑η : Kˣ) : K) : K[n√a]) n *
      root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) ^ n)
    ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
  0
Tactic: rw [map_sub, map_pow, aeval_C, aeval_X, Algebra.smul_def, mul_pow, root_X_pow_sub_C_pow,
      AdjoinRoot.algebraMap_eq, ← map_pow, this, map_one, one_mul, sub_self]
-- 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]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) := ⋯
this_2 : IsDomain.{u} K[n√a] := ⋯
this : DecidableEq K := Classical.decEq K
⊢ (if a = 0 then 1
      else
        HDiv.hDiv (α := K[n√a])
          ((σ : (a_1 : K[n√a]) → K[n√a])
              (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            K[n√a])
          (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))) ^
      n =
    1
have isTrue : a = 0 → HPow.hPow (α := K[n√a]) 1 n = 1
Tactic: split
-- 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]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) := ⋯
this_2 : IsDomain.{u} K[n√a] := ⋯
this : DecidableEq K := Classical.decEq K
isTrue : a = 0 → HPow.hPow (α := K[n√a]) 1 n = 1
⊢ (if a = 0 then 1
      else
        HDiv.hDiv (α := K[n√a])
          ((σ : (a_1 : K[n√a]) → K[n√a])
              (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            K[n√a])
          (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))) ^
      n =
    1
have isFalse : ¬a = 0 →
  HDiv.hDiv (α := K[n√a])
        ((σ : (a_1 : K[n√a]) → K[n√a])
            (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
          K[n√a])
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ^
      n =
    1
Tactic: split
-- 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]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) := ⋯
this_2 : IsDomain.{u} K[n√a] := ⋯
this : DecidableEq K := Classical.decEq K
h : ¬a = 0
⊢ HDiv.hDiv (α := K[n√a])
        ((σ : (a_1 : K[n√a]) → K[n√a])
            (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
          K[n√a])
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ^
      n =
    1
have isFalse : HDiv.hDiv (α := K[n√a])
    ((σ : (a_1 : K[n√a]) → K[n√a])
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) ^ n) :
      K[n√a])
    (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) ^ n) =
  1
Tactic: rw [div_pow, ← map_pow]
-- 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]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) := ⋯
this_2 : IsDomain.{u} K[n√a] := ⋯
this : DecidableEq K := Classical.decEq K
h : ¬a = 0
⊢ HDiv.hDiv (α := K[n√a])
      ((σ : (a_1 : K[n√a]) → K[n√a])
          (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) ^ n) :
        K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) ^ n) =
    1
have isFalse : HDiv.hDiv (α := K[n√a]) (β := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a])
    ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
  1
Tactic: simp only [root_X_pow_sub_C_pow, ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
-- 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]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) := ⋯
this_2 : IsDomain.{u} K[n√a] := ⋯
this : DecidableEq K := Classical.decEq K
h : ¬a = 0
⊢ HDiv.hDiv (α := K[n√a]) (β := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a])
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    1
have isFalse : Ne (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) (0 : K[n√a])
Tactic: rw [div_self]
-- 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]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) := ⋯
this_2 : IsDomain.{u} K[n√a] := ⋯
this : DecidableEq K := Classical.decEq K
h : ¬a = 0
⊢ Ne (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) (0 : K[n√a])
have isFalse : ¬Eq (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) (0 : K[n√a])
Tactic: rwa [Ne, map_eq_zero_iff _ (algebraMap K _).injective]
-- 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]))
inst_1 : NeZero n
η : ↥(rootsOfUnity n K)
⊢ AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
      (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom (↥(rootsOfUnity n K)) (K[n√a] ≃ₐ[K] K[n√a])) η) =
    η
have this : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
Tactic: have := Fact.mk 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]))
inst_1 : NeZero n
η : ↥(rootsOfUnity n K)
this : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
⊢ AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
      (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η) =
    η
have this₁ : IsDomain.{u} K[n√a]
Tactic: have : IsDomain K[n√a] := inferInstance
-- 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]))
inst_1 : NeZero n
η : ↥(rootsOfUnity n K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
⊢ AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
      (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η) =
    η
have a₁ : Eq (α := ↥(rootsOfUnity n K[n√a]))
  ((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) sorry hζ :
        (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
      (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
        (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η)) :
    ↥(rootsOfUnity n K[n√a]))
  ((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) sorry hζ :
        (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
      η :
    ↥(rootsOfUnity n K[n√a]))
Tactic: apply (rootsOfUnityEquivOfPrimitiveRoots (algebraMap K K[n√a]).injective hζ).injective
-- 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]))
inst_1 : NeZero n
η : ↥(rootsOfUnity n K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
⊢ Eq (α := ↥(rootsOfUnity n K[n√a]))
    ((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
          (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
        (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
          (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η)) :
      ↥(rootsOfUnity n K[n√a]))
    ((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
          (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
        η :
      ↥(rootsOfUnity n K[n√a]))
have a₁ : Eq.{u + 1} (α := K[n√a])
  (↑(↑((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) sorry hζ :
              (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
            (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
              (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η))) :
        K[n√a]ˣ) :
    K[n√a])
  (↑(↑((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) sorry hζ :
              (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
            η) :
        K[n√a]ˣ) :
    K[n√a])
Tactic: ext
-- 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]))
inst_1 : NeZero n
η : ↥(rootsOfUnity n K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
⊢ Eq.{u + 1} (α := K[n√a])
    (↑(↑((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
                (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
              (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
                (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η))) :
          K[n√a]ˣ) :
      K[n√a])
    (↑(↑((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
                (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
              η) :
          K[n√a]ˣ) :
      K[n√a])
have a₁ : (if a = 0 then 1
  else
    HMul.hMul (α := K[n√a])
        ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :
              (a_1 : K) → K[n√a])
            (↑(↑η : Kˣ) : K) :
          K[n√a])
        (root (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]))) =
  (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
    (↑(↑η : Kˣ) : K)
Tactic: simp only [AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
      autAdjoinRootXPowSubC_root, Algebra.smul_def, MulEquiv.apply_symm_apply,
      rootsOfUnity.val_mkOfPowEq_coe, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe,
      AdjoinRootXPowSubCEquivToRootsOfUnity]
-- 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]))
inst_1 : NeZero n
η : ↥(rootsOfUnity n K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
⊢ (if a = 0 then 1
    else
      HMul.hMul (α := K[n√a])
          ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :
                (a_1 : K) → K[n√a])
              (↑(↑η : Kˣ) : K) :
            K[n√a])
          (root (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]))) =
    (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
      (↑(↑η : Kˣ) : K)
have pos : ∀ (h : a = 0),
  Eq (α := K[n√a]) (1 : K[n√a])
    ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
        (↑(↑η : Kˣ) : K) :
      K[n√a])
Tactic: split_ifs with h