awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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)
⊢ ∃ (α : 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⟮α⟯ ⊤
have this : 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
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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) ζ
⊢ ∃ (α : 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⟮α⟯ ⊤
have 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⟮α⟯ ⊤
Tactic: obtain ⟨v, hv⟩ := (Module.End.hasEigenvalue_of_isRoot this).exists_hasEigenvector
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ ∃ (α : 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⟮α⟯ ⊤
have hv' : ∀ (n : ℕ), (σ.toLinearMap ^ n : (a : L) → L) v = ζ ^ n • v
Tactic: have hv' := hv.pow_apply
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ ∃ (α : 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⟮α⟯ ⊤
have hv'₁ : ∀ (n : ℕ), (σ ^ n : (a : L) → L) v = ζ ^ n • v
Tactic: simp_rw [← AlgEquiv.pow_toLinearMap, AlgEquiv.toLinearMap_apply] at hv'
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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⟮α⟯ ⊤
have refine_1 : Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) (v ^ finrank K L)
Tactic: refine ⟨v, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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)
⊢ ∃ (α : 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⟮α⟯ ⊤
have refine_2 : Eq (α := IntermediateField K L) K⟮v⟯ ⊤
Tactic: refine ⟨v, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ Membership.mem (γ := Set L) (Set.range.{u_1, u + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) (v ^ finrank K L)
have 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)
Tactic: rw [← IntermediateField.mem_bot,
      ← OrderIso.map_bot IsGalois.intermediateFieldEquivSubgroup.symm]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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)) ⊥) σ'
⊢ 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
have 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
Tactic: obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')
Cleared hypotheses: σ', hσ'
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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)
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ 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
have refine_1₃ : (ζ ^ n • 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]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ 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
have refine_1₄ : (ζ ^ n) ^ finrank K L • 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]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ 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
have refine_1₅ : ζ ^ (n * finrank K L) • 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]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ 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
have refine_1₆ : ζ ^ (finrank K L * n) • 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]