awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ p ∣ n
have rsuffices : ∀ (q : ℕ) (hq : Nat.Prime q) (t s : ℕ) (ht₁ : t ≠ 0) (ht₂ : n = q ^ t) (hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s),
  p ∣ n
Tactic: rsuffices ⟨q, hq, t, s, ht₁, ht₂, hs⟩ :
      ∃ q, q.Prime ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ (p : ℤ) ∣ (q : ℤ) ^ s := by
    obtain hn | hn := lt_or_eq_of_le hn
    · by_cases! h : ∃ q, q.Prime ∧ ∃ t, q ^ t = n
      · obtain ⟨q, hq, t, hn'⟩ := h
        have : Fact (Nat.Prime q) := ⟨hq⟩
        cases t with
        | zero => simp [← hn'] at hn
        | succ r =>
          rw [← hn'] at hC hμ
          refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
          by_cases hq' : q = 2
          · cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
          · rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp
      · rw [IsPrimitiveRoot.norm_toInteger_sub_one_eq_one hμ hn, one_pow,
          Int.natCast_dvd_ofNat, Nat.dvd_one] at hp
        · exact (Nat.Prime.ne_one hF.out hp).elim
        · exact fun {p} a k ↦ h p a k
    · rw [← hn] at hμ hC ⊢
      refine ⟨2, Nat.prime_two, 1, Module.finrank ℚ⟮ζ⟯ K, one_ne_zero, by rw [pow_one], ?_⟩
      rwa [hμ.norm_toInteger_sub_one_of_eq_two, neg_eq_neg_one_mul, mul_pow, IsUnit.dvd_mul_left
        ((isUnit_pow_iff Module.finrank_pos.ne').mpr isUnit_neg_one)] at hp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
⊢ p = q
have hs₁ : p ∣ q ^ s
Tactic: rw [← Int.natCast_pow, Int.natCast_dvd_natCast] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
⊢ p ∣ n
have this₁ : p = q
Tactic: have : p = q := by
    rw [← Int.natCast_pow, Int.natCast_dvd_natCast] at hs
    exact (Nat.prime_dvd_prime_iff_eq hF.out hq).mp (hF.out.dvd_of_dvd_pow hs)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
this : p = q
⊢ p ∣ n
have rw : q ∣ q ^ t
Tactic: rw [ht₂, this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
⊢ NumberField.discr K =
    HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))
have hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
Tactic: have hζ := IsCyclotomicExtension.zeta_spec (p ^ k) ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
⊢ NumberField.discr K =
    HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))
have this : NumberField K
Tactic: have : NumberField K := IsCyclotomicExtension.numberField {p ^ k} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ NumberField.discr K =
    HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))
have a : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (NumberField.discr K) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) :
    ℚ)
Tactic: apply (algebraMap ℤ ℚ).injective_int
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (NumberField.discr K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) :
      ℚ)
have a : Algebra.discr (ι := Fin pB₁.dim) ℚ (B := K)
    (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) : (a : Fin pB₁.dim) → K) =
  (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
    (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1)))
Tactic: rw [← NumberField.discr_eq_discr _ pB₁.basis, ← Algebra.discr_localizationLocalization ℤ ℤ⁰ K]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ Algebra.discr (ι := Fin pB₁.dim) ℚ (B := K)
      (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) : (a : Fin pB₁.dim) → K) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1)))
have h : Algebra.discr (ι := Fin pB₁.dim) ℚ (B := K)
    (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) : (a : Fin pB₁.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: convert!
    IsCyclotomicExtension.discr_prime_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _)) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
h :
  Algebra.discr (ι := Fin pB₁.dim) ℚ (B := K)
      (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) : (a : Fin pB₁.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 pB₁.dim) ℚ (B := K)
      (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) : (a : Fin pB₁.dim) → K) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1)))
have h₁ : (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
    (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) =
  HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
Tactic: convert!
    IsCyclotomicExtension.discr_prime_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _)) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ pB₁.dim = PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ)
have rw : Module.finrank.{0, u} ℤ (𝓞 K) = Module.finrank ℚ K
Tactic: rw [← PowerBasis.finrank, ← PowerBasis.finrank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ Algebra.discr (ι := Fin pB₁.dim) ℚ (B := K)
      (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) : (a : Fin pB₁.dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
have this₁ : pB₁.dim = PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ)
Tactic: have : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim := by
      rw [← PowerBasis.finrank, ← PowerBasis.finrank]
      exact RingOfIntegers.rank K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this_1 : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
this : pB₁.dim = PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ)
⊢ Algebra.discr (ι := Fin pB₁.dim) ℚ (B := K)
      (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) : (a : Fin pB₁.dim) → K) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
have h : Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
    (Function.comp (β := Fin pB₁.dim)
      (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis : Module.Basis (Fin pB₁.dim) ℚ K) :
        (a : Fin pB₁.dim) → K)
      (⇑(finCongr this).symm : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → Fin pB₁.dim)) =
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
    (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
Tactic: rw [← Algebra.discr_reindex _ _ (finCongr this)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this_1 : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
this : pB₁.dim = PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ)
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (Function.comp (β := Fin pB₁.dim)
        (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis : Module.Basis (Fin pB₁.dim) ℚ K) :
          (a : Fin pB₁.dim) → K)
        (⇑(finCongr this).symm : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → Fin pB₁.dim)) =
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
have h : Eq (α := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ)) → K)
  (Function.comp (β := Fin pB₁.dim)
    (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis : Module.Basis (Fin pB₁.dim) ℚ K) : (a : Fin pB₁.dim) → K)
    (⇑(finCongr this).symm : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → Fin pB₁.dim))
  (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this_1 : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
this : pB₁.dim = PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ)
⊢ Eq (α := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ)) → K)
    (Function.comp (β := Fin pB₁.dim)
      (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis : Module.Basis (Fin pB₁.dim) ℚ K) :
        (a : Fin pB₁.dim) → K)
      (⇑(finCongr this).symm : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → Fin pB₁.dim))
    (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
have h : ∀ (i : Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))),
  Eq (α := K)
    (Function.comp (β := Fin pB₁.dim)
        (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis : Module.Basis (Fin pB₁.dim) ℚ K) :
          (a : Fin pB₁.dim) → K)
        (⇑(finCongr this).symm : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → Fin pB₁.dim) i :
      K)
    ((PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) i : K)
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this_1 : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
this : pB₁.dim = PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))
⊢ Eq (α := K)
    (Function.comp (β := Fin pB₁.dim)
        (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis : Module.Basis (Fin pB₁.dim) ℚ K) :
          (a : Fin pB₁.dim) → K)
        (⇑(finCongr this).symm : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → Fin pB₁.dim) i :
      K)
    ((PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) i : K)
have h : Eq (α := K)
  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      (hζ.toInteger ^
        (↑(((finCongr this).symm :
                (a : Fin (minpoly ℚ (zeta (p ^ k) ℚ K)).natDegree) → Fin hζ.integralPowerBasisOfPrimePow.dim)
              i) :
          ℕ)) :
    K)
  ((PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ) : (a : Fin (minpoly ℚ (zeta (p ^ k) ℚ K)).natDegree) → K) i : K)
Tactic: simp_rw [Function.comp_apply, Module.Basis.localizationLocalization_apply, powerBasis_dim,
      PowerBasis.coe_basis, pB₁, integralPowerBasisOfPrimePow_gen]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
have h : (Int.castRingHom ℚ : (a : ℤ) → ℚ)
    (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) =
  HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
Tactic: simp_rw [algebraMap_int_eq, map_mul, map_pow, map_neg, map_one, map_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
h :
  (Int.castRingHom ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
⊢ (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
have h₁ : HMul.hMul (α := ℚ) (β := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2)) : ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) : ℚ) =
  HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
Tactic: simp_rw [algebraMap_int_eq, map_mul, map_pow, map_neg, map_one, map_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
h :
  (Int.castRingHom ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
h₁ :
  HMul.hMul (α := ℚ) (β := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2)) : ℚ)
      ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) : ℚ) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
⊢ (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
have h₂ : HPow.hPow (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (-1) : ℚ) (φ (p ^ k) / 2) *
    HPow.hPow (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (↑p : ℤ) : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1)) =
  HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
Tactic: simp_rw [algebraMap_int_eq, map_mul, map_pow, map_neg, map_one, map_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
h :
  (Int.castRingHom ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
h₁ :
  HMul.hMul (α := ℚ) (β := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2)) : ℚ)
      ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) : ℚ) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
h₂ :
  HPow.hPow (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (-1) : ℚ) (φ (p ^ k) / 2) *
      HPow.hPow (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (↑p : ℤ) : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
⊢ (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
have h₃ : HPow.hPow (α := ℚ) (-(Int.castRingHom ℚ : (a : ℤ) → ℚ) 1 : ℚ) (φ (p ^ k) / 2) *
    HPow.hPow (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (↑p : ℤ) : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1)) =
  HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
Tactic: simp_rw [algebraMap_int_eq, map_mul, map_pow, map_neg, map_one, map_natCast]