-- Mathlib/FieldTheory/KummerExtension.lean
/-- If `L/K` is a cyclic extension of degree `n`, and `K` contains all `n`-th roots of unity,
then `L = K[α]` for some `α ^ n ∈ K`. -/
lemma exists_root_adjoin_eq_top_of_isCyclic [IsGalois K L] [IsCyclic (L ≃ₐ[K] L)] :
    ∃ (α : L), α ^ (finrank K L) ∈ Set.range (algebraMap K L) ∧ K⟮α⟯ = ⊤

Proof state:
case mk.intro.intro.refine_1.intro
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic (L ≃ₐ[K] L)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : L ≃ₐ[K] L
hσ : Function.Surjective fun x => σ ^ x
hσ'✝ : orderOf σ = Nat.card (L ≃ₐ[K] L)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ ⊥
⊢ ⟨σ ^ n, hσ'⟩ • v ^ finrank K L = v ^ finrank K L

Tactic:
rw [smul_pow', Submonoid.smul_def, AlgEquiv.smul_def, hv', smul_pow, ← pow_mul,
  mul_comm, pow_mul, hζ.pow_eq_one, one_pow, one_smul]

Result:
no goals

Proof state:
case mk.intro
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic (L ≃ₐ[K] L)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : L ≃ₐ[K] L
hσ : Function.Surjective fun x => σ ^ x
hσ' : orderOf σ = Nat.card (L ≃ₐ[K] L)
this : (minpoly K σ.toLinearMap).IsRoot ζ
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
obtain ⟨v, hv⟩ := (Module.End.hasEigenvalue_of_isRoot this).exists_hasEigenvector

Result:
case mk.intro.intro
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic (L ≃ₐ[K] L)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : L ≃ₐ[K] L
hσ : Function.Surjective fun x => σ ^ x
hσ' : orderOf σ = Nat.card (L ≃ₐ[K] L)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Proof state:
case mk.intro.intro.refine_2.a.intro.intro
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic (L ≃ₐ[K] L)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : L ≃ₐ[K] L
hσ : Function.Surjective fun x => σ ^ x
hσ'✝ : orderOf σ = Nat.card (L ≃ₐ[K] L)
this✝ : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
k : ℕ
hσ' : σ ^ (finrank K L * k) ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
this : ζ ^ (finrank K L * k) • v = 1 • v
⊢ 1 ∈ ⊤

Tactic:
exact one_mem _

Result:
no goals

Proof state:
case mk.intro.intro.refine_2.a.intro
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic (L ≃ₐ[K] L)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : L ≃ₐ[K] L
hσ : Function.Surjective fun x => σ ^ x
hσ'✝ : orderOf σ = Nat.card (L ≃ₐ[K] L)
this✝ : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
this : ζ ^ n • v = v
⊢ σ ^ n ∈ ⊤

Tactic:
conv_rhs at this => rw [← one_smul K v]

Result:
case mk.intro.intro.refine_2.a.intro
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic (L ≃ₐ[K] L)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : L ≃ₐ[K] L
hσ : Function.Surjective fun x => σ ^ x
hσ'✝ : orderOf σ = Nat.card (L ≃ₐ[K] L)
this✝ : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
this : ζ ^ n • v = 1 • v
⊢ σ ^ n ∈ ⊤

Proof state:
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic (L ≃ₐ[K] L)
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

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

Result:
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic (L ≃ₐ[K] L)
ζ : K
hζ : ζ ∈ primitiveRoots (finrank K L) K
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤