awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 + 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)
pos : ∀ (hk : k = 0), 1 < p ^ k * (p - 1)
⊢ 1 < p ^ k * (p - 1)
have neg : ∀ (hk : ¬k = 0), 1 < p ^ k * (p - 1)
Tactic: by_cases hk : k = 0
-- 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 + 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)
have pos : ∀ (htwo : p ≠ 2), 2 < p
Tactic: simp only [hk, zero_add, pow_one, pow_zero, one_mul, Nat.lt_sub_iff_add_lt,
        Nat.reduceAdd] at htwo ⊢
Cleared hypotheses: htwo
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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)
⊢ False
have hdim₁ : 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)
Cleared hypotheses: hdim
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ False
have h₁ : hζ.toInteger = (↑p : 𝓞 K) * x + (↑n : 𝓞 K)
Tactic: rw [sub_eq_iff_eq_add] at h
Cleared hypotheses: h, pB, hdim
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ False
have 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) :
    ℤ)
Tactic: replace h := pB.basis.ext_elem_iff.1 h ⟨1, hdim⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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) :
      ℤ)
⊢ False
have this : (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⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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) : ℕ)
⊢ False
have this₁ : (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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) : ℕ)
⊢ False
have this₁ : pB.gen = hζ.toInteger
Tactic: simp only [PowerBasis.coe_basis, pow_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ False
have 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) :
    ℤ)
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
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ False
have 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) :
      ℤ)
Tactic: simp only [↓reduceIte, map_add, Finsupp.coe_add, Pi.add_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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) :
        ℤ)
⊢ False
have 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, sorry⟩ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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)
⊢ False
have 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) :
      ℤ)
Tactic: simp only [smul_eq_mul, Fin.mk.injEq, zero_ne_one, ↓reduceIte, mul_zero, add_zero] at h
Cleared hypotheses: h
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
⊢ ¬∃ (n : ℤ), (↑p : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)
have refine : ∀ (h : p ^ (k + 1) = 2), False
Tactic: refine not_exists_int_prime_dvd_sub_of_prime_pow_ne_two hζ (fun 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
hodd : p ≠ 2
⊢ ¬∃ (n : ℤ), (↑p : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)
have this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
Tactic: have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
-- 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
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
⊢ ¬∃ (n : ℤ), (↑p : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)
have hζ₁ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
Tactic: replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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))
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}))
have this : NumberField K
Tactic: have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : NumberField 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:
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}) ⊥
⊢ 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 (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
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}))
have this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
Tactic: have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
-- 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
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ.toInteger - 1}))
have hζ₁ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
Tactic: replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
have pos : ∀ (htwo : p ^ (k + 1) = 2), hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
Tactic: by_cases htwo : p ^ (k + 1) = 2
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
pos : ∀ (htwo : p ^ (k + 1) = 2), hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
have neg : ∀ (htwo : ¬p ^ (k + 1) = 2), hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
Tactic: by_cases htwo : p ^ (k + 1) = 2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
have hp2 : p = 2
Tactic: have ⟨hp2, hk⟩ := (Nat.Prime.pow_eq_iff Nat.prime_two).1 htwo
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
hp2 : p = 2
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
have hk : k + 1 = 1
Tactic: have ⟨hp2, hk⟩ := (Nat.Prime.pow_eq_iff Nat.prime_two).1 htwo
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
hp2 : p = 2
hk : k + 1 = 1
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
have hk₁ : k = 0
Tactic: simp only [add_eq_right] at hk
Cleared hypotheses: hk
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
⊢ ζ = -1
have refine : IsPrimitiveRoot ζ 2
Tactic: refine IsPrimitiveRoot.eq_neg_one_of_two_right ?_
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
⊢ IsPrimitiveRoot ζ 2
have rwa : ∀ (hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0),
  IsPrimitiveRoot ζ 2
Tactic: rwa [hk, zero_add, pow_one, hp2] at hζ
Cleared hypotheses: hζ, htwo, hp2, hk
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
rwa :
  ∀ (hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0),
    IsPrimitiveRoot ζ 2
rwa₁ :
  ∀ (hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0),
    IsPrimitiveRoot ζ 2
⊢ IsPrimitiveRoot ζ 2
have rwa₂ : ∀ (hζ : IsPrimitiveRoot ζ p) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0), IsPrimitiveRoot ζ 2
Tactic: rwa [hk, zero_add, pow_one, hp2] at hζ
Cleared hypotheses: hζ, htwo, hp2, hk
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
rwa :
  ∀ (hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0),
    IsPrimitiveRoot ζ 2
rwa₁ :
  ∀ (hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0),
    IsPrimitiveRoot ζ 2
rwa₂ : ∀ (hζ : IsPrimitiveRoot ζ p) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0), IsPrimitiveRoot ζ 2
⊢ IsPrimitiveRoot ζ 2
have rwa₃ : ∀ (hζ : IsPrimitiveRoot ζ 2) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0), IsPrimitiveRoot ζ 2
Tactic: rwa [hk, zero_add, pow_one, hp2] at hζ
Cleared hypotheses: hζ, htwo, hp2, hk
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
hp2 : p = 2
hk : k = 0
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
have hζ' : ζ = -1
Tactic: have hζ' : ζ = -1 := by
      refine IsPrimitiveRoot.eq_neg_one_of_two_right ?_
      rwa [hk, zero_add, pow_one, hp2] at hζ
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : ζ = -1
⊢ hζ.toInteger = -1
have h : (↑hζ.toInteger : K) = (↑(-1) : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
hp2 : p = 2
hk : k = 0
hζ' : ζ = -1
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
have hζ'₁ : hζ.toInteger = -1
Tactic: replace hζ' : hζ.toInteger = -1 := by
      ext
      exact hζ'
Cleared hypotheses: hζ'
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
have pos : HSub.hSub (α := 𝓞 K) (-1) 1 ∣ (↑2 : 𝓞 K)
Tactic: rw [hζ', hp2]
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
have neg : hζ.toInteger - 1 ∣ (↑(↑p : ℤ) : 𝓞 K)
Tactic: suffices (hζ.toInteger - 1) ∣ (p : ℤ) by simpa
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ hζ.toInteger - 1 ∣ (↑(↑p : ℤ) : 𝓞 K)
have this : NumberField K
Tactic: have := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
this : NumberField K
⊢ hζ.toInteger - 1 ∣ (↑(↑p : ℤ) : 𝓞 K)
have H : (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ HPow.hPow (β := ℕ) p 0 - 1) =
  HPow.hPow (α := ℤ) (↑p : ℤ) (HPow.hPow (β := ℕ) p 0)
Tactic: have H := hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two zero_le htwo
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
this : NumberField K
H :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ HPow.hPow (β := ℕ) p 0 - 1) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (HPow.hPow (β := ℕ) p 0)
⊢ hζ.toInteger - 1 ∣ (↑(↑p : ℤ) : 𝓞 K)
have H₁ : (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) = HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1
Tactic: rw [pow_zero, pow_one] at H
Cleared hypotheses: H
-- 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 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
H : (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) = HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1
⊢ hζ.toInteger - 1 ∣ (↑(↑p : ℤ) : 𝓞 K)
have neg : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1 ∣ (↑p : ℤ)
Tactic: rw [← Ideal.norm_dvd_iff, H]