awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_1₆ : ζ ^ (finrank K L * 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₇ : (ζ ^ 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]
-- 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
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
⊢ 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 (α := K) 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
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
⊢ 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₉ : HSMul.hSMul.{u, u_1, u_1} (α := K) 1 (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
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
⊢ 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₁₀ : 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σ' : 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
⊢ Eq (α := IntermediateField K L) K⟮v⟯ ⊤
have 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))ᵒᵈ)
Tactic: apply IsGalois.intermediateFieldEquivSubgroup.injective
-- 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
⊢ 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))ᵒᵈ)
have 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))ᵒᵈ)
Tactic: rw [map_top, eq_top_iff]
-- 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))
    ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField K L) → (Subgroup Gal(L/K))ᵒᵈ) K⟮v⟯ :
      (Subgroup Gal(L/K))ᵒᵈ)
    σ'
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ σ'
have 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)
Tactic: obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')
Cleared hypotheses: σ', hσ'
-- 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σ'_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)
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ (σ ^ n)
have this₁ : σ ^ n • (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ (↑K⟮v⟯ : Set L)) v sorry) : L) =
  (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ (↑K⟮v⟯ : Set L)) v sorry) : L)
Tactic: have := hσ' ⟨v, IntermediateField.mem_adjoin_simple_self K v⟩
-- 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σ'_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)
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ (σ ^ n)
have this₁ : ζ ^ n • v = v
Tactic: simp only [AlgEquiv.smul_def, hv'] at this
Cleared hypotheses: this
-- 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_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
| v
have rw : HSMul.hSMul.{u, u_1, u_1} (α := K) 1 v
Tactic: rw [← one_smul K v]
-- 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σ'_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
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ (σ ^ n)
have this₁ : ζ ^ n • v = HSMul.hSMul.{u, u_1, u_1} (α := K) 1 v
Tactic: conv_rhs at this => rw [← one_smul K v]
Cleared hypotheses: this
-- 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_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
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ (σ ^ n)
have 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))
Tactic: obtain ⟨k, rfl⟩ := hζ.dvd_of_pow_eq_one n (smul_left_injective K hv.2 this)
Cleared hypotheses: n, hσ', this
-- 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_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
⊢ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ (σ ^ (finrank K L * k))
have refine_2 : Membership.mem (γ := Subgroup Gal(L/K)) ⊤ 1
Tactic: rw [pow_mul, ← IsGalois.card_aut_eq_finrank, pow_card_eq_one', one_pow]
-- 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
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
⊢ HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]) = minpoly K α
have refine_1 : Eq.{u_1 + 1} (α := L)
  ((aeval α : (a : K [X]) → L)
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) :
    L)
  (0 : L)
Tactic: refine minpoly.unique _ _ (monic_X_pow_sub_C _ finrank_pos.ne.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
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
refine_1 :
  Eq.{u_1 + 1} (α := L)
    ((aeval α : (a : K [X]) → L)
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) :
      L)
    (0 : L)
⊢ HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]) = minpoly K α
have refine_2 : ∀ (q : K [X]),
  q.Monic →
    Eq.{u_1 + 1} (α := L) ((aeval α : (a : K [X]) → L) q : L) (0 : L) →
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).degree ≤
        q.degree
Tactic: refine minpoly.unique _ _ (monic_X_pow_sub_C _ finrank_pos.ne.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
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
q : K [X]
hq : q.Monic
hq' : Eq.{u_1 + 1} (α := L) ((aeval α : (a : K [X]) → L) q : L) (0 : L)
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).degree ≤ q.degree
have refine_2 : (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).degree ≤
  degree (minpoly K α)
Tactic: refine le_trans ?_ (degree_le_of_dvd (minpoly.dvd _ _ hq') hq.ne_zero)
-- 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
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L : (a : K) → L) a
hα : Eq (α := IntermediateField K L) K⟮α⟯ ⊤
q : K [X]
hq : q.Monic
hq' : Eq.{u_1 + 1} (α := L) ((aeval α : (a : K [X]) → L) q : L) (0 : L)
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])).degree ≤
    degree (minpoly K α)
have refine_2 : finrank K L ≤ finrank.{u, u_1} K ↥⊤
Tactic: rw [degree_X_pow_sub_C finrank_pos,
        degree_eq_natDegree (minpoly.ne_zero (IsIntegral.of_finite K α)),
        ← IntermediateField.adjoin.finrank (IsIntegral.of_finite K α), hα, Nat.cast_le]