awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
⊢ Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
have this₁ : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
Tactic: have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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_5 : 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))
this_6 : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
this : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
have rw : IsCyclotomicExtension.{0, u} {n₁.lcm n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
Tactic: rw [← Nat.Coprime.lcm_eq_mul 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₂
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_5 : 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))
this_6 : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
this : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
⊢ Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
have this₁ : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
Tactic: have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
-- 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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
Tactic: have h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤ := by
      have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
      have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
      exact isCyclotomicExtension_eq {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₂
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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
⊢ IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
have rw : (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime
  (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
Tactic: rw [Int.isCoprime_iff_nat_coprime, hK₁, hK₂]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
⊢ (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime
    (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
have refine : (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
Tactic: refine Coprime.coprime_div_left ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
⊢ (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
have refine : (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂)
Tactic: refine Coprime.coprime_div_right ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
-- 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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
Tactic: have h_cpr : IsCoprime (discr ℚ⟮ζ ^ n₂⟯) (discr ℚ⟮ζ ^ n₁⟯) := by
      rw [Int.isCoprime_iff_nat_coprime, hK₁, hK₂]
      refine Coprime.coprime_div_left ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
      refine Coprime.coprime_div_right ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
      exact Coprime.pow_left _ (Coprime.pow_right _ 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₂
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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have h_dsj : IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯
Tactic: have h_dsj : ℚ⟮ζ ^ n₂⟯.LinearDisjoint ℚ⟮ζ ^ n₁⟯ :=
      linearDisjoint_of_isGalois_isCoprime_discr _ _ _ h_cpr
-- 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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
Tactic: have h_div₁ := prod_primeFactors_pow_totient_ediv_dvd n₁.pos_of_neZero
-- 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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
Tactic: have h_div₂ := prod_primeFactors_pow_totient_ediv_dvd n₂.pos_of_neZero
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))
have e_a : (n₁ ^ φ n₁) ^ φ n₂ * (n₂ ^ φ n₂) ^ φ n₁ /
    HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, (x ^ (φ n₁ / (x - 1))) ^ φ n₂)
      (∏ x ∈ n₂.primeFactors, (x ^ (φ n₂ / (x - 1))) ^ φ n₁) =
  (n₁ * n₂) ^ φ (n₁ * n₂) /
    HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ (n₁ * n₂) / (x - 1)))
      (∏ x ∈ n₂.primeFactors, x ^ (φ (n₁ * n₂) / (x - 1)))
Tactic: rw [natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow K ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯ h_dsj h_top
      (isCoprime_differentIdeal_of_isCoprime_discr _ h_cpr), hK₁, hK₂,
      finrank n₁ ℚ⟮ζ ^ n₂⟯, finrank n₂ ℚ⟮ζ ^ n₁⟯, Nat.div_pow h_div₁, Nat.div_pow h_div₂,
      ← Nat.mul_div_mul_comm (pow_dvd_pow_of_dvd h_div₁ n₂.totient)
      (pow_dvd_pow_of_dvd h_div₂ n₁.totient), primeFactors_mul (NeZero.ne _) (NeZero.ne _),
      Finset.prod_union h.disjoint_primeFactors, ← Finset.prod_pow, ← Finset.prod_pow]
-- 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_5 : 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))
this : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
⊢ (n₁ ^ φ n₁) ^ φ n₂ * (n₂ ^ φ n₂) ^ φ n₁ /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, (x ^ (φ n₁ / (x - 1))) ^ φ n₂)
        (∏ x ∈ n₂.primeFactors, (x ^ (φ n₂ / (x - 1))) ^ φ n₁) =
    (n₁ * n₂) ^ φ (n₁ * n₂) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ (n₁ * n₂) / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ (n₁ * n₂) / (x - 1)))
have this₁ : ∀ {n p : ℕ} (hp : p ∈ n.primeFactors), p - 1 ∣ φ n
Tactic: have {n p : ℕ} (hp : p ∈ n.primeFactors) : p - 1 ∣ n.totient :=
      p.totient_prime (prime_of_mem_primeFactors hp) ▸ totient_dvd_of_dvd (b := n)
        <| dvd_of_mem_primeFactors hp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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_5 : 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))
this_6 : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
this : ∀ {n p : ℕ} (hp : p ∈ n.primeFactors), p - 1 ∣ φ n
⊢ (n₁ ^ φ n₁) ^ φ n₂ * (n₂ ^ φ n₂) ^ φ n₁ /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, (x ^ (φ n₁ / (x - 1))) ^ φ n₂)
        (∏ x ∈ n₂.primeFactors, (x ^ (φ n₂ / (x - 1))) ^ φ n₁) =
    (n₁ * n₂) ^ φ (n₁ * n₂) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ (n₁ * n₂) / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ (n₁ * n₂) / (x - 1)))
have e_a : n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₂ * φ n₁) /
    HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
      (∏ x ∈ n₂.primeFactors, x ^ (φ n₂ * φ n₁ / (x - 1))) =
  (n₁ * n₂) ^ (φ n₁ * φ n₂) /
    HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
      (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
Tactic: simp_rw +contextual [← pow_mul, Nat.div_mul_right_comm (this _), Nat.totient_mul h]