-- 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_2
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⟮v⟯ = ⊤

Tactic:
apply IsGalois.intermediateFieldEquivSubgroup.injective

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
⊢ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯ = IsGalois.intermediateFieldEquivSubgroup ⊤

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
⊢ v ^ finrank K L ∈ Set.range ⇑(algebraMap K L)

Tactic:
rw [← IntermediateField.mem_bot,
  ← OrderIso.map_bot IsGalois.intermediateFieldEquivSubgroup.symm]

Result:
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
⊢ v ^ finrank K L ∈ IsGalois.intermediateFieldEquivSubgroup.symm ⊥

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 = 1 • v
⊢ σ ^ n ∈ ⊤

Tactic:
obtain ⟨k, rfl⟩ := hζ.dvd_of_pow_eq_one n (smul_left_injective K hv.2 this)

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
⊢ σ ^ (finrank K L * k) ∈ ⊤

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:
simp only [AlgEquiv.smul_def, hv'] at this

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 = v
⊢ σ ^ n ∈ ⊤

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

Tactic:
have hv' := hv.pow_apply

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

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⟯ = IsGalois.intermediateFieldEquivSubgroup ⊤

Tactic:
rw [map_top, eq_top_iff]

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
⊢ ⊤ ≤ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯