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
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))
⊢ (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 (α := ℚ) (-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 (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p} ℚ K
⊢ NumberField.discr K = HPow.hPow (α := ℤ) (-1) ((p - 1) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p - 2)
have this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
Tactic: have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by
    rw [zero_add, pow_one]
    infer_instance
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ NumberField.discr K = HPow.hPow (α := ℤ) (-1) ((p - 1) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p - 2)
have 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)
Tactic: rw [discr_prime_pow_succ p 0 K]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
⊢ NumberField.discr K =
    HPow.hPow (α := ℤ) (-1) (φ n / 2) *
      (HPow.hPow (α := ℤ) (↑n : ℤ) (φ n) / (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) : ℤ))
have this : NumberField K
Tactic: haveI : NumberField K := IsCyclotomicExtension.numberField {n} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ NumberField.discr K =
    HPow.hPow (α := ℤ) (-1) (φ n / 2) *
      (HPow.hPow (α := ℤ) (↑n : ℤ) (φ n) / (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) : ℤ))
have 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))) : ℤ))
Tactic: rw [← Int.sign_mul_natAbs (NumberField.discr K), sign_discr, nrComplexPlaces_eq_totient_div_two n]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ 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))) : ℤ))
have e_a : (NumberField.discr K).natAbs = n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ (NumberField.discr K).natAbs = (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))
have this₁ : Fact (Nat.Prime p)
Tactic: have : Fact (Nat.Prime p) := ⟨hp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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)
⊢ (NumberField.discr K).natAbs = (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))
have 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))
Tactic: rw [discr_prime_pow p k K]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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)
⊢ (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))
have 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))
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
Cleared hypotheses: k, hn, hK
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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))
⊢ (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))
have 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))
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
Cleared hypotheses: k, hn, hK
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have this₁ : NeZero n₁
Tactic: have : NeZero n₁ := NeZero.of_gt hn₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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_1 : NumberField K
this : NeZero n₁
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have this₁ : NeZero n₂
Tactic: have : NeZero n₂ := NeZero.of_gt hn₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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_1 : NumberField K
this_2 : NeZero n₁
this : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
Tactic: have hζ := zeta_spec (n₁ * n₂) ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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_1 : NumberField K
this_2 : NeZero n₁
this : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
⊢ n₁ * n₂ = n₂ * n₁
have rw : n₂ * n₁ = n₂ * n₁
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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_1 : NumberField K
this_2 : NeZero n₁
this : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
Tactic: have hζ₁ := hζ.pow (NeZero.pos _) (a := n₂) (b := n₁) (by rw [mul_comm])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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_1 : NumberField K
this_2 : NeZero n₁
this : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have this₁ : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
Tactic: have := hζ₁.intermediateField_adjoin_isCyclotomicExtension ℚ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
Tactic: have hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have hK₃ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
Tactic: replace hK₁ := @hK₁ ℚ⟮ζ ^ n₂⟯ _ _ _ _ (of_intermediateField _)
Cleared hypotheses: hK₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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))
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
Tactic: have hζ₂ := hζ.pow (NeZero.pos _) (a := n₁) (b := n₂) rfl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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))
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have this₁ : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
Tactic: have := hζ₂.intermediateField_adjoin_isCyclotomicExtension ℚ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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))
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have hζ₂' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
Tactic: have hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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))
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have hK₃ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
Tactic: replace hK₂ := @hK₂ ℚ⟮ζ ^ n₁⟯ _ _ _ _ (of_intermediateField _)
Cleared hypotheses: hK₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have this₁ : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
Tactic: have : IsGalois ℚ ℚ⟮ζ ^ n₂⟯ := isGalois {n₁} ℚ _