-- 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
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 ⊥

Tactic:
intro ⟨σ', hσ'⟩

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

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

Tactic:
refine ⟨v, ?_, ?_⟩

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

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⟯ = ⊤

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

Tactic:
rw [mem_primitiveRoots finrank_pos] at hζ

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ζ : IsPrimitiveRoot ζ (finrank K L)
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap 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⟯
⊢ σ ^ n ∈ ⊤

Tactic:
have := hσ' ⟨v, IntermediateField.mem_adjoin_simple_self 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, ⋯⟩ = ↑⟨v, ⋯⟩
⊢ σ ^ n ∈ ⊤

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

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

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⟯
⊢ σ ^ 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)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : L ≃ₐ[K] L
hσ : Function.Surjective fun x => σ ^ x
hσ' : orderOf σ = Nat.card (L ≃ₐ[K] L)
⊢ (minpoly K σ.toLinearMap).IsRoot ζ

Tactic:
simpa [minpoly_algEquiv_toLinearMap σ (isOfFinOrder_of_finite σ), hσ',
  sub_eq_zero, IsGalois.card_aut_eq_finrank] using hζ.pow_eq_one

Result:
no goals

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

Tactic:
obtain ⟨σ, hσ⟩ := ‹IsCyclic (L ≃ₐ[K] L)›

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