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]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : Algebra K K[n√a] := inferInstance
this : n ≠ 0
adjoin_rootSet' :
  Membership.mem (γ := Set K[n√a])
    ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).rootSet K[n√a])
    (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
adjoin_rootSet'₁ :
  Eq (α := K[n√a])
    ((aeval (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
        (a_1 : K [X]) → K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
    0
adjoin_rootSet'₂ :
  eval₂ (algebraMap K K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    0
adjoin_rootSet'₃ :
  eval₂ (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    0
⊢ Subset (α := Set K[n√a])
    {root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))}
    ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).rootSet K[n√a])
have adjoin_rootSet'₄ : Eq.{u + 1} (α := K[n√a]) 0 0
Tactic: rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero
      (Nat.pos_of_ne_zero this) a), aeval_def, AdjoinRoot.algebraMap_eq, AdjoinRoot.eval₂_root]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
⊢ Function.Bijective.{u + 1, u_1 + 1} (α := K[n√a]) (β := L)
    (⇑(liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K L) α ⋯) :
      (a : K[n√a]) → L)
have this : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
Tactic: haveI := Fact.mk H
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : IsSplittingField K K[n√a]
  (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :=
  ⋯
⊢ Function.Bijective.{u + 1, u_1 + 1} (α := K[n√a]) (β := L)
    (⇑(liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K L) α ⋯) :
      (a : K[n√a]) → L)
have refine : Function.Surjective.{u + 1, u_1 + 1} (α := K[n√a]) (β := L)
  (⇑(liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
        (Algebra.ofId K L) α sorry) :
    (a : K[n√a]) → L)
Tactic: refine ⟨(liftAlgHom (X ^ n - C a) _ α _).injective, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H_1 : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα_1 : α ^ n = (algebraMap K L : (a : K) → L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
hα : α ^ n = (algebraMap K L : (a : K) → L) a
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : IsSplittingField K K[n√a]
  (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :=
  ⋯
⊢ Function.Surjective.{u + 1, u_1 + 1} (α := K[n√a]) (β := L)
    (⇑(liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K L) α ⋯) :
      (a : K[n√a]) → L)
have hf : Splits (R := K[n√a])
  (Polynomial.map (algebraMap K K[n√a])
    (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
Tactic: rw [← AlgHom.range_eq_top, ← IsSplittingField.adjoin_rootSet _ (X ^ n - C a),
      eq_comm, Splits.adjoin_rootSet_eq_range, IsSplittingField.adjoin_rootSet]
-- 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
⊢ (adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    α
have rw : (AlgEquiv.ofBijective
        (liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K L) α sorry)
        sorry :
      (a : K[n√a]) → L)
    (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
  α
Tactic: rw [adjoinRootXPowSubCEquiv, AlgEquiv.coe_ofBijective, liftAlgHom_root]
-- 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
rw :
  (AlgEquiv.ofBijective
          (liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
            (Algebra.ofId K L) α ⋯)
          ⋯ :
        (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    α
⊢ (adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    α
have rw₁ : (liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) (Algebra.ofId K L) α
        sorry :
      (a : K[n√a]) → L)
    (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
  α
Tactic: rw [adjoinRootXPowSubCEquiv, AlgEquiv.coe_ofBijective, liftAlgHom_root]
-- 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
rw :
  (AlgEquiv.ofBijective
          (liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
            (Algebra.ofId K L) α ⋯)
          ⋯ :
        (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    α
rw₁ :
  (liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) (Algebra.ofId K L)
          α ⋯ :
        (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    α
⊢ (adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    α
have rw₂ : α = α
Tactic: rw [adjoinRootXPowSubCEquiv, AlgEquiv.coe_ofBijective, liftAlgHom_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
⊢ ((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α =
    root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
have a₁ : Eq.{u_1 + 1} (α := L)
  ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
      (((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α : K[n√a]) :
    L)
  ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
    L)
Tactic: apply (adjoinRootXPowSubCEquiv hζ H 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]))
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsSplittingField K L (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
α : L
hα : α ^ n = (algebraMap K L : (a : K) → L) a
⊢ Eq.{u_1 + 1} (α := L)
    ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
        (((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α : K[n√a]) :
      L)
    ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
      L)
have a₁ : α =
  (adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
    (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
Tactic: rw [(adjoinRootXPowSubCEquiv hζ H hα).apply_symm_apply, 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
a₁ :
  α =
    (adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
⊢ Eq.{u_1 + 1} (α := L)
    ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
        (((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α : K[n√a]) :
      L)
    ((adjoinRootXPowSubCEquiv hζ H hα : (a : K[n√a]) → L)
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
      L)
have a₂ : α = α
Tactic: rw [(adjoinRootXPowSubCEquiv hζ H hα).apply_symm_apply, 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
⊢ Eq (α := Subalgebra K L) K [α] ⊤
have a₁ : Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
  Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤
Tactic: apply Subalgebra.map_injective (B := K[n√a]) (f := (adjoinRootXPowSubCEquiv hζ H hα).symm)
    (adjoinRootXPowSubCEquiv hζ H hα).symm.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]))
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
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤
have a₁ : Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
  (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]).range
Tactic: rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
    (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgEquiv.coe_algHom, adjoinRootXPowSubCEquiv_symm_eq_root,
      adjoinRoot_eq_top]
-- 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
a₁ :
  Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]).range
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤
have a₂ : Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] = ⊤
Tactic: rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
    (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgEquiv.coe_algHom, adjoinRootXPowSubCEquiv_symm_eq_root,
      adjoinRoot_eq_top]
-- 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
a₁ :
  Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]).range
a₂ : Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] = ⊤
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤
have a₃ : Eq (α := Subalgebra K K[n√a])
  (adjoin K (Set.image (α := L) (⇑(↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) {α}))
  ⊤
Tactic: rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
    (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgEquiv.coe_algHom, adjoinRootXPowSubCEquiv_symm_eq_root,
      adjoinRoot_eq_top]
-- 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
a₁ :
  Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]).range
a₂ : Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] = ⊤
a₃ :
  Eq (α := Subalgebra K K[n√a])
    (adjoin K
      (Set.image (α := L) (⇑(↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) {α}))
    ⊤
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤
have a₄ : Eq (α := Subalgebra K K[n√a])
  K [(((↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) α : K[n√a])] ⊤
Tactic: rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
    (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgEquiv.coe_algHom, adjoinRootXPowSubCEquiv_symm_eq_root,
      adjoinRoot_eq_top]
-- 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
a₁ :
  Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]).range
a₂ : Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] = ⊤
a₃ :
  Eq (α := Subalgebra K K[n√a])
    (adjoin K
      (Set.image (α := L) (⇑(↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) {α}))
    ⊤
a₄ :
  Eq (α := Subalgebra K K[n√a])
    K [(((↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) α : K[n√a])] ⊤
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤
have a₅ : Eq (α := Subalgebra K K[n√a]) K [(((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α : K[n√a])] ⊤
Tactic: rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
    (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgEquiv.coe_algHom, adjoinRootXPowSubCEquiv_symm_eq_root,
      adjoinRoot_eq_top]
-- 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
a₁ :
  Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]).range
a₂ : Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] = ⊤
a₃ :
  Eq (α := Subalgebra K K[n√a])
    (adjoin K
      (Set.image (α := L) (⇑(↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) {α}))
    ⊤
a₄ :
  Eq (α := Subalgebra K K[n√a])
    K [(((↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) α : K[n√a])] ⊤
a₅ : Eq (α := Subalgebra K K[n√a]) K [(((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α : K[n√a])] ⊤
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤
have a₆ : Eq (α := Subalgebra K K[n√a])
  K [root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))] ⊤
Tactic: rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
    (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgEquiv.coe_algHom, adjoinRootXPowSubCEquiv_symm_eq_root,
      adjoinRoot_eq_top]
-- 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
a₁ :
  Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]).range
a₂ : Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] = ⊤
a₃ :
  Eq (α := Subalgebra K K[n√a])
    (adjoin K
      (Set.image (α := L) (⇑(↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) {α}))
    ⊤
a₄ :
  Eq (α := Subalgebra K K[n√a])
    K [(((↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) : (a_1 : L) → K[n√a]) α : K[n√a])] ⊤
a₅ : Eq (α := Subalgebra K K[n√a]) K [(((adjoinRootXPowSubCEquiv hζ H hα).symm : (a_1 : L) → K[n√a]) α : K[n√a])] ⊤
a₆ :
  Eq (α := Subalgebra K K[n√a])
    K [root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))] ⊤
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) K [α] =
    Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm : L →ₐ[K] K[n√a]) ⊤
have a₇ : Eq.{u + 1} (α := Subalgebra K K[n√a]) ⊤ ⊤
Tactic: rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
    (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgEquiv.coe_algHom, adjoinRootXPowSubCEquiv_symm_eq_root,
      adjoinRoot_eq_top]
-- 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
⊢ Eq (α := IntermediateField K L) K⟮α⟯ ⊤
have refine : Eq (α := Subalgebra K L) (toSubalgebra ⊤) K [α]
Tactic: refine (IntermediateField.eq_adjoin_of_eq_algebra_adjoin _ _ _ ?_).symm