awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)

Tactic:
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Premises used: IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
hodd : p ≠ 2
rw :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    HPow.hPow (α := ℚ) (-1) ((p - 1) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p - 2)

Tactic:
rw [← discr_odd_prime hζ (cyclotomic.irreducible_rat hp.out.pos) hodd]

Premises used: IsCyclotomicExtension.discr_odd_prime, Nat.Prime.pos, Polynomial.cyclotomic.irreducible_rat, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
hodd : p ≠ 2
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)

Tactic:
hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Premises used: IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
hodd : p ≠ 2
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)

Tactic:
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Premises used: IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
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)
rw :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
rw [← discr_prime_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _))]

Premises used: Polynomial.cyclotomic.irreducible_rat, NeZero.pos, IsCyclotomicExtension.discr_prime_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
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)
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)

Tactic:
hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Premises used: IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
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)
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)

Tactic:
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Premises used: IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
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)
rw :
  ∃ (u : ℤˣ) (n : ℕ),
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
        (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
      (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
⊢ ∃ (u : ℤˣ) (n : ℕ),
    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

Tactic:
rw [hζ.discr_zeta_eq_discr_zeta_sub_one.symm]

Premises used: IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
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)
⊢ ∃ (u : ℤˣ) (n : ℕ),
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
        (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
      (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n

Tactic:
discr_prime_pow_eq_unit_mul_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _))

Premises used: IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, Polynomial.cyclotomic.irreducible_rat, NeZero.pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
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)
⊢ ∃ (u : ℤˣ) (n : ℕ),
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
        (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
      (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n

Tactic:
exact discr_prime_pow_eq_unit_mul_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _))

Premises used: IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, Polynomial.cyclotomic.irreducible_rat, NeZero.pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K

Tactic:
⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩

Premises used: Subtype.val_injective, IsIntegralClosure.mk, Subtype.mk, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
refine_1 : ∀ (x : K) (h : IsIntegral ℤ x), Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
refine_2 : ∀ (x : K), (∃ (y : ↥ℤ[ζ]), (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K) y = x) → IsIntegral ℤ x
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K

Tactic:
refine ⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
y : ↥ℤ[ζ]
⊢ IsIntegral ℤ (A := K) ((algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K) y : K)

Tactic:
IsIntegral.algebraMap
        ((le_integralClosure_iff_isIntegral.1
          (adjoin_le_integralClosure (hζ.isIntegral (NeZero.pos _)))).isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
y : ↥ℤ[ζ]
⊢ IsIntegral ℤ (A := K) ((algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K) y : K)

Tactic:
exact
      IsIntegral.algebraMap
        ((le_integralClosure_iff_isIntegral.1
          (adjoin_le_integralClosure (hζ.isIntegral (NeZero.pos _)))).isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
⊢ IsIntegral ℤ B.gen

Tactic:
have hint : IsIntegral ℤ B.gen := (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
    (Algebra.discr (ι := Fin B.dim) ℚ (B := K) (⇑B.basis : (a : Fin B.dim) → K) • x)

Tactic:
have H := discr_mul_isIntegral_mem_adjoin ℚ hint h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
    (Algebra.discr (ι := Fin B.dim) ℚ (B := K) (⇑B.basis : (a : Fin B.dim) → K) • x)
refine_1 :
  ∀ (u : ℤˣ) (n : ℕ)
    (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),
    Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x

Tactic:
obtain ⟨u, n, hun⟩ := discr_prime_pow_eq_unit_mul_pow' hζ

Premises used: IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
    (Algebra.discr (ι := Fin B.dim) ℚ (B := K) (⇑B.basis : (a : Fin B.dim) → K) • x)
u : ℤˣ
n : ℕ
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
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (((↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n) • x)

Tactic:
rw [hun] at H
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
    (Algebra.discr (ι := Fin B.dim) ℚ (B := K) (⇑B.basis : (a : Fin B.dim) → K) • x)
u : ℤˣ
n : ℕ
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] (((↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n) • x)
⊢ 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

Tactic:
rw [hun] at H
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
u : ℤˣ
n : ℕ
H : Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (((↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n) • x)
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
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (u.inv • ((↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n) • x)

Tactic:
replace H := Subalgebra.smul_mem _ H u.inv
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
u : ℤˣ
n : ℕ
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] (u.inv • ((↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n) • x)
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)

Tactic:
rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, zsmul_eq_mul, ← Int.cast_mul,
    Units.inv_mul, Int.cast_one, one_mul, smul_def, map_pow] at H

Premises used: zsmul_eq_mul, smul_assoc, Units.inv_eq_val_inv, Units.inv_mul, smul_mul_assoc, map_pow, Int.cast_mul, Algebra.smul_def, one_mul, Int.cast_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
u : ℤˣ
n : ℕ
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)
refine_1 :
  ∀ [hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K] (hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)),
    let B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ;
    ∀ (hint : IsIntegral ℤ B.gen)
      (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
refine_1₁ :
  ∀ (n_1 : ℕ) [hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))),
    let B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ;
    ∀ (hint : IsIntegral ℤ B.gen)
      (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
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x

Tactic:
cases k
-- 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 : 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)
⊢ IsCyclotomicExtension {1} ℚ K

Tactic:
simpa using hcycl
-- 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 : 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)
⊢ IsCyclotomicExtension {1} ℚ K

Tactic:
haveI : IsCyclotomicExtension {1} ℚ K := by simpa using hcycl
-- 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
rw : Membership.mem (γ := Subalgebra ℚ K) ⊤ x
⊢ Membership.mem (γ := Subalgebra ℚ K) ⊥ x

Tactic:
rw [singleton_one ℚ K]

Premises used: Rat, IsCyclotomicExtension.singleton_one
-- 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:
mem_top

Premises used: Algebra.mem_top, Set.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 : ℕ
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:
exact mem_top

Premises used: Algebra.mem_top