awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this_1 : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
this_2 : IsCyclotomicExtension {1} ℚ K
y : ℚ
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
    (HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n)
      ((algebraMap ℚ K : (a : ℚ) → K) y : K))
this : Membership.mem (α := K) (γ := Subalgebra ℚ K) ⊥ ((algebraMap ℚ K : (a : ℚ) → K) y : K)
h : IsIntegral ℤ y
⊢ Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℚ K : (a : ℚ) → K) y : K)
have refine_1 : ∀ (z : ℤ) (hz : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) z = y),
  Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℚ K : (a : ℚ) → K) y : K)
Tactic: obtain ⟨z, hz⟩ := IsIntegrallyClosed.isIntegral_iff.1 h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this_1 : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
this_2 : IsCyclotomicExtension {1} ℚ K
y : ℚ
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
    (HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n)
      ((algebraMap ℚ K : (a : ℚ) → K) y : K))
this : Membership.mem (α := K) (γ := Subalgebra ℚ K) ⊥ ((algebraMap ℚ K : (a : ℚ) → K) y : K)
h : IsIntegral ℤ y
z : ℤ
hz : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) z = y
⊢ Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℚ K : (a : ℚ) → K) y : K)
have refine_1 : Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℤ K : (a : ℤ) → K) z : K)
Tactic: rw [← hz, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
have h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
Tactic: have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
have h₂ : minpoly ℚ (ζ - 1) = comp (cyclotomic (p ^ (n_1 + 1)) ℚ) (HAdd.hAdd (α := ℚ[X]) X 1)
Tactic: have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (NeZero.pos _))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
h₂ : minpoly ℚ (ζ - 1) = comp (cyclotomic (p ^ (n_1 + 1)) ℚ) (HAdd.hAdd (α := ℚ[X]) X 1)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
have h₃ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
Tactic: rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : minpoly ℚ (ζ - 1) = comp (cyclotomic (p ^ (n_1 + 1)) ℚ) (HAdd.hAdd (α := ℚ[X]) X 1)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
have h₃ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) =
  map (algebraMap ℤ ℚ) (comp (cyclotomic (p ^ (n_1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1))
Tactic: rw [h₁, ← map_cyclotomic_int, ← algebraMap_int_eq,
        show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ :
  map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) =
    map (algebraMap ℤ ℚ) (comp (cyclotomic (p ^ (n_1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1))
⊢ IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
have rw : (comp (cyclotomic (p ^ (n_1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))
Tactic: rw [IsPrimitiveRoot.subOnePowerBasis_gen,
        map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have hmin : IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
Tactic: have hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {(p : ℤ)}) := by
      have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
      have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (NeZero.pos _))
      rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁
      rw [h₁, ← map_cyclotomic_int, ← algebraMap_int_eq,
        show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂
      rw [IsPrimitiveRoot.subOnePowerBasis_gen,
        map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
      exact cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
hmin : IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have refine_1 : {B.gen} ⊆ (↑ℤ[ζ] : Set K)
Tactic: refine
      adjoin_le ?_
        (mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt (n := n)
          (Nat.prime_iff_prime_int.1 hp.out) hint h (by simpa using H) hmin)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n_1 : ℕ
hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
hmin : IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))
⊢ {B.gen} ⊆ (↑ℤ[ζ] : Set K)
have refine_1 : Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] B.gen
Tactic: simp only [Set.singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K
have hcycl₁ : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
Tactic: rw [← pow_one p] at hζ hcycl
Cleared hypotheses: hcycl, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
hcycl₁ : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 1} ℚ K
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K
have hζ₁ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)
Tactic: rw [← pow_one p] at hζ hcycl
Cleared hypotheses: hcycl, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
have hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
Tactic: have hζ := zeta_spec (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
have refine_1 : ∀ (x : CyclotomicField (p ^ k) ℚ) (h : IsIntegral ℤ x),
  Membership.mem (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
    (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1}) x
Tactic: refine ⟨IsFractionRing.injective _ _, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
refine_1 :
  ∀ (x : CyclotomicField (p ^ k) ℚ) (h : IsIntegral ℤ x),
    Membership.mem (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
      (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1}) x
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
have refine_2 : ∀ (x : CyclotomicField (p ^ k) ℚ),
  (∃ (y : CyclotomicRing (p ^ k) ℤ ℚ),
      (algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ) :
            (a : CyclotomicRing (p ^ k) ℤ ℚ) → CyclotomicField (p ^ k) ℚ)
          y =
        x) →
    IsIntegral ℤ x
Tactic: refine ⟨IsFractionRing.injective _ _, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
⊢ Membership.mem (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
    (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1}) x
have refine_1 : ∀ (y : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)])
  (h :
    IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
      ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
            (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
          y :
        CyclotomicField (p ^ k) ℚ)),
  Membership.mem (α := CyclotomicField (p ^ k) ℚ) (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
    (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1})
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)
Tactic: obtain ⟨y, rfl⟩ := (isIntegralClosure_adjoin_singleton_of_prime_pow hζ).isIntegral_iff.1 h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)
⊢ Membership.mem (α := CyclotomicField (p ^ k) ℚ) (γ := Subalgebra ℤ (CyclotomicField (p ^ k) ℚ))
    (adjoin ℤ {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1})
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)
have refine_1 : Subset (α := Set (CyclotomicField (p ^ k) ℚ)) {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}
  {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1}
Tactic: refine adjoin_mono ?_ y.2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (M := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField (p ^ k) ℚ)
    ((algebraMap (↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) (CyclotomicField (p ^ k) ℚ) :
          (a : ↥ℤ[zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)]) → CyclotomicField (p ^ k) ℚ)
        y :
      CyclotomicField (p ^ k) ℚ)
⊢ Subset (α := Set (CyclotomicField (p ^ k) ℚ)) {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}
    {b : CyclotomicField (p ^ k) ℚ | b ^ p ^ k = 1}
have refine_1 : HPow.hPow (α := CyclotomicField (p ^ k) ℚ) (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k) = 1
Tactic: simp only [Set.singleton_subset_iff, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)
have rw : IsIntegralClosure (CyclotomicRing (HPow.hPow (β := ℕ) p 1) ℤ ℚ) ℤ (CyclotomicField (HPow.hPow (β := ℕ) p 1) ℚ)
Tactic: rw [← pow_one p]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
hk : 1 < k
hζ : IsPrimitiveRoot ζ k
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}))
have refine : ∀ (h : Eq (α := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}) ⊥), False
Tactic: refine Ideal.finiteQuotientOfFreeOfNeBot _ (fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
hk : 1 < k
hζ : IsPrimitiveRoot ζ k
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}) ⊥
⊢ False
have h₁ : hζ.toInteger = 1
Tactic: simp only [Ideal.span_singleton_eq_bot, sub_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
inst_2 : NeZero k
hζ : IsPrimitiveRoot ζ k
⊢ Nat.card.{u} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1})) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
have rw : Submodule.cardQuot.{u, u} (R := 𝓞 K) (M := 𝓞 K) (Ideal.span {hζ.toInteger - 1}) =
  Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
Tactic: rw [← Submodule.cardQuot_apply, ← Ideal.absNorm_apply, Ideal.absNorm_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
inst_2 : NeZero k
hζ : IsPrimitiveRoot ζ k
rw :
  Submodule.cardQuot.{u, u} (R := 𝓞 K) (M := 𝓞 K) (Ideal.span {hζ.toInteger - 1}) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
⊢ Nat.card.{u} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1})) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
have rw₁ : (Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) =
  Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
Tactic: rw [← Submodule.cardQuot_apply, ← Ideal.absNorm_apply, Ideal.absNorm_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : NumberField K
k : ℕ
inst_2 : NeZero k
hζ : IsPrimitiveRoot ζ k
rw :
  Submodule.cardQuot.{u, u} (R := 𝓞 K) (M := 𝓞 K) (Ideal.span {hζ.toInteger - 1}) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
rw₁ :
  (Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
⊢ Nat.card.{u} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1})) =
    Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
have rw₂ : Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1)) =
  Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1))
Tactic: rw [← Submodule.cardQuot_apply, ← Ideal.absNorm_apply, Ideal.absNorm_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.integralPowerBasisOfPrimePow.gen = (↑hζ.toInteger : K)
have rw : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
    ((hζ.adjoinEquivRingOfIntegersOfPrimePow : (a : ↥ℤ[ζ]) → 𝓞 K)
        (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ sorry) :
      𝓞 K) =
  (↑hζ.toInteger : K)
Tactic: rw [integralPowerBasisOfPrimePow, PowerBasis.map_gen, adjoin.powerBasis'_gen]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((hζ.adjoinEquivRingOfIntegersOfPrimePow : (a : ↥ℤ[ζ]) → 𝓞 K)
          (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ ⋯) :
        𝓞 K) =
    (↑hζ.toInteger : K)
have simp : (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K)
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ sorry) =
  ζ
Tactic: simp only [adjoinEquivRingOfIntegersOfPrimePow_apply, IsIntegralClosure.algebraMap_lift]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ Eq (α := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯] ⊤
have refine : Membership.mem (γ := Subalgebra ℤ (𝓞 K))
  ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) sorry]
  hζ.integralPowerBasisOfPrimePow.gen
Tactic: refine hζ.integralPowerBasisOfPrimePow.adjoin_eq_top_of_gen_mem_adjoin ?_