awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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 : ℕ
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
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
this : IsCyclotomicExtension {1} ℚ K
⊢ Membership.mem (γ := Subalgebra ℚ K) ⊥ x

Tactic:
have : x ∈ (⊥ : Subalgebra ℚ K) := by
      rw [singleton_one ℚ K]
      exact mem_top
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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 : ℕ
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
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
this_2 : IsCyclotomicExtension {1} ℚ K
this : Membership.mem (γ := Subalgebra ℚ K) ⊥ x
refine_1 :
  ∀ (y : ℚ) (h : IsIntegral ℤ (A := K) ((algebraMap ℚ K : (a : ℚ) → K) y : K))
    (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)),
    Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℚ K : (a : ℚ) → K) y : K)
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x

Tactic:
obtain ⟨y, rfl⟩ := mem_bot.1 this

Premises used: Algebra.mem_bot, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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 : IsIntegral ℤ (A := K) ((algebraMap ℚ K : (a : ℚ) → K) y : K)
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)
⊢ IsIntegral ℤ y

Tactic:
replace h := (isIntegral_algebraMap_iff (algebraMap ℚ K).injective).1 h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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
refine_1 :
  ∀ (z : ℤ) (hz : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) z = y),
    Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℚ K : (a : ℚ) → K) y : K)
⊢ Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℚ K : (a : ℚ) → K) y : K)

Tactic:
obtain ⟨z, hz⟩ := IsIntegrallyClosed.isIntegral_iff.1 h

Premises used: IsIntegrallyClosed.isIntegral_iff, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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
refine_1 : Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℤ K : (a : ℤ) → K) z : K)
⊢ Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℚ K : (a : ℚ) → K) y : K)

Tactic:
rw [← hz, ← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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) z : K)

Tactic:
Subalgebra.algebraMap_mem _ _

Premises used: Set.Mem, Subalgebra.algebraMap_mem
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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) z : K)

Tactic:
exact Subalgebra.algebraMap_mem _ _

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
⊢ minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)

Tactic:
have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
⊢ 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 _))
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
⊢ minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))

Tactic:
rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁

Premises used: IsPrimitiveRoot.subOnePowerBasis_gen
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
h₃ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
⊢ minpoly ℚ (ζ - 1) = comp (cyclotomic (p ^ (n_1 + 1)) ℚ) (HAdd.hAdd (α := ℚ[X]) X 1)

Tactic:
rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁

Premises used: IsPrimitiveRoot.subOnePowerBasis_gen
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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 ℤ ℚ) (cyclotomic (p ^ (n_1 + 1)) ℤ)).comp (HAdd.hAdd (α := ℚ[X]) X 1)
⊢ HAdd.hAdd (α := ℚ[X]) X 1 = map (algebraMap ℤ ℚ) (HAdd.hAdd (α := ℤ[X]) X 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
⊢ 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₂

Premises used: Polynomial.map_cyclotomic_int, algebraMap_int_eq, Polynomial.map_comp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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))
rw : (comp (cyclotomic (p ^ (n_1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))
⊢ IsEisensteinAt (minpoly ℤ B.gen) (ℤ ∙ (↑p : ℤ))

Tactic:
rw [IsPrimitiveRoot.subOnePowerBasis_gen,
        map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]

Premises used: Algebra.algebraMap, Rat, Polynomial.map_injective, Int, IsPrimitiveRoot.subOnePowerBasis_gen, RingHom.injective_int
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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))
⊢ (comp (cyclotomic (p ^ (n_1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))

Tactic:
cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _

Premises used: cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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))
⊢ (comp (cyclotomic (p ^ (n_1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))

Tactic:
exact cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _

Premises used: cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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 : ℤ))

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 _
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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) ℤ[B.gen] (HPow.hPow (α := ℤ) (↑p : ℤ) n • x)

Tactic:
simpa using H
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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 : ℤ))
refine_1 : {B.gen} ⊆ (↑ℤ[ζ] : Set K)
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x

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)

Premises used: Nat.prime_iff_prime_int, Algebra.adjoin_le, Iff.mp, mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt, Fact.out