-- 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
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 : ℕ), (σ.toLinearMap ^ n) v = ζ ^ n • v
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
simp_rw [← AlgEquiv.pow_toLinearMap, AlgEquiv.toLinearMap_apply] at hv'

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
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • 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
⊢ σ ^ (finrank K L * k) ∈ ⊤

Tactic:
rw [pow_mul, ← IsGalois.card_aut_eq_finrank, pow_card_eq_one, one_pow]

Result:
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 ∈ ⊤

Proof state:
case mk.intro.intro.refine_2.a
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
⊢ ⊤ ≤ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯

Tactic:
intros σ' hσ'

Result:
case mk.intro.intro.refine_2.a
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
σ' : L ≃ₐ[K] L
hσ' : σ' ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
⊢ σ' ∈ ⊤

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)
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
have : IsRoot (minpoly K σ.toLinearMap) ζ := by
  simpa [minpoly_algEquiv_toLinearMap σ (isOfFinOrder_of_finite σ), hσ',
    sub_eq_zero, IsGalois.card_aut_eq_finrank] using hζ.pow_eq_one

Result:
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⟮α⟯ = ⊤

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
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
have hσ' := orderOf_eq_card_of_forall_mem_zpowers hσ

Result:
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)
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Proof state:
case mk.intro.intro.refine_1
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
σ' : L ≃ₐ[K] L
hσ' : σ' ∈ ⊥
⊢ ⟨σ', hσ'⟩ • v ^ finrank K L = v ^ finrank K L

Tactic:
obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')

Result:
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