awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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 (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
IsCyclotomicExtension.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
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)
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))
⊢ 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:
convert!
    IsCyclotomicExtension.discr_prime_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _)) using 1

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
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
rw : Module.finrank.{0, u} ℤ (𝓞 K) = Module.finrank ℚ K
⊢ pB₁.dim = PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ)

Tactic:
rw [← PowerBasis.finrank, ← PowerBasis.finrank]

Premises used: PowerBasis.finrank
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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
⊢ Module.finrank.{0, u} ℤ (𝓞 K) = Module.finrank ℚ K

Tactic:
RingOfIntegers.rank K

Premises used: NumberField.RingOfIntegers.rank
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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
⊢ Module.finrank.{0, u} ℤ (𝓞 K) = Module.finrank ℚ K

Tactic:
exact RingOfIntegers.rank K

Premises used: NumberField.RingOfIntegers.rank
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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ζ)

Tactic:
have : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim := by
      rw [← PowerBasis.finrank, ← PowerBasis.finrank]
      exact RingOfIntegers.rank K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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ζ)
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)
⊢ 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:
rw [← Algebra.discr_reindex _ _ (finCongr this)]

Premises used: finCongr, Algebra.discr_reindex
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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ζ)
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)
⊢ 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:
congr 1
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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ζ)
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)
⊢ 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:
ext i
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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ζ))
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)
⊢ 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:
simp_rw [Function.comp_apply, Module.Basis.localizationLocalization_apply, powerBasis_dim,
      PowerBasis.coe_basis, pB₁, integralPowerBasisOfPrimePow_gen]

Premises used: IsPrimitiveRoot.powerBasis_dim, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, Module.Basis.localizationLocalization_apply, PowerBasis.coe_basis, Function.comp_apply
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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ζ))
⊢ PowerBasis.gen (IsPrimitiveRoot.powerBasis ℚ hζ) ^ (↑i : ℕ) =
    (PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) i

Tactic:
((IsPrimitiveRoot.powerBasis ℚ hζ).basis_eq_pow i).symm

Premises used: Rat, PowerBasis.basis_eq_pow, IsPrimitiveRoot.powerBasis, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)
    ((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:
convert! ← ((IsPrimitiveRoot.powerBasis ℚ hζ).basis_eq_pow i).symm using 1

Premises used: Rat, PowerBasis.basis_eq_pow, IsPrimitiveRoot.powerBasis, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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))
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))
h₄ :
  HPow.hPow (α := ℚ) (-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))

Tactic:
simp_rw [algebraMap_int_eq, map_mul, map_pow, map_neg, map_one, map_natCast]

Premises used: map_neg, map_pow, map_mul, map_natCast, map_one, algebraMap_int_eq
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
⊢ NumberField.discr K =
    HPow.hPow (α := ℤ) (-1) (p ^ k * (p - 1) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
simpa [totient_prime_pow hp.out (succ_pos k)] using discr_prime_pow p (k + 1) K

Premises used: Nat.totient_prime_pow, IsCyclotomicExtension.Rat.discr_prime_pow, HAdd.hAdd, Nat.succ_pos, OfNat.ofNat, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 rw : IsCyclotomicExtension {p} ℚ K
⊢ IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K

Tactic:
rw [zero_add, pow_one]

Premises used: zero_add, pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p} ℚ K
⊢ IsCyclotomicExtension {p} ℚ K

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p} ℚ K
⊢ IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by
    rw [zero_add, pow_one]
    infer_instance
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
rw :
  HPow.hPow (α := ℤ) (-1) (HPow.hPow (β := ℕ) p 0 * (p - 1) / 2) *
      HPow.hPow (α := ℤ) (↑p : ℤ) (HPow.hPow (β := ℕ) p 0 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1)) =
    HPow.hPow (α := ℤ) (-1) ((p - 1) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p - 2)
⊢ NumberField.discr K = HPow.hPow (α := ℤ) (-1) ((p - 1) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p - 2)

Tactic:
rw [discr_prime_pow_succ p 0 K]

Premises used: IsCyclotomicExtension.Rat.discr_prime_pow_succ, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
⊢ HPow.hPow (α := ℤ) (-1) (HPow.hPow (β := ℕ) p 0 * (p - 1) / 2) *
      HPow.hPow (α := ℤ) (↑p : ℤ) (HPow.hPow (β := ℕ) p 0 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1)) =
    HPow.hPow (α := ℤ) (-1) ((p - 1) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p - 2)

Tactic:
simp [Nat.sub_sub]

Premises used: Nat.sub_sub
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
⊢ NumberField K

Tactic:
haveI : NumberField K := IsCyclotomicExtension.numberField {n} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
rw :
  HPow.hPow (α := ℤ) (-1) (φ n / 2) * (↑(NumberField.discr K).natAbs : ℤ) =
    HPow.hPow (α := ℤ) (-1) (φ n / 2) *
      (HPow.hPow (α := ℤ) (↑n : ℤ) (φ n) / (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) : ℤ))
⊢ NumberField.discr K =
    HPow.hPow (α := ℤ) (-1) (φ n / 2) *
      (HPow.hPow (α := ℤ) (↑n : ℤ) (φ n) / (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) : ℤ))

Tactic:
rw [← Int.sign_mul_natAbs (NumberField.discr K), sign_discr, nrComplexPlaces_eq_totient_div_two n]

Premises used: IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two, NumberField.discr, NumberField.sign_discr, Int.sign_mul_natAbs
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
e_a : (NumberField.discr K).natAbs = n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))
⊢ HPow.hPow (α := ℤ) (-1) (φ n / 2) * (↑(NumberField.discr K).natAbs : ℤ) =
    HPow.hPow (α := ℤ) (-1) (φ n / 2) *
      (HPow.hPow (α := ℤ) (↑n : ℤ) (φ n) / (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) : ℤ))

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (R := ℕ) 0
hK : IsCyclotomicExtension {0} ℚ K
this : NumberField K
⊢ (NumberField.discr K).natAbs = HPow.hPow (α := ℕ) 0 (φ 0) / ∏ p ∈ primeFactors 0, p ^ (φ 0 / (p - 1))

Tactic:
(neZero_zero_iff_false.mp hn).elim

Premises used: False.elim, neZero_zero_iff_false, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (R := ℕ) 0
hK : IsCyclotomicExtension {0} ℚ K
this : NumberField K
⊢ (NumberField.discr K).natAbs = HPow.hPow (α := ℕ) 0 (φ 0) / ∏ p ∈ primeFactors 0, p ^ (φ 0 / (p - 1))

Tactic:
exact (neZero_zero_iff_false.mp hn).elim

Premises used: False.elim, neZero_zero_iff_false, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Nat.Prime p
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
this : NumberField K
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact (Nat.Prime p) := ⟨hp⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Nat.Prime p
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
this_1 : NumberField K
this : Fact (Nat.Prime p)
e_a :
  (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))).natAbs =
    (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))
⊢ (NumberField.discr K).natAbs = (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))

Tactic:
rw [discr_prime_pow p k K]

Premises used: IsCyclotomicExtension.Rat.discr_prime_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
hp : Nat.Prime p
K : Type u
inst : Field K
inst_1 : CharZero K
this_1 : NumberField K
this : Fact (Nat.Prime p)
hn : NeZero (HPow.hPow (β := ℕ) p 0)
hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K
⊢ (HPow.hPow (α := ℤ) (-1) (φ (HPow.hPow (β := ℕ) p 0) / 2) *
        HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ HSub.hSub (α := ℕ) 0 1 * ((p - 1) * 0 - 1))).natAbs =
    HPow.hPow (β := ℕ) p 0 ^ φ (HPow.hPow (β := ℕ) p 0) /
      ∏ p_1 ∈ (HPow.hPow (β := ℕ) p 0).primeFactors, p_1 ^ (φ (HPow.hPow (β := ℕ) p 0) / (p_1 - 1))

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
hp : Nat.Prime p
K : Type u
inst : Field K
inst_1 : CharZero K
this_1 : NumberField K
this : Fact (Nat.Prime p)
k : ℕ
hn : NeZero (p ^ (k + 1))
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
⊢ (HPow.hPow (α := ℤ) (-1) (φ (p ^ (k + 1)) / 2) *
        HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))).natAbs =
    (p ^ (k + 1)) ^ φ (p ^ (k + 1)) / ∏ p_1 ∈ (p ^ (k + 1)).primeFactors, p_1 ^ (φ (p ^ (k + 1)) / (p_1 - 1))

Tactic:
simpa only [Int.reduceNeg, add_tsub_cancel_right, Int.natAbs_mul, Int.natAbs_pow,
        IsUnit.neg_iff, isUnit_one, Int.natAbs_of_isUnit, one_pow, Int.natAbs_natCast, one_mul]
        using (Nat.prime_pow_pow_totient_ediv_prod hp k.zero_lt_succ).symm

Premises used: one_pow, Int.natAbs_mul, Int.reduceNeg, Nat.zero_lt_succ, IsUnit.neg_iff, Int.natAbs_pow, isUnit_one, add_tsub_cancel_right, Int.natAbs_natCast, Eq.symm, Int.natAbs_of_isUnit, one_mul, Nat.prime_pow_pow_totient_ediv_prod
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Nat.Prime p
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
this_1 : NumberField K
this : Fact (Nat.Prime p)
e_a :
  ∀ [hn : NeZero (HPow.hPow (β := ℕ) p 0)] [hK : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K],
    (HPow.hPow (α := ℤ) (-1) (φ (HPow.hPow (β := ℕ) p 0) / 2) *
          HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ HSub.hSub (α := ℕ) 0 1 * ((p - 1) * 0 - 1))).natAbs =
      HPow.hPow (β := ℕ) p 0 ^ φ (HPow.hPow (β := ℕ) p 0) /
        ∏ p_1 ∈ (HPow.hPow (β := ℕ) p 0).primeFactors, p_1 ^ (φ (HPow.hPow (β := ℕ) p 0) / (p_1 - 1))
e_a₁ :
  ∀ (k : ℕ) [hn : NeZero (p ^ (k + 1))] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K],
    (HPow.hPow (α := ℤ) (-1) (φ (p ^ (k + 1)) / 2) *
          HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))).natAbs =
      (p ^ (k + 1)) ^ φ (p ^ (k + 1)) / ∏ p_1 ∈ (p ^ (k + 1)).primeFactors, p_1 ^ (φ (p ^ (k + 1)) / (p_1 - 1))
⊢ (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))).natAbs =
    (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))

Tactic:
cases k with
    | zero => simp
    | succ k =>
      simpa only [Int.reduceNeg, add_tsub_cancel_right, Int.natAbs_mul, Int.natAbs_pow,
        IsUnit.neg_iff, isUnit_one, Int.natAbs_of_isUnit, one_pow, Int.natAbs_natCast, one_mul]
        using (Nat.prime_pow_pow_totient_ediv_prod hp k.zero_lt_succ).symm

Premises used: one_pow, Int.natAbs_mul, Int.reduceNeg, Nat.zero_lt_succ, IsUnit.neg_iff, Int.natAbs_pow, isUnit_one, Nat.zero, add_tsub_cancel_right, Int.natAbs_natCast, Eq.symm, Nat.succ, Int.natAbs_of_isUnit, one_mul, Nat.prime_pow_pow_totient_ediv_prod
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₁ :
  ∀ (K : Type u) [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K]
    (this : NumberField K), (NumberField.discr K).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hK₂ :
  ∀ (K : Type u) [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K]
    (this : NumberField K), (NumberField.discr K).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this : NumberField K
⊢ NeZero n₁

Tactic:
have : NeZero n₁ := NeZero.of_gt hn₁