awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : ζ ∈ primitiveRoots (finrank K L) K
⊢ IsPrimitiveRoot ζ (finrank K L)

Tactic:
rw [mem_primitiveRoots finrank_pos] at hζ

Premises used: mem_primitiveRoots, Module.finrank_pos
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
obtain :
  ∀ (σ : Gal(L/K)) (hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ ∃ (α : L),
    Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) (α ^ finrank K L) ∧
      Eq (α := IntermediateField K L) K⟮α⟯ ⊤

Tactic:
obtain ⟨σ, hσ⟩ := ‹IsCyclic Gal(L/K)›

Premises used: AlgEquiv, IsCyclic
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
⊢ orderOf σ = Nat.card.{u_1} Gal(L/K)

Tactic:
have hσ' := orderOf_eq_card_of_forall_mem_zpowers hσ
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
⊢ orderOf σ = finrank K L

Tactic:
rw [IsGalois.card_aut_eq_finrank] at hσ'

Premises used: IsGalois.card_aut_eq_finrank
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = finrank K L
⊢ IsRoot (minpoly K σ.toLinearMap) ζ

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

Premises used: sub_eq_zero, isOfFinOrder_of_finite, minpoly_algEquiv_toLinearMap, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
⊢ IsRoot (minpoly K σ.toLinearMap) ζ

Tactic:
have : IsRoot (minpoly K σ.toLinearMap) ζ := by
    rw [IsGalois.card_aut_eq_finrank] at hσ'
    simpa [minpoly_algEquiv_toLinearMap σ (isOfFinOrder_of_finite σ), hσ',
      sub_eq_zero] using hζ.pow_eq_one
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
obtain :
  ∀ (v : L) (hv : End.HasEigenvector σ.toLinearMap ζ v),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ ∃ (α : L),
    Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) (α ^ finrank K L) ∧
      Eq (α := IntermediateField K L) K⟮α⟯ ⊤

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

Premises used: Module.End.hasEigenvalue_of_isRoot, Module.End.HasEigenvalue.exists_hasEigenvector
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
⊢ ∀ (n : ℕ), (σ.toLinearMap ^ n : (a : L) → L) v = ζ ^ n • v

Tactic:
have hv' := hv.pow_apply
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ.toLinearMap ^ n : (a : L) → L) v = ζ ^ n • v
⊢ ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v

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

Premises used: AlgEquiv.pow_toLinearMap, AlgEquiv.toLinearMap_apply
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
⊢ ∃ (α : L),
    Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) (α ^ finrank K L) ∧
      Eq (α := IntermediateField K L) K⟮α⟯ ⊤

Tactic:
⟨v, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
refine_1 :
  Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) (v ^ finrank K L)
refine_2 : Eq (α := IntermediateField K L) K⟮v⟯ ⊤
⊢ ∃ (α : L),
    Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) (α ^ finrank K L) ∧
      Eq (α := IntermediateField K L) K⟮α⟯ ⊤

Tactic:
refine ⟨v, ?_, ?_⟩
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
refine_1 :
  Membership.mem (γ := IntermediateField K L)
    ((OrderIso.symm IsGalois.intermediateFieldEquivSubgroup : (a : (Subgroup Gal(L/K))ᵒᵈ) → IntermediateField K L) ⊥ :
      IntermediateField K L)
    (v ^ finrank K L)
⊢ Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) (v ^ finrank K L)

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

Premises used: OrderIso.symm, IsGalois.intermediateFieldEquivSubgroup, IntermediateField.mem_bot, OrderIso.map_bot
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
σ' : Gal(L/K)
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K)) ((OrderDual.ofDual : (a : (Subgroup Gal(L/K))ᵒᵈ) → Subgroup Gal(L/K)) ⊥) σ'
refine_1 :
  ∀ (n : ℕ)
    (hσ' :
      Membership.mem (γ := Subgroup Gal(L/K)) ((OrderDual.ofDual : (a : (Subgroup Gal(L/K))ᵒᵈ) → Subgroup Gal(L/K)) ⊥)
        (σ ^ n)),
    Subtype.mk (p := fun (x : Gal(L/K)) ↦
          Membership.mem (γ := Subgroup Gal(L/K))
            ((OrderDual.ofDual : (a : (Subgroup Gal(L/K))ᵒᵈ) → Subgroup Gal(L/K)) ⊥) x)
          (σ ^ n) hσ' •
        v ^ finrank K L =
      v ^ finrank K L
⊢ Subtype.mk (p := fun (x : Gal(L/K)) ↦
        Membership.mem (γ := Subgroup Gal(L/K)) ((OrderDual.ofDual : (a : (Subgroup Gal(L/K))ᵒᵈ) → Subgroup Gal(L/K)) ⊥)
          x)
        σ' hσ' •
      v ^ finrank K L =
    v ^ finrank K L

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

Premises used: Iff.mpr, mem_powers_iff_mem_zpowers, rfl
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
n : ℕ
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K)) ((OrderDual.ofDual : (a : (Subgroup Gal(L/K))ᵒᵈ) → Subgroup Gal(L/K)) ⊥)
    (σ ^ n)
refine_1 :
  (Subtype.mk (p := fun (x : Gal(L/K)) ↦
          Membership.mem (γ := Subgroup Gal(L/K))
            ((OrderDual.ofDual : (a : (Subgroup Gal(L/K))ᵒᵈ) → Subgroup Gal(L/K)) ⊥) x)
          (σ ^ n) hσ' •
        v) ^
      finrank K L =
    v ^ finrank K L
refine_1₁ :
  ((↑(Subtype.mk (p := fun (x : Gal(L/K)) ↦
              Membership.mem (γ := Subgroup Gal(L/K))
                ((OrderDual.ofDual : (a : (Subgroup Gal(L/K))ᵒᵈ) → Subgroup Gal(L/K)) ⊥) x)
              (σ ^ n) hσ') :
          Gal(L/K)) •
        v) ^
      finrank K L =
    v ^ finrank K L
refine_1₂ :
  HPow.hPow (α := L)
      (((↑(Subtype.mk (p := fun (x : Gal(L/K)) ↦
                  Membership.mem (γ := Subgroup Gal(L/K))
                    ((OrderDual.ofDual : (a : (Subgroup Gal(L/K))ᵒᵈ) → Subgroup Gal(L/K)) ⊥) x)
                  (σ ^ n) hσ') :
              Gal(L/K)) :
            (a : L) → L)
          v :
        L)
      (finrank K L) =
    v ^ finrank K L
refine_1₃ : (ζ ^ n • v) ^ finrank K L = v ^ finrank K L
refine_1₄ : (ζ ^ n) ^ finrank K L • v ^ finrank K L = v ^ finrank K L
refine_1₅ : ζ ^ (n * finrank K L) • v ^ finrank K L = v ^ finrank K L
refine_1₆ : ζ ^ (finrank K L * n) • v ^ finrank K L = v ^ finrank K L
refine_1₇ : (ζ ^ finrank K L) ^ n • v ^ finrank K L = v ^ finrank K L
refine_1₈ : HPow.hPow (α := K) 1 n • v ^ finrank K L = v ^ finrank K L
refine_1₉ : HSMul.hSMul.{u, u_1, u_1} (α := K) 1 (v ^ finrank K L) = v ^ finrank K L
refine_1₁₀ refine_1₁₁ : v ^ finrank K L = v ^ finrank K L
⊢ Subtype.mk (p := fun (x : Gal(L/K)) ↦
        Membership.mem (γ := Subgroup Gal(L/K)) ((OrderDual.ofDual : (a : (Subgroup Gal(L/K))ᵒᵈ) → Subgroup Gal(L/K)) ⊥)
          x)
        (σ ^ 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]

Premises used: one_pow, smul_pow', AlgEquiv.smul_def, pow_mul, one_smul, Submonoid.smul_def, smul_pow, mul_comm, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
refine_2 :
  Eq (α := (Subgroup Gal(L/K))ᵒᵈ)
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) ⊤ :
      (Subgroup Gal(L/K))ᵒᵈ)
⊢ Eq (α := IntermediateField K L) K⟮v⟯ ⊤

Tactic:
apply IsGalois.intermediateFieldEquivSubgroup.injective

Premises used: OrderIso.injective, IsGalois.intermediateFieldEquivSubgroup
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ' : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
refine_2 :
  LE.le (α := (Subgroup Gal(L/K))ᵒᵈ) (⊤ : (Subgroup Gal(L/K))ᵒᵈ)
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
⊢ Eq (α := (Subgroup Gal(L/K))ᵒᵈ)
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) ⊤ :
      (Subgroup Gal(L/K))ᵒᵈ)

Tactic:
rw [map_top, eq_top_iff]

Premises used: eq_top_iff, TopHomClass.map_top
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
σ' : Gal(L/K)
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    σ'
refine_2 :
  ∀ (n : ℕ)
    (hσ' :
      Membership.mem (γ := Subgroup Gal(L/K))
        ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
          (Subgroup Gal(L/K))ᵒᵈ)
        (σ ^ n)),
    Membership.mem (γ := Subgroup Gal(L/K)) ⊤ (σ ^ n)
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ σ'

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

Premises used: Iff.mpr, mem_powers_iff_mem_zpowers, rfl
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
n : ℕ
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    (σ ^ n)
⊢ σ ^ n • (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ (↑K⟮v⟯ : Set L)) v ⋯) : L) =
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ (↑K⟮v⟯ : Set L)) v ⋯) : L)

Tactic:
have := hσ' ⟨v, IntermediateField.mem_adjoin_simple_self K v⟩
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this_1 : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
n : ℕ
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    (σ ^ n)
this :
  σ ^ n • (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ (↑K⟮v⟯ : Set L)) v ⋯) : L) =
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ (↑K⟮v⟯ : Set L)) v ⋯) : L)
⊢ ζ ^ n • v = v

Tactic:
simp only [AlgEquiv.smul_def, hv'] at this

Premises used: AlgEquiv.smul_def
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this_1 : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
n : ℕ
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    (σ ^ n)
this : ζ ^ n • v = v
rw : HSMul.hSMul.{u, u_1, u_1} (α := K) 1 v
| v

Tactic:
rw [← one_smul K v]

Premises used: one_smul
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this_1 : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
n : ℕ
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    (σ ^ n)
this : ζ ^ n • v = v
⊢ ζ ^ n • v = HSMul.hSMul.{u, u_1, u_1} (α := K) 1 v

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

Premises used: one_smul
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this_1 : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
n : ℕ
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    (σ ^ n)
this : ζ ^ n • v = HSMul.hSMul.{u, u_1, u_1} (α := K) 1 v
refine_2 :
  ∀ (k : ℕ)
    (hσ' :
      Membership.mem (γ := Subgroup Gal(L/K))
        ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
          (Subgroup Gal(L/K))ᵒᵈ)
        (σ ^ (finrank K L * k)))
    (this : ζ ^ (finrank K L * k) • v = HSMul.hSMul.{u, u_1, u_1} (α := K) 1 v),
    Membership.mem (γ := Subgroup Gal(L/K)) ⊤ (σ ^ (finrank K L * k))
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ (σ ^ n)

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

Premises used: smul_left_injective, And.right, IsPrimitiveRoot.dvd_of_pow_eq_one, rfl
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst_4 : IsGalois K L
inst_5 : IsCyclic.{u_1} Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective.{1, u_1 + 1} (β := Gal(L/K)) fun (x : ℤ) ↦ σ ^ x
hσ'_1 : orderOf σ = Nat.card.{u_1} Gal(L/K)
this_1 : IsRoot (minpoly K σ.toLinearMap) ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
k : ℕ
hσ' :
  Membership.mem (γ := Subgroup Gal(L/K))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    (σ ^ (finrank K L * k))
this : ζ ^ (finrank K L * k) • v = HSMul.hSMul.{u, u_1, u_1} (α := K) 1 v
refine_2 : Membership.mem (γ := Subgroup Gal(L/K)) ⊤ 1
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ (σ ^ (finrank K L * k))

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

Premises used: one_pow, IsGalois.card_aut_eq_finrank, pow_card_eq_one', pow_mul