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]))
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
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])
⊢ (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 neg : ∀ (h : ¬a = 0),
  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: split_ifs with 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]))
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
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])
have pos : ∀ (hζ : (primitiveRoots 1 K).Nonempty)
  (H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
  [NeZero (R := ℕ) 1] (η : ↥(rootsOfUnity 1 K))
  (this :
    Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X]))))
  (this_3 : IsDomain.{u} K[1√a]),
  Eq (α := K[1√a]) (1 : K[1√a])
    ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        (↑(↑η : Kˣ) : K) :
      K[1√a])
Tactic: obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
Cleared hypotheses: n, hζ, H, inst_1, η, this_1, this_2, this
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u
inst : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero (R := ℕ) 1
__spread.0 : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
η : ↥(rootsOfUnity 1 K)
this_1 :
  Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[1√a]
this : Algebra K K[1√a] := inferInstance
⊢ Eq (α := K[1√a]) (1 : K[1√a])
    ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        (↑(↑η : Kˣ) : K) :
      K[1√a])
have this₁ : (↑η : Kˣ) = 1
Tactic: have : (η : Kˣ) = 1 := (pow_one _).symm.trans η.prop
-- 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
e : K[n√a] ≃ₐ[K] K[n√a]
⊢ OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom (↥(rootsOfUnity n K)) (K[n√a] ≃ₐ[K] K[n√a]))
      (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e) =
    e
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 (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
e : 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 : Algebra K K[n√a] := inferInstance
⊢ OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
      (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e) =
    e
have a₁ : (↑(OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
        (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) :
    K[n√a] →ₐ[K] K[n√a]) =
  (↑e : K[n√a] →ₐ[K] K[n√a])
Tactic: apply AlgEquiv.coe_algHom_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
e : 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 : Algebra K K[n√a] := inferInstance
⊢ (↑(OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
          (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) :
      K[n√a] →ₐ[K] K[n√a]) =
    (↑e : K[n√a] →ₐ[K] K[n√a])
have a₁ : Eq (α := K[n√a])
  (((↑(OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
              (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) :
          K[n√a] →ₐ[K] 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])
  (((↑e : K[n√a] →ₐ[K] 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])
Tactic: apply AdjoinRoot.algHom_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
e : 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 : Algebra K K[n√a] := inferInstance
⊢ Eq (α := K[n√a])
    (((↑(OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
                (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) :
            K[n√a] →ₐ[K] 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])
    (((↑e : K[n√a] →ₐ[K] 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])
have 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])
      (↑(↑((MulEquiv.symm
                    (rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f :=
                      of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) sorry
                      hζ) :
                  (a : ↥(rootsOfUnity n K[n√a])) → ↥(rootsOfUnity n K))
                (rootsOfUnity.mkOfPowEq
                  (if a = 0 then 1
                  else
                    HDiv.hDiv (α := K[n√a])
                      ((e : (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]))))
                  sorry)) :
            Kˣ) :
        K) *
    root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
  (e : (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])))
Tactic: simp only [AdjoinRootXPowSubCEquivToRootsOfUnity, AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe,
      MonoidHom.toOneHom_coe, AlgEquiv.coe_algHom, autAdjoinRootXPowSubC_root, Algebra.smul_def]
-- 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
e : 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 : Algebra K K[n√a] := inferInstance
⊢ (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])
        (↑(↑((MulEquiv.symm
                      (rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f :=
                        of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ⋯
                        hζ) :
                    (a : ↥(rootsOfUnity n K[n√a])) → ↥(rootsOfUnity n K))
                  (rootsOfUnity.mkOfPowEq
                    (if a = 0 then 1
                    else
                      HDiv.hDiv (α := K[n√a])
                        ((e : (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]))))
                    ⋯)) :
              Kˣ) :
          K) *
      root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (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])))
have a₁ : (if a = 0 then 1
    else
      HDiv.hDiv (α := K[n√a])
        ((e : (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])))) *
    root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
  (e : (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])))
Tactic: rw [rootsOfUnityEquivOfPrimitiveRoots_symm_apply, rootsOfUnity.val_mkOfPowEq_coe]
-- 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
e : 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 : Algebra K K[n√a] := inferInstance
⊢ (if a = 0 then 1
      else
        HDiv.hDiv (α := K[n√a])
          ((e : (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])))) *
      root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (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])))
have pos : ∀ (h : a = 0),
  1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (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])))
Tactic: split_ifs with 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]))
inst_1 : NeZero n
e : 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 : Algebra K K[n√a] := inferInstance
pos :
  ∀ (h : a = 0),
    1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
      (e : (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])))
⊢ (if a = 0 then 1
      else
        HDiv.hDiv (α := K[n√a])
          ((e : (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])))) *
      root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (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])))
have neg : ∀ (h : ¬a = 0),
  HDiv.hDiv (α := K[n√a])
        ((e : (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]))) *
      root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (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])))
Tactic: split_ifs with 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]))
inst_1 : NeZero n
e : 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 : Algebra K K[n√a] := inferInstance
h : a = 0
⊢ 1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (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])))
have pos : ∀ (hζ : (primitiveRoots 1 K).Nonempty)
  (H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
  [NeZero (R := ℕ) 1] (e : K[1√a] ≃ₐ[K] K[1√a])
  (this :
    Fact
      (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))),
  1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (a_1 : K[1√a]) → K[1√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
Tactic: obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
Cleared hypotheses: n, hζ, H, inst_1, e, this_1, this
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero (R := ℕ) 1
__spread.0 : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
e : Gal(K[1√a]/K)
this_1 :
  Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[1√a] := inferInstance
⊢ 1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (a_1 : K[1√a]) → K[1√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
have pos : HMul.hMul (α := K[1√a]) (β := K[1√a]) (1 : K[1√a])
    ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        a :
      K[1√a]) =
  (e : (a_1 : K[1√a]) → K[1√a])
    ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
        (a_1 : K) → K[1√a])
      a)
Tactic: rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul,
        ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero (R := ℕ) 1
__spread.0 : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
e : Gal(K[1√a]/K)
this_1 :
  Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[1√a] := inferInstance
pos :
  HMul.hMul (α := K[1√a]) (β := K[1√a]) (1 : K[1√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
            (a_1 : K) → K[1√a])
          a :
        K[1√a]) =
    (e : (a_1 : K[1√a]) → K[1√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        a)
⊢ 1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (a_1 : K[1√a]) → K[1√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
have pos₁ : Eq (α := K[1√a])
  ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
        (a_1 : K) → K[1√a])
      a :
    K[1√a])
  ((e : (a_1 : K[1√a]) → K[1√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        a) :
    K[1√a])
Tactic: rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul,
        ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero (R := ℕ) 1
__spread.0 : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
e : Gal(K[1√a]/K)
this_1 :
  Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[1√a] := inferInstance
pos :
  HMul.hMul (α := K[1√a]) (β := K[1√a]) (1 : K[1√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
            (a_1 : K) → K[1√a])
          a :
        K[1√a]) =
    (e : (a_1 : K[1√a]) → K[1√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        a)
pos₁ :
  Eq (α := K[1√a])
    ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        a :
      K[1√a])
    ((e : (a_1 : K[1√a]) → K[1√a])
        ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
            (a_1 : K) → K[1√a])
          a) :
      K[1√a])
⊢ 1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (a_1 : K[1√a]) → K[1√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
have pos₂ : Eq (α := K[1√a]) ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a : K[1√a])
  ((e : (a_1 : K[1√a]) → K[1√a]) ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a) : K[1√a])
Tactic: rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul,
        ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero (R := ℕ) 1
__spread.0 : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
e : Gal(K[1√a]/K)
this_1 :
  Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[1√a] := inferInstance
pos :
  HMul.hMul (α := K[1√a]) (β := K[1√a]) (1 : K[1√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
            (a_1 : K) → K[1√a])
          a :
        K[1√a]) =
    (e : (a_1 : K[1√a]) → K[1√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        a)
pos₁ :
  Eq (α := K[1√a])
    ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        a :
      K[1√a])
    ((e : (a_1 : K[1√a]) → K[1√a])
        ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
            (a_1 : K) → K[1√a])
          a) :
      K[1√a])
pos₂ :
  Eq (α := K[1√a]) ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a : K[1√a])
    ((e : (a_1 : K[1√a]) → K[1√a]) ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a) : K[1√a])
⊢ 1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (a_1 : K[1√a]) → K[1√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
have pos₃ : Eq (α := K[1√a]) ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a : K[1√a])
  ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a : K[1√a])
Tactic: rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul,
        ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
-- 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
σ : K[n√a] ≃ₐ[K] K[n√a]
⊢ HSMul.hSMul (α := Kˣ)
      (↑(((autAdjoinRootXPowSubCEquiv hζ H).symm : (a : K[n√a] ≃ₐ[K] K[n√a]) → ↥(rootsOfUnity n K)) σ) : Kˣ)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    (σ : (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])))
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