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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
hk : k = 0
pos : ∀ (htwo : p ≠ 2), 2 < p
⊢ 1 < p ^ k * (p - 1)

Tactic:
simp only [hk, zero_add, pow_one, pow_zero, one_mul, Nat.lt_sub_iff_add_lt,
        Nat.reduceAdd] at htwo ⊢

Premises used: Nat.lt_sub_iff_add_lt, Nat.reduceAdd, zero_add, pow_zero, pow_one, one_mul
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
hk : k = 0
htwo : p ≠ 2
⊢ 2 < p

Tactic:
htwo.symm.lt_of_le hp.1.two_le

Premises used: Ne.symm, Nat.Prime.two_le, Ne.lt_of_le, Fact.out
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
hk : k = 0
htwo : p ≠ 2
⊢ 2 < p

Tactic:
exact htwo.symm.lt_of_le hp.1.two_le

Premises used: Ne.symm, Nat.Prime.two_le, Ne.lt_of_le, Fact.out
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
hk : ¬k = 0
this : 2 ≤ p
⊢ 1 ≤ p - 1

Tactic:
lia
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
hk : ¬k = 0
⊢ 1 < p ^ k * (p - 1)

Tactic:
exact one_lt_mul_of_lt_of_le (one_lt_pow₀ hp.1.one_lt hk)
        (have := Nat.Prime.two_le hp.out; by lia)

Premises used: Nat.Prime.one_lt, one_lt_mul_of_lt_of_le, Nat.Prime.two_le, one_lt_pow₀, Fact.out
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
⊢ 1 < pB.dim

Tactic:
replace hdim : 1 < pB.dim := by
    rw [Nat.one_lt_iff_ne_zero_and_ne_one, hdim]
    refine ⟨by simp only [ne_eq, mul_eq_zero, NeZero.ne _, Nat.sub_eq_zero_iff_le, false_or,
      not_le, Nat.Prime.one_lt hp.out], ne_of_gt ?_⟩
    by_cases hk : k = 0
    · simp only [hk, zero_add, pow_one, pow_zero, one_mul, Nat.lt_sub_iff_add_lt,
        Nat.reduceAdd] at htwo ⊢
      exact htwo.symm.lt_of_le hp.1.two_le
    · exact one_lt_mul_of_lt_of_le (one_lt_pow₀ hp.1.one_lt hk)
        (have := Nat.Prime.two_le hp.out; by lia)
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
⊢ hζ.toInteger = (↑p : 𝓞 K) * x + (↑n : 𝓞 K)

Tactic:
rw [sub_eq_iff_eq_add] at h

Premises used: sub_eq_iff_eq_add
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h₁ : hζ.toInteger = (↑p : 𝓞 K) * x + (↑n : 𝓞 K)
⊢ let pB := hζ.integralPowerBasisOfPrimePow;
  1 < pB.dim

Tactic:
rw [sub_eq_iff_eq_add] at h

Premises used: sub_eq_iff_eq_add
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger = (↑p : 𝓞 K) * x + (↑n : 𝓞 K)
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
⊢ Eq (α := ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) hζ.toInteger : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)

Tactic:
replace h := pB.basis.ext_elem_iff.1 h ⟨1, hdim⟩
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h :
  Eq (α := ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) hζ.toInteger : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
⊢ (pB.basis : (a : Fin pB.dim) → 𝓞 K) (⟨1, hdim⟩ : Fin pB.dim) = pB.gen ^ (↑(⟨1, hdim⟩ : Fin pB.dim) : ℕ)

Tactic:
have := pB.basis_eq_pow ⟨1, hdim⟩
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h :
  Eq (α := ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) hζ.toInteger : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
this : (pB.basis : (a : Fin pB.dim) → 𝓞 K) (⟨1, hdim⟩ : Fin pB.dim) = pB.gen ^ (↑(⟨1, hdim⟩ : Fin pB.dim) : ℕ)
⊢ (pB.basis : (a : Fin pB.dim) → 𝓞 K) (⟨1, hdim⟩ : Fin pB.dim) = hζ.toInteger ^ (↑(⟨1, hdim⟩ : Fin pB.dim) : ℕ)

Tactic:
rw [hζ.integralPowerBasisOfPrimePow_gen] at this

Premises used: IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h :
  Eq (α := ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) hζ.toInteger : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
this : (pB.basis : (a : Fin pB.dim) → 𝓞 K) (⟨1, hdim⟩ : Fin pB.dim) = hζ.toInteger ^ (↑(⟨1, hdim⟩ : Fin pB.dim) : ℕ)
⊢ pB.gen = hζ.toInteger

Tactic:
simp only [PowerBasis.coe_basis, pow_one] at this

Premises used: PowerBasis.coe_basis, pow_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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h :
  Eq (α := ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) pB.gen : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
this : pB.gen = hζ.toInteger
⊢ pB.gen = pB.gen ^ (↑(⟨1, hdim⟩ : Fin pB.dim) : ℕ)

Tactic:
simp
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h :
  Eq (α := ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) hζ.toInteger : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
this : pB.gen = hζ.toInteger
⊢ Eq (α := ℤ) (if (⟨1, hdim⟩ : Fin pB.dim) = ⟨1, hdim⟩ then 1 else 0 : ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)

Tactic:
rw [← this, show pB.gen = pB.gen ^ (⟨1, hdim⟩ : Fin pB.dim).1 by simp, ← pB.basis_eq_pow,
    pB.basis.repr_self_apply] at h

Premises used: Module.Basis.repr_self_apply, PowerBasis.basis, PowerBasis.basis_eq_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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h :
  Eq (α := ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) hζ.toInteger : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
this : pB.gen = hζ.toInteger
h₁ :
  Eq (α := ℤ) (if (⟨1, hdim⟩ : Fin pB.dim) = ⟨1, hdim⟩ then 1 else 0 : ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
⊢ pB.gen = hζ.toInteger

Tactic:
rw [← this, show pB.gen = pB.gen ^ (⟨1, hdim⟩ : Fin pB.dim).1 by simp, ← pB.basis_eq_pow,
    pB.basis.repr_self_apply] at h

Premises used: Module.Basis.repr_self_apply, PowerBasis.basis, PowerBasis.basis_eq_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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h :
  Eq (α := ℤ) (if (⟨1, hdim⟩ : Fin pB.dim) = ⟨1, hdim⟩ then 1 else 0 : ℤ)
    ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x + (↑n : 𝓞 K)) : Fin pB.dim →₀ ℤ) :
          (a : Fin pB.dim) → ℤ)
        (⟨1, hdim⟩ : Fin pB.dim) :
      ℤ)
this : pB.gen = hζ.toInteger
⊢ 1 =
    HAdd.hAdd (α := ℤ) (β := ℤ)
      ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x) : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
          (⟨1, hdim⟩ : Fin pB.dim) :
        ℤ)
      ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) (↑n : 𝓞 K) : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
          (⟨1, hdim⟩ : Fin pB.dim) :
        ℤ)

Tactic:
simp only [↓reduceIte, map_add, Finsupp.coe_add, Pi.add_apply] at h

Premises used: map_add, Pi.add_apply, Finsupp.coe_add, reduceIte
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h :
  1 =
    HAdd.hAdd (α := ℤ) (β := ℤ)
      ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x) : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
          (⟨1, hdim⟩ : Fin pB.dim) :
        ℤ)
      ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) (↑n : 𝓞 K) : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
          (⟨1, hdim⟩ : Fin pB.dim) :
        ℤ)
⊢ (↑p : 𝓞 K) * x = HSMul.hSMul (α := ℤ) (↑p : ℤ) x

Tactic:
simp
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h :
  1 =
    HSMul.hSMul (α := ℤ) (β := ℤ) (↑p : ℤ) ((pB.basis.coord (⟨1, hdim⟩ : Fin pB.dim) : (a : 𝓞 K) → ℤ) x : ℤ) +
      HSMul.hSMul (β := ℤ) n ((pB.basis.coord (⟨1, hdim⟩ : Fin pB.dim) : (a : 𝓞 K) → ℤ) 1 : ℤ)
⊢ 0 < pB.dim

Tactic:
lia
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h :
  1 =
    HSMul.hSMul (α := ℤ) (β := ℤ) (↑p : ℤ) ((pB.basis.coord (⟨1, hdim⟩ : Fin pB.dim) : (a : 𝓞 K) → ℤ) x : ℤ) +
      HSMul.hSMul (β := ℤ) n ((pB.basis.coord (⟨1, hdim⟩ : Fin pB.dim) : (a : 𝓞 K) → ℤ) 1 : ℤ)
⊢ 1 = pB.gen ^ (↑(⟨0, ⋯⟩ : Fin pB.dim) : ℕ)

Tactic:
simp
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h :
  1 =
    HAdd.hAdd (α := ℤ) (β := ℤ)
      ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) ((↑p : 𝓞 K) * x) : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
          (⟨1, hdim⟩ : Fin pB.dim) :
        ℤ)
      ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) (↑n : 𝓞 K) : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
          (⟨1, hdim⟩ : Fin pB.dim) :
        ℤ)
⊢ 1 =
    HSMul.hSMul (α := ℤ) (β := ℤ) (↑p : ℤ)
        ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) x : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
            (⟨1, hdim⟩ : Fin pB.dim) :
          ℤ) +
      HSMul.hSMul (β := ℤ) n (if (⟨0, ⋯⟩ : Fin pB.dim) = (⟨1, hdim⟩ : Fin pB.dim) then 1 else 0)

Tactic:
rw [show (p : 𝓞 K) * x = (p : ℤ) • x by simp, ← pB.basis.coord_apply,
    map_smul, ← zsmul_one, ← pB.basis.coord_apply, map_smul,
    show 1 = pB.gen ^ (⟨0, by lia⟩ : Fin pB.dim).1 by simp, ← pB.basis_eq_pow,
    pB.basis.coord_apply, pB.basis.coord_apply, pB.basis.repr_self_apply] at h

Premises used: Module.Basis.repr_self_apply, PowerBasis.basis, PowerBasis.basis_eq_pow, zsmul_one, Module.Basis.coord_apply, map_smul
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h :
  1 =
    HSMul.hSMul (α := ℤ) (β := ℤ) (↑p : ℤ)
        ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) x : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
            (⟨1, hdim⟩ : Fin pB.dim) :
          ℤ) +
      HSMul.hSMul (β := ℤ) n (if (⟨0, ⋯⟩ : Fin pB.dim) = (⟨1, hdim⟩ : Fin pB.dim) then 1 else 0)
⊢ 1 =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) x : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
          (⟨1, hdim⟩ : Fin pB.dim) :
        ℤ)

Tactic:
simp only [smul_eq_mul, Fin.mk.injEq, zero_ne_one, ↓reduceIte, mul_zero, add_zero] at h

Premises used: Fin.mk.injEq, zero_ne_one, MulZeroClass.mul_zero, reduceIte, smul_eq_mul, add_zero
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h :
  1 =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) x : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
          (⟨1, hdim⟩ : Fin pB.dim) :
        ℤ)
⊢ Nat.Prime (Int.natAbs (↑p : ℤ))

Tactic:
simp [hp.1]

Premises used: Fact.out
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h :
  1 =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((((pB.basis.repr : (a : 𝓞 K) → Fin pB.dim →₀ ℤ) x : Fin pB.dim →₀ ℤ) : (a : Fin pB.dim) → ℤ)
          (⟨1, hdim⟩ : Fin pB.dim) :
        ℤ)
⊢ False

Tactic:
exact (Int.prime_iff_natAbs_prime.2 (by simp [hp.1])).not_dvd_one ⟨_, h⟩

Premises used: Iff.mpr, Prime.not_dvd_one, Exists.intro, Int.prime_iff_natAbs_prime
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
⊢ ¬∃ (n : ℤ), (↑p : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)

Tactic:
not_exists_int_prime_dvd_sub_of_prime_pow_ne_two hζ (fun h ↦ ?_)

Premises used: IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
refine : ∀ (h : p ^ (k + 1) = 2), False
⊢ ¬∃ (n : ℤ), (↑p : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)

Tactic:
refine not_exists_int_prime_dvd_sub_of_prime_pow_ne_two hζ (fun h ↦ ?_)

Premises used: IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
h assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ : p ^ (k + 1) = 2
⊢ p ^ (k + 1) = 2

Tactic:
assumption_mod_cast
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
h : p ^ (k + 1) = 2
⊢ False

Tactic:
simp_all only [(@Nat.Prime.pow_eq_iff 2 p (k + 1) Nat.prime_two).mp (by assumption_mod_cast),
    pow_one, ne_eq]

Premises used: ne_eq, Nat.prime_two, pow_one, Iff.mp, Nat.Prime.pow_eq_iff
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ_1 : IsPrimitiveRoot ζ p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ ¬∃ (n : ℤ), (↑p : 𝓞 K) ∣ hζ_1.toInteger - (↑n : 𝓞 K)

Tactic:
not_exists_int_prime_dvd_sub_of_prime_ne_two hζ hodd

Premises used: IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ_1 : IsPrimitiveRoot ζ p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ ¬∃ (n : ℤ), (↑p : 𝓞 K) ∣ hζ_1.toInteger - (↑n : 𝓞 K)

Tactic:
exact not_exists_int_prime_dvd_sub_of_prime_ne_two hζ hodd

Premises used: IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ NumberField K

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : NumberField K
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}))

Tactic:
Ideal.finiteQuotientOfFreeOfNeBot _ (fun h ↦ ?_)

Premises used: Ideal.finiteQuotientOfFreeOfNeBot
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : NumberField K
refine : ∀ (h : Eq (α := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}) ⊥), False
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}))

Tactic:
refine Ideal.finiteQuotientOfFreeOfNeBot _ (fun h ↦ ?_)

Premises used: Ideal.finiteQuotientOfFreeOfNeBot
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : NumberField K
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}) ⊥
⊢ hζ.toInteger = 1

Tactic:
simp only [Ideal.span_singleton_eq_bot, sub_eq_zero] at h

Premises used: Ideal.span_singleton_eq_bot, sub_eq_zero
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : NumberField K
h : hζ.toInteger = 1
⊢ False

Tactic:
hζ.ne_one (one_lt_pow₀ hp.1.one_lt (Nat.zero_ne_add_one k).symm)
    (RingOfIntegers.ext_iff.1 h)

Premises used: Nat.Prime.one_lt, Ne.symm, Iff.mp, NumberField.RingOfIntegers.ext_iff, one_lt_pow₀, IsPrimitiveRoot.ne_one, Fact.out, Nat.zero_ne_add_one