awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₁⟯) ⊤
rw :
  (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime
    (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
⊢ IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)

Tactic:
rw [Int.isCoprime_iff_nat_coprime, hK₁, hK₂]

Premises used: Int.isCoprime_iff_nat_coprime
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)))

Tactic:
Coprime.coprime_div_left ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))

Premises used: NeZero.pos, Nat.Coprime.coprime_div_left, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₁⟯) ⊤
refine : (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
⊢ (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime
    (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))

Tactic:
refine Coprime.coprime_div_left ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))

Premises used: NeZero.pos, Nat.Coprime.coprime_div_left, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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)))

Tactic:
Coprime.coprime_div_right ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))

Premises used: Nat.Coprime.coprime_div_right, NeZero.pos, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₁⟯) ⊤
refine : (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂)
⊢ (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))

Tactic:
refine Coprime.coprime_div_right ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))

Premises used: Nat.Coprime.coprime_div_right, NeZero.pos, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₂)

Tactic:
Coprime.pow_left _ (Coprime.pow_right _ h)

Premises used: Nat.Coprime.pow_right, Nat.Coprime.pow_left
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₂)

Tactic:
exact Coprime.pow_left _ (Coprime.pow_right _ h)

Premises used: Nat.Coprime.pow_right, Nat.Coprime.pow_left
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₁⟯)

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)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₁⟯)
⊢ IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯

Tactic:
have h_dsj : ℚ⟮ζ ^ n₂⟯.LinearDisjoint ℚ⟮ζ ^ n₁⟯ :=
      linearDisjoint_of_isGalois_isCoprime_discr _ _ _ h_cpr
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₁⟯
⊢ ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁

Tactic:
have h_div₁ := prod_primeFactors_pow_totient_ediv_dvd n₁.pos_of_neZero
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₁
⊢ ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂

Tactic:
have h_div₂ := prod_primeFactors_pow_totient_ediv_dvd n₂.pos_of_neZero
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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₂
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)))
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 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]

Premises used: NumberField.isCoprime_differentIdeal_of_isCoprime_discr, NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow, Nat.mul_div_mul_comm, Rat, pow_dvd_pow_of_dvd, Membership.mem, Subtype, Finset.prod_union, Nat.totient, HPow.hPow, IntermediateField.adjoin, IsCyclotomicExtension.Rat.finrank, Nat.primeFactors_mul, Nat.Coprime.disjoint_primeFactors, Singleton.singleton, Finset.prod_pow, Nat.div_pow, NeZero.ne
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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 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
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
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
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)))
⊢ (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:
simp_rw +contextual [← pow_mul, Nat.div_mul_right_comm (this _), Nat.totient_mul h]

Premises used: Nat.totient_mul, pow_mul, Nat.div_mul_right_comm